Prove the joint G20 exchange floor: 18 ADDs even with cross-component gates

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

@@ -0,0 +1,106 @@
+# Three G20 exchanges still need 18 ADDs under joint synthesis
+
+**Source-bound application of a known lower bound; no new kappa.** Arbitrary
+cross-component ADDs cannot lower the three PR5840 bank exchanges below
+18 unit ADDs per boundary side, even after allowing independent invertible
+binary bases within each two-wire bank. Exactly eight of the 46,656 allowed
+endpoint maps attain 18; every other map needs at least 19. This closes the
+specific direct-sum question in [the released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19230486).
+
+The lower-bound technique is **Bu, Fan and Joo**, [Minimum Synthesis Cost of
+CNOT Circuits, arXiv:2408.07898](https://arxiv.org/abs/2408.07898), Lemma 3.6
+and Theorem 5.2. We claim its source-bound application, endpoint census and
+sharp witnesses, not a new general CNOT bound. The proof below is self-contained;
+no external paper download or executable is needed for replay.
+
+## Exact contract and proof
+
+The source is Ali Romman's PR5840 at
+`6a043d0fc0199ee5b24c61f883f1943eaf6424be`, its controller retained unchanged
+by PR5851. The three bank exchanges are `(8,14)`, `(9,13)`, `(10,12)`:
+physical wires `(16,17,28,29)`, `(18,19,26,27)`, `(20,21,24,25)`.
+Each bank pair has endpoint `[[0,A],[B,0]]`, with `A,B in GL(2,F2)`.
+All twelve inputs are independent; every ADD costs one, including any operation
+implementing a basis choice. Gates may connect any of these twelve wires.
+There is no scratch, reset or free physical permutation.
+
+For completeness, count two disjoint sorts of gates. Build the undirected
+interaction graph by adding each gate's source/destination edge as the word
+runs. A gate joining two previously separate components is a join. Every row
+of the current linear map has support within its interaction component.
+Thus a join adds a source row with zero coefficient at the destination's own
+input coordinate: it cannot alter a diagonal entry. Any other gate alters at
+most one diagonal entry. If the final map has `z` zero diagonal entries, it
+therefore requires at least `z` non-join gates. If its undirected support graph
+has `v` components, the final interaction graph has at most `v` components,
+so at least `n-v` joins occurred. Consequently every word has length
+`L >= n-v+z`. This is the cited link/diagonal bound, with monotone interaction
+components used for the counting proof.
+
+Every allowed endpoint here has `n=z=12`. Its support graph has no singleton:
+a singleton would have an all-zero row because its diagonal is zero, contrary
+to invertibility. Hence `v<=6` and `L>=18`. Cross-component gates do not evade
+this argument. If `L=18`, then `v=6`, so all support components have two
+vertices. Invertibility and the zero diagonal force each such component to
+be an ordinary swap. Within a bank pair only the straight and crossed
+matchings qualify; there are `2^3=8` global endpoints. Each is attained by six
+three-ADD swaps. For every other endpoint `v<=5`, proving `L>=19`.
+
+The exact graph-bound histogram is `{18:8, 19:408, 20:6936, 21:39304}`.
+The entries above 18 are **lower bounds**, not asserted exact distances.
+The source has the straight matching in each block, so both its boundary and
+inverse cost exactly 18 on these twelve wires, or 36 together per port.
+For 111 independent ports this subtotal is 3,996 ADDs under the source's
+per-port tariff. No vectorized cross-port optimality is asserted.
+
+## Evidence and reproduction
+
+```sh
+python3 -I -W error -B research/g20-joint-exchange-floor/verify.py
+python3 -I -O -W error -B research/g20-joint-exchange-floor/verify.py
+python3.12 -B scripts/research_package.py --package research/g20-joint-exchange-floor
+```
+
+Expected: `PASS_G20_JOINT_EXCHANGE_FLOOR maps=46656 floor=18 attaining=8
+GL3_edges=1008 no_new_kappa`. Standard library only; no search on twelve-wire
+circuits. The verifier checks source hashes, literal source words and serialized
+rows, every allowed endpoint with two separate graph algorithms, all eight
+18-ADD witnesses and inverse actions on every independent input column.
+It also checks all 168 GL(3,2) matrices and 1,008 ADD edges against the graph
+bound, plus gate-omission, identity and nonmatching-bank controls. Finite checks
+corroborate the written argument; they are not its universal proof.
+
+## Limits
+
+The 18-wire chain/exchange component remains excluded. PR5942's component-local
+20-ADD floor cannot simply be added to this 18-ADD floor when gates may mix
+those two larger components. Thus no 32-wire optimum, new paid-rank saving,
+native admission, changed supplier or kappa follows. All five selected
+framework assumptions remain. General GL2 bases affecting the chain, scratch,
+changed controllers and nonunit tariffs remain outside this task.
+
+## Open next questions
+
+The next useful question is whether the exact 32-wire boundary admits fewer
+than 38 ADDs when gates mix the chain and these exchanges. First compute the
+same endpoint graph bound and identify its shortfall from 38 before expanding
+search; the missing obligation is a bound or constructive word across that cut.
+Structured scope and next steps are in TASK.json.
+
+## Sources and credit
+
+Canonical base `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8,
+selected PR6030 conditional kappa `0.003125804`, unchanged.
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5804#discussioncomment-19233737).
+The overlap snapshot covered 341 open PRs, 5,722 Discussion records and
+8,348 local notes with complete reported coverage on 2026-10-28 at 04:55 UTC;
+unpublished work and full remote closed-PR history remain limitations.
+
+Retain Ali Romman/PR5840 and its G20/native/controller lineage; Charan . /
+PR5851 `c698080add27ea02f62da393f27f05c537558ff8` for the isolated floor;
+Nick Petalas/PR5942 `1f1c37ba713d027fb0c568f0dcfa41c42feaa884` and the explicit
+remaining direct-sum question. Their executable replays are not re-run.
+Bu, Fan and Joo own the general lower-bound method. This source application,
+proof presentation and exact checks were prepared by JoyboyBrian with
+substantial OpenAI Codex assistance. Apache-2.0; no independent human or
+proof-assistant acceptance is claimed.

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

@@ -0,0 +1,51 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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-chain-exchange-floor/PROOF.md",
+      "usage": "input",
+      "git_blob": "3d5f4282f184d5aa90f6b6b14d81792f24e00524",
+      "sha256": "1605a3520b4c2b7442199bc6d06319f439eb7652719543f0ee83e92872c3677a"
+    },
+    {
+      "path": "research/g20-isolated-exchange-floor/PROOF.md",
+      "usage": "input",
+      "git_blob": "05f4803c78a5d0e87c3088c74453b393bfe4c7e9",
+      "sha256": "2b87e4db7c291f934ca1cbd611dfcdf5b4eda1bee110cc870e237499fe01b529"
+    },
+    {
+      "path": "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "73fa9f40a032f11dabf357eba69066fcf9bf0a02",
+      "sha256": "978536e852c0cfbc150f143e19d2cfddbb434bac6017d914974eb99f641593a8"
+    }
+  ],
+  "external_mathematics": {
+    "authors": [
+      "Alan Bu",
+      "Evan Fan",
+      "Robert Joo"
+    ],
+    "title": "Minimum Synthesis Cost of CNOT Circuits",
+    "url": "https://arxiv.org/abs/2408.07898",
+    "version": "arXiv:2408.07898v1, 15 August 2024",
+    "cited_results": [
+      "Lemma 3.6",
+      "Theorem 5.2"
+    ],
+    "usage": "Attribution for general bound; self-contained proof included, no network or external code needed at replay."
+  }
+}

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

@@ -0,0 +1,77 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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": "Apply the attributed link/diagonal lower bound to all 36^3 PR5840 three-exchange endpoint maps, allowing arbitrary cross-component ADDs; prove the sharp 18 floor and equality classification.",
+  "scope_change_reason": "The original card asks for a changed BIT contract. The explicit handoff asks whether joint scalar synthesis of three disconnected bank exchanges can save work; this is a scoped cost decision, not a new helper trajectory.",
+  "bottleneck_link": "Closes one proposed scalar-boundary saving route; does not change paid recursive ranks or the selected supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop with the sharp 12-wire floor and finite corroboration; no global 32-wire search.",
+  "outcome": "negative-result",
+  "evidence": "python3 -B scripts/research_package.py --package research/g20-joint-exchange-floor",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance in research, proof, implementation and checks; no independent human or proof-kernel review.",
+  "open_questions": [
+    {
+      "question": "Can gates mixing the 18-wire chain component with the 12 exchanged wires shorten the full 32-wire boundary below 38 ADDs?",
+      "why_it_matters": "Separate component floors do not imply global additivity.",
+      "first_step": "Evaluate the attributed support/diagonal bound on the exact full source endpoint and identify the remaining gap before synthesis.",
+      "blocked_by": "A proof or concrete word accounting for gates across that cut; no large search is authorized here."
+    }
+  ]
+}

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

@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/g20-chain-exchange-floor/PROOF.md",
+    "research/g20-isolated-exchange-floor/PROOF.md",
+    "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Complete 46,656 endpoint inventory, source binding, independent graph and input checks, sharp witnesses and rejection controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same complete checks with optimization enabled"
+    }
+  ]
+}