Prove extra wires do not lower the G20 boundary below 38 ADDs (no κ)

research/g20-extended-wire-boundary-floor/README.md

@@ -0,0 +1,134 @@
+# Extra wires do not lower the G20 boundary below 38 ADDs
+
+This scoped proof was produced by Nick Petalas. **No new κ.** It answers the
+open question of unpaidmoon's
+[PR6641](https://github.com/CrocSwap/integer-mult-bounds/pull/6641)
+(`5af623f5912f997163639e061feca4ebcf7e189e`): neither a priced scratch wire
+nor a gate that leaves the 32 boundary wires lowers a legal GL(2)-commutant
+side of the pinned PR5840 G20 boundary below **38 unit ADDs**. This holds for
+any number of extra wires, under any nonnegative tariff, and whether each extra
+wire is clean, dirty and restored, or left holding garbage. The scratch-free
+words attain 38, so the exact minimum stays **38 per side and 76 per port**.
+
+## Lemma
+
+Work over F2 on `N = n + k` wires. A unit ADD is `x_d <- x_d + x_s` with
+`d != s`; a SWAP costs three ADDs. A word of length `T` has matrix `M`. Let `A`
+be the `n x n` block of `M` on a fixed set of n data wires (data outputs as
+functions of data inputs). Let `v(A)` be the number of components of the
+undirected graph on the data wires with an edge `{i, j}` when `A_ij = 1` or
+`A_ji = 1`, and let `z(A)` be the number of zero diagonal entries of `A`. Then
+
+```text
+T >= n - v(A) + z(A).
+```
+
+Nothing is assumed about the extra wires' inputs or outputs, or about the
+other three blocks of `M`.
+
+**Proof.** This is the counting argument of Bu, Fan and Joo (arXiv:2408.07898,
+Lemma 3.6 and Theorem 5.2), as written out for 32 wires in JoyboyBrian's
+[PR6105](https://github.com/CrocSwap/integer-mult-bounds/pull/6105), run on
+all `N` wires and then restricted to the data block. Let `P_t` be the partition
+of the `N` wires into components of the graph of the first `t` gates.
+
+1. *Support invariant.* `M_t[i][j] = 1` implies `i, j` lie in one block of
+   `P_t`. This holds at `t = 0`. A gate `d <- d + s` changes only row `d`, to a
+   row supported in the blocks of `d` and `s`, which the gate merges.
+2. *Potential.* Put `Φ_t = N - |P_t| + z_N(M_t)`, where `z_N` counts zero
+   diagonal entries over all `N` wires, so `Φ_0 = 0`. If a gate joins two
+   blocks, `|P|` drops by one and `M_t[s][d] = 0` by step 1, so no diagonal
+   entry changes. Otherwise `|P|` is unchanged and only entry `d` can change.
+   Either way `Φ` grows by at most one per gate, so `Φ_T <= T`.
+3. *Restriction.* The data block of `M` is `A`, so `z_N(M) >= z(A)`. If
+   `A_ij = 1`, then `i, j` share a block of `P_T` by step 1. Each block of `P_T`
+   that meets the data wires is therefore a union of support components of
+   `A`, so at most `v(A)` blocks meet them. The other blocks lie among the `k`
+   extra wires. Hence `|P_T| <= v(A) + k` and
+   `T >= Φ_T >= n + k - v(A) - k + z(A) = n - v(A) + z(A)`. ∎
+
+## Consequence for the G20 boundary
+
+The consumer reads the 32 labelled wires, so a word that implements one side
+must have that side as its data block, with the data block's inputs on the
+same 32 labels. For a legal basis `S` in PR6641's commutant `GL(2, F2)^16`,
+the side is `S^{-1} L` or `R S`. PR6641 proves that the minimum of
+`n - v + z` over that commutant is 38 on each side. By the lemma, every
+extended word for every legal side therefore costs at least 38. A scratch
+tariff is added on top, and the published scratch-free words reach 38, so no
+nonnegative tariff helps.
+
+The same lemma settles the scalar part of the two-helper question in
+[PR5898](https://github.com/CrocSwap/integer-mult-bounds/pull/5898): any bank
+exchange `(a, b) -> (A b, B a)` has `z = 4` and `v <= 2`, so it costs at least
+six ADDs with any number of helpers.
+
+## Evidence
+
+`verify.py` uses only the standard library and writes nothing:
+
+- **Pinned boundary.** Both programs replay to the stored rows of the
+  SHA256-pinned controller, each expands to 38 ADDs and each side has
+  `n - v + z = 38`.
+- **Eight extended-wire controls.** On a 33rd wire, per side: a clean scratch
+  that copies data and is cleared from final rows (47 left, 41 right), a garbage
+  scratch (39), a clean relay that carries wire 31 through the whole word (42)
+  and a dirty live wire that carries wire 31 and is restored exactly (44). Each
+  realizes the same data block, respects the floor and costs more than 38.
+- **Potential trace.** On 400 seeded random words with one to three extra
+  wires, every step checks the support invariant, the unchanged diagonal at
+  joins and `Φ_t <= t`. 47 words meet the floor with equality.
+- **Complete width four.** Breadth-first search gives exact distances for all
+  20,160 elements of GL(4, F2). All 302,400 (state, data subset) pairs respect
+  the floor. As a statistic, 140 of the 480 reachable data blocks of width one
+  to three meet it at their least distance.
+
+The finite checks test the lemma's arithmetic. The proof above is the claim.
+
+## Reproduce
+
+From the repository root, with CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/g20-extended-wire-boundary-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/g20-extended-wire-boundary-floor
+```
+
+Expected output:
+
+```text
+PASS_G20_EXTENDED_WIRE_FLOOR side=38 port=76 witness=38/38 controls=8 control_lengths=[39, 41, 42, 44, 47] random_words=400 random_tight=47 gl4_states=20160 gl4_checks=302400 gl4_blocks=480 gl4_attained=140 no_new_kappa
+```
+
+Use another CPython 3.12 path on another machine. The run takes under a second.
+
+## Limits
+
+This is a scoped proof for unit two-wire XOR words, plus SWAPs at three ADDs.
+It is not a multiplication theorem or a supplier admission. Selected
+conditional κ and its five framework assumptions are unchanged. Not covered:
+
+- outputs that end on different physical wires, with the consumer relabelled;
+- nonlinear gates, multi-target XORs at unit cost and non-unit tariffs;
+- a changed controller, target diagonal or basis outside PR6641's commutant;
+- native, ownership, compiler, precision and caller obligations.
+
+The commutant minimum of 38 is PR6641's result, cited at its head and not
+replayed here. No Lean, Docker, native or selected-frontier replay was run.
+
+## Open next questions
+
+1. Can a side that leaves its data on other physical wires, with the consumer's
+   relabelling charged, beat 76 ADDs per port? The first step is to price the
+   relabel and compute `n - v + z` for the row-permuted data block.
+2. Does a priced multi-target or nonlinear gate lower either side? The
+   potential count above uses two-wire XOR gates only. Test one priced
+   multi-target XOR on the four-wire exchange corner first.
+
+## Credit
+
+unpaidmoon posed the question and proved the commutant floor (PR6641).
+JoyboyBrian proved the fixed-boundary 38-ADD floor and wrote out the counting
+proof extended here (PR6105). Alan Bu, Evan Fan and Robert Joo own the
+`n - v + z` bound. Ali Romman supplied the PR5840 controller, retained by
+Charan . in PR5851. Nick Petalas's PR5898 posed the two-helper question.

research/g20-extended-wire-boundary-floor/SOURCES.json

@@ -0,0 +1,45 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "73fa9f40a032f11dabf357eba69066fcf9bf0a02",
+      "sha256": "978536e852c0cfbc150f143e19d2cfddbb434bac6017d914974eb99f641593a8"
+    }
+  ],
+  "mathematical_references": [
+    {
+      "pr": 6641,
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6641",
+      "head": "5af623f5912f997163639e061feca4ebcf7e189e",
+      "path": "research/g20-gl2-commutant-floor/README.md",
+      "author": "unpaidmoon",
+      "use": "Question source and the commutant minimum 38 of n - v + z over GL(2)^16, used as a cited step, not replayed."
+    },
+    {
+      "pr": 6105,
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6105",
+      "author": "JoyboyBrian",
+      "path": "research/g20-full-boundary-floor/README.md",
+      "use": "Scratch-free fixed-boundary floor whose counting proof is extended here."
+    },
+    {
+      "reference": "Alan Bu, Evan Fan and Robert Joo, Minimum Synthesis Cost of CNOT Circuits, arXiv:2408.07898, Lemma 3.6 and Theorem 5.2",
+      "use": "The n - v + z counting bound on n wires."
+    }
+  ]
+}

research/g20-extended-wire-boundary-floor/TASK.json

@@ -0,0 +1,116 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "bit-helper-contract",
+    "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "research/g20-helper-split/README.md",
+      "research/g20-conjugation-admission/README.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "G20",
+      "helper split",
+      "5679",
+      "5708",
+      "independent target"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove that the n - v + z unit-ADD floor of a target data block holds for every word on any number of added wires, whatever their initial or final contract, and apply it to the pinned PR5840 G20 boundary: no scratch wire, external wire or tariff lowers a legal GL(2)-commutant side below 38 unit ADDs.",
+  "scope_change_reason": "The card asks for a changed G20 helper path or target split. PR6641 leaves a narrower live question on the same boundary: whether one priced scratch wire, or a gate that leaves the 32 wires, lowers the 38-ADD side. That question is answered here for every number of extra wires. Helpers, targets and the recursive moment are unchanged.",
+  "bottleneck_link": "A cheaper boundary word would lower the scalar BIT conversion invoice. Workspace was the remaining unpriced route left by the scratch-free floors. It is closed for unit binary ADD words, so a BIT improvement on this boundary must change the target, the controller or the gate alphabet.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop when the extended-wire floor is proved and bound to the pinned boundary. Do not search for nonlinear gates or changed output placements.",
+  "outcome": "negative-result",
+  "evidence": "PROOF in README.md; verify.py replays both pinned sides, eight extended-wire controls, a step-by-step potential check on 400 seeded random words with extra wires, and every state of GL(4, F2) against every data-wire subset.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a word that leaves the data on a different set of physical wires, charged for the consumer's relabelling, beat 76 ADDs per port?",
+      "why_it_matters": "The floor fixes the 32 output labels. Ending a side on scratch wires and relabelling the consumer is a different contract that this proof does not cover.",
+      "first_step": "Price the consumer-side relabel and compute n - v + z for the row-permuted data block of one side.",
+      "blocked_by": "Requires a caller contract that accepts relocated outputs."
+    },
+    {
+      "question": "Does a nonlinear or non-unit gate (Toffoli, carry, multi-target XOR at one unit) lower either side?",
+      "why_it_matters": "The potential argument uses only two-wire XOR gates. A multi-target or controlled gate changes the alphabet and the bound.",
+      "first_step": "Fix one priced multi-target XOR tariff and redo the potential count on the four-wire exchange corner.",
+      "blocked_by": "No such gate is priced in the current native model."
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 5840,
+      "author": "Ali Romman",
+      "relationship": "Controller, equal-target diagonal, and boundary programs used as the live input."
+    },
+    {
+      "pr": 5851,
+      "author": "Charan .",
+      "relationship": "Vendored controller retained by the isolated-exchange package; not re-proved."
+    },
+    {
+      "pr": 6081,
+      "author": "JoyboyBrian",
+      "relationship": "Fixed-endpoint 38-ADD theorem whose open GL2 question this package answers."
+    },
+    {
+      "pr": 6105,
+      "author": "JoyboyBrian",
+      "relationship": "Full fixed-boundary 38-ADD floor with cross-component gates; scratch excluded there."
+    },
+    {
+      "pr": 6641,
+      "author": "unpaidmoon",
+      "relationship": "GL(2)-commutant 38-ADD floor at head 5af623f5912f997163639e061feca4ebcf7e189e and the open question answered here. Cited, not replayed."
+    },
+    {
+      "pr": 5898,
+      "author": "Nick Petalas",
+      "relationship": "One-clean-helper bank-exchange floor; the lemma here also covers its open two-helper question for the scalar floor."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376826"
+}

research/g20-extended-wire-boundary-floor/VERIFY.json

@@ -0,0 +1,23 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Pinned boundary replay and floor 38, eight extended-wire controls, step-by-step potential on 400 seeded words with extra wires, and every GL(4, F2) state against every data subset."
+    }
+  ]
+}