Prove exact 20-ADD floor for the G20 chain/exchange component (no new κ)

research/g20-chain-exchange-floor/PROOF.md

@@ -0,0 +1,94 @@
+# Exact minimum of the G20 chain/exchange component
+
+## Model
+
+Work over F2 on the 32 boundary wires of PR5840. A state is a list of rows:
+row `w` is the set of input coordinates currently held on wire `w`. An ADD is
+`x_d <- x_d + x_s` with `d != s`, cost one. No scratch, reset, copy or free
+relabelling of wires is allowed. A word implements a target when it maps the
+identity rows to the target rows exactly.
+
+## The component
+
+Replaying the authenticated PR5840 `left_program` gives `left_rows`. Wires
+`0..15, 30, 31` form a closed set: their rows read only those coordinates and
+no other wire reads them. The source word spends fourteen chain ADDs and two
+three-ADD exchanges (`SWAP 15 30`, `SWAP 14 31`) there: **20 ADDs**. The other
+fourteen wires carry the three isolated four-wire bank exchanges covered by
+#5850/#5851 and two untouched wires.
+
+The 18-register component splits again into two closed 9-wire parts:
+
+```
+even  wires 0,2,...,12 : x_{2i}  = e_{2i} + e_{2i+2}      (i = 0..6)
+      wire 14          : e_31
+      wire 31          : e_14
+odd   wire 1           : e_1
+      wires 3,...,13   : x_{2i+1} = e_1 + e_3 + ... + e_{2i+1}
+      wire 15          : e_30
+      wire 30          : e_1 + e_3 + ... + e_13 + e_15
+```
+
+The source spends ten ADDs on each part.
+
+## Statement
+
+1. Every word on the nine even wires implementing the even part has at least
+   10 ADDs. The same holds for the odd part.
+2. Every word on all eighteen component wires implementing the component,
+   including words whose ADDs cross between the even and odd parts, has at
+   least 20 ADDs.
+3. The right boundary is the reverse of the left word and the exact inverse
+   map, so it has the same minimum. Each component side is exactly 20.
+
+## Hand proof of the even bound
+
+All nine even rows differ from the identity, so each even wire is a
+destination at least once. A nine-ADD word therefore updates each wire exactly
+once, and that update must produce its final row. A chain wire `2i` holds
+`e_{2i}` before its update and its final row after it, so it never holds a
+coordinate `e_31`. Suppose wire 14 is updated first among 14 and 31. Its
+source must hold `e_14 + e_31`; wire 31 still holds `e_31`, and no chain wire
+holds `e_31`. If wire 31 is updated first, its source must also hold
+`e_14 + e_31`; wire 14 still holds `e_14`. Either case is impossible.
+
+## Computer proof of all three bounds
+
+`verify.py` runs an exhaustive depth-first search for each budget from zero up
+to the source cost. It prunes a state only by two admissible bounds:
+
+- each row of the state that differs from the target needs one more ADD;
+- the remaining map `R = target * state^-1` needs at least as many ADDs as it
+  has non-unit columns. The reversed word of transposed ADDs implements `R^T`
+  with the same length, and the row bound applies to `R^T`.
+
+The search tracks `R^T` incrementally: the state step `x_a += x_c` changes
+`R^T` row `c` to `R^T[c] + R^T[a]`. A memo records the largest failed budget
+for each state, which is sound because failure at budget `b` implies failure
+at every smaller budget. Every ADD of the restricted wire set is tried at each
+node, so no ordering or normal form is assumed. A search that exceeds its node
+limit fails the check instead of reporting a bound.
+
+The first feasible budget is the minimum. Its witness word is replayed as rows
+and on every Boolean input of the wires. Four controls must behave as known:
+the chain alone needs exactly 14, a weakened even target fits in nine, and a
+two-wire exchange needs exactly three.
+
+## Consequence for the source boundary
+
+Within the stated model, a side of the PR5840 boundary cannot gain by
+resynthesising the chain together with the bank 7/15 exchange, or by mixing
+even and odd chain wires, as long as the gates stay on these 18 wires.
+Adding the component-local six-ADD floor of the other three exchanges
+(#5850/#5851) gives 20 + 18 = 38 per side and 76 per port. This is still a
+component-local statement: gates linking the 18 wires to the exchange wires or
+to the two untouched wires are not covered, so no global 32-wire minimum is
+proved.
+
+## Not covered
+
+General GL2 bases inside equal-target pairs (pairs `(2k, 2k+1)` mix the even
+and odd parts and change the target), scratch or helper wires, gates leaving
+the component, changed controllers, nonunit tariffs, and any recursive,
+physical, compiler or precision cost. The paid recursive profile is unchanged
+and kappa is unchanged.

research/g20-chain-exchange-floor/README.md

@@ -0,0 +1,99 @@
+# G20 chain/exchange component: exact 20-ADD minimum
+
+**Scoped negative result; no new kappa.** The remaining 18-register component
+of the PR5840 G20 boundary (wires 0-15, 30, 31: fourteen chain ADDs plus the
+bank 7/15 exchange) needs exactly **20 unit ADDs per side**, even when gates
+may mix chain and exchange operations anywhere on those 18 wires. The source
+attains 20. The component splits into two closed 9-wire parts, and each needs
+exactly 10.
+
+This answers, inside the component, the question that
+[#5850](https://github.com/CrocSwap/integer-mult-bounds/pull/5850) leaves open
+("the remaining 18-register component ... may permit a cheaper complete
+boundary") and the joint chain/exchange question of
+[#5851](https://github.com/CrocSwap/integer-mult-bounds/pull/5851). With their
+component-local six-ADD exchange floor, 20 + 3 x 6 = 38 per side and 76 per
+port stay optimal for synthesis that keeps gates inside each component.
+
+Claim type: finite exhaustive certificate (a computer proof), with a written
+model and a hand proof of the even 9-wire bound in [PROOF.md](PROOF.md). It is
+not a 32-wire global minimum, a search failure, a new kappa or a complete
+multiplication theorem.
+
+## Result
+
+| Target (scratch-free, unit ADDs) | Wires | Source cost | Exact minimum |
+|---|---:|---:|---:|
+| even part: chain on 0,2,...,12 with exchange 14/31 | 9 | 10 | 10 |
+| odd part: prefix chain on 1,3,...,13 with exchange 15/30 | 9 | 10 | 10 |
+| whole component, cross-part gates allowed | 18 | 20 | 20 |
+
+The search excludes every word of at most 19 ADDs on the 18 wires. It visits
+2,016,480 nodes at budget 19 and finds a 20-ADD witness at budget 20.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and only the standard library:
+
+```sh
+python3 -I -W error -B research/g20-chain-exchange-floor/verify.py
+python3 -B scripts/research_package.py --package research/g20-chain-exchange-floor
+```
+
+Expected last line of the direct run:
+`PASS_G20_CHAIN_EXCHANGE_FLOOR component18=20 even9=10 odd9=10 controls=4`.
+Locally a run takes about 35 seconds and 400 MB of memory.
+
+The only live input is the PR5840 controller already vendored by #5851 at
+`research/g20-isolated-exchange-floor/inputs/CONTROLLER.json` (SHA256 pinned in
+[SOURCES.json](SOURCES.json) and checked by the verifier). The verifier replays
+both source programs against the stored rows, checks that the 18 wires are
+closed and that the right boundary is the exact inverse, then runs the search.
+
+## Method
+
+Exhaustive depth-first search for each budget, trying every ADD on the wire
+set at every node. Pruning uses two admissible bounds: rows that still differ
+from the target, and non-unit columns of the remaining map (valid because the
+reversed transposed word has the same length). Failed states are memoized with
+their largest failed budget. A node limit turns an overlong search into a
+failure, never into a bound. Witnesses are replayed on all Boolean inputs.
+Controls: the chain alone needs exactly 14, a weakened even target fits in
+nine, and a two-wire exchange needs exactly three.
+
+## Limits
+
+Not covered: gates linking the component to the other 14 boundary wires,
+general GL2 bases in the equal-target pairs `(2k, 2k+1)` (they mix the two
+parts and change the target), scratch or helpers, a changed controller,
+nonunit tariffs, and every recursive, physical, compiler, precision or analytic
+obligation. The paid recursive profile is unchanged. The selected conditional
+kappa 0.00310045 and its five framework assumptions are unchanged.
+
+## Open next questions
+
+1. Does any scratch-free word on all 32 boundary wires implement one side in
+   fewer than 38 ADDs? This matters because every current floor is
+   component-local. First step: run the same search on the chain component
+   plus one four-wire exchange (22 wires, budget 25). Blocker: search cost
+   grows quickly with wires and slack, so a stronger bound or a written
+   argument is likely needed.
+2. Do GL2 bases inside the equal-target pairs lower the 20-ADD component cost?
+   This matters because pair bases are the freedom PR5840 released. First
+   step: enumerate the pair-basis orbit of the 18-wire target up to
+   cost-preserving symmetries and search the cheapest representatives.
+   Blocker: each basis must also be priced at the caller and checked against
+   the target diagonal.
+
+Structured versions are in [TASK.json](TASK.json).
+
+## Credit
+
+Ali Romman supplied the PR5840 G20 target-pair boundary and its controller.
+Charan . (#5850, #5851) posed the 18-register and joint chain/exchange
+questions and proved the isolated four-wire exchange floor cited above; the
+controller copy vendored by #5851 is the input. Their retained lineage
+(PR5834, PR5807/5828, PR5708/5671, ai-nanachi PR5512, Dugongue, ToikY) is
+recorded in those packages. Budgeted depth-first search and the transpose
+argument are standard; the new work is the component decomposition, the exact
+20-ADD minimum and its verifier, produced by Nick Petalas. Apache-2.0.

research/g20-chain-exchange-floor/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "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"
+    }
+  ]
+}

research/g20-chain-exchange-floor/TASK.json

@@ -0,0 +1,103 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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": "Exact scratch-free unit-ADD minimum of the 18-register chain/exchange component (wires 0-15, 30, 31) of the PR5840 G20 boundary: 20 per side, with both closed 9-wire parts exactly 10. Gates may cross between the parts but stay on the 18 wires.",
+  "scope_change_reason": "The card asks for a changed helper path or independent-target split with a complete BIT moment. This side result instead answers the boundary-synthesis question PR5850 leaves open for the remaining 18-register component, without changing helpers, targets or the recursive profile.",
+  "bottleneck_link": "Closes one proposed scalar route to a cheaper G20 boundary: joint chain/exchange resynthesis on the component wires cannot beat the source. Remaining scalar routes must use gates leaving the component, scratch, GL2 pair bases or a changed controller.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the exact minimum for the 18-wire component (or a shorter witness). Do not enlarge to the full 32-wire boundary.",
+  "outcome": "negative-result",
+  "evidence": "verify.py: exhaustive budgeted search with admissible row/column bounds, witness replay on all Boolean inputs, four controls; PROOF.md gives the model and a hand proof of the even 9-wire bound.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does any scratch-free ADD word on all 32 boundary wires implement a PR5840 boundary side in fewer than 38 ADDs?",
+      "why_it_matters": "This result and PR5850/PR5851 are component-local; gates linking the chain component to the exchange or untouched wires are not covered.",
+      "first_step": "Extend the same budgeted search to the chain component plus one four-wire exchange (22 wires, budget 25) before attempting all 32 wires.",
+      "blocked_by": "Search cost grows quickly with wires and slack; a stronger admissible bound or a written argument is needed."
+    },
+    {
+      "question": "Do general GL2 bases inside the equal-target pairs (2k, 2k+1) of the chain component lower its 20-ADD cost?",
+      "why_it_matters": "Pair bases mix the even and odd 9-wire parts and change the target map, so this exact minimum does not cover them.",
+      "first_step": "Enumerate the pair-basis orbit of the 18-wire target modulo the bases that leave the cost unchanged and search the cheapest representatives.",
+      "blocked_by": "Each basis change must also be priced at the caller and checked against the target diagonal."
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 5850,
+      "author": "Charan .",
+      "path": "research/g20-gl2-tail-floor",
+      "relationship": "Poses the open 18-register component question; its four-wire exchange floor is cited for the 38-per-side total."
+    },
+    {
+      "pr": 5851,
+      "author": "Charan .",
+      "path": "research/g20-isolated-exchange-floor",
+      "relationship": "Its vendored PR5840 controller is the live input; its isolated-exchange floor is cited, not replayed."
+    },
+    {
+      "pr": 5840,
+      "author": "Ali Romman",
+      "relationship": "G20 target-pair boundary construction whose left/right programs are the object studied."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19219123"
+}

research/g20-chain-exchange-floor/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "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": 300,
+      "checks": "Source replay and component closure, exhaustive budgeted exclusion of words of at most 19 ADDs on the 18-wire component (9 for each 9-wire part), witness replay on all Boolean inputs, four controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Same exact exclusion and controls with assertions disabled; all checks use explicit exceptions."
+    }
+  ]
+}