Prove the exact 38-ADD floor for the full fixed G20 boundary

research/g20-full-boundary-floor/README.md

@@ -0,0 +1,83 @@
+# The full fixed G20 boundary needs exactly 38 ADDs
+
+**Scoped source-bound proof; no new kappa.** Each exact 32-wire boundary of
+Ali Romman's PR5840 needs exactly 38 unit binary ADDs, even when intermediate
+ADDs connect different endpoint components or the two untouched wires.
+This closes the fixed-endpoint question explicitly left by PR6081
+`2f258ab31a018b069d77449a148fe80727a6b9a1`,
+`research/g20-joint-exchange-floor/README.md`, Open next questions.
+
+## Contract and proof
+
+The live input is PR5840's controller, retained by Charan ./PR5851 in
+`research/g20-isolated-exchange-floor/inputs/CONTROLLER.json` and pinned in
+SOURCES.json. Work over F2 with 32 independent input wires, unit gates
+`x_d <- x_d + x_s`, d != s, fixed physical labels and the literal source
+endpoint. Gates may connect any two of the 32 wires. No extra scratch, resets,
+free basis changes or relabelling are allowed.
+
+We use the connectivity/diagonal bound of Alan Bu, Evan Fan and Robert Joo,
+*Minimum Synthesis Cost of CNOT Circuits*, arXiv:2408.07898v1, Lemma 3.6 and
+Theorem 5.2, also used by PR6081. Here is its counting proof. Build the
+undirected interaction graph of all gates seen so far. Each current row is
+supported inside its interaction component. A gate joining separate components
+therefore adds a source row with zero coefficient on the destination's own
+original input: such a join cannot change any diagonal entry. Every other gate
+changes at most one diagonal entry. If the endpoint has z zero diagonals,
+at least z non-join gates are necessary. If the endpoint's undirected support
+graph has v components, the interaction graph has at most v components, so
+at least n-v joins are necessary. These are disjoint gate classes, hence
+L >= n-v+z. This reasoning permits arbitrary intermediate cross-component gates.
+
+For **both** source endpoints, the exact support components are:
+
+- `(0,2,4,6,8,10,12,14,31)` and `(1,3,5,7,9,11,13,15,30)`;
+- `(16,28)`, `(17,29)`, `(18,26)`, `(19,27)`, `(20,24)`, `(21,25)`;
+- `(22)` and `(23)`.
+
+Thus n=32 and v=10. The zero diagonal indices are 14 through 21 and 24
+through 31, so z=16. The bound is **32-10+16=38**. The source contains eight
+SWAPs and fourteen ADDs. Expanding each SWAP into three ADDs gives a literal
+38-gate witness for each side. The two endpoints are inverse maps. This proves
+exact minimality for each fixed boundary; it does not add separate
+component-local lower bounds.
+
+## Evidence and reproduction
+
+```
+python3.12 -B scripts/research_package.py --package research/g20-full-boundary-floor
+```
+
+The registered normal and optimized checks authenticate source hashes, replay
+both literal programs and compare their serialized endpoint rows, compute the
+support partition by two algorithms, check every input column separately,
+verify the inverse composition, and reject all 76 single-gate omissions.
+Identity, ADD, swap and unused-wire controls check the bound's conventions.
+The universal lower bound follows from the proof, not finite testing.
+
+## Open next questions
+
+This closes fixed physical endpoints, including gates through wires 22 and 23.
+It does not cover basis changes that alter the chain endpoint, additional
+scratch, nonlinear gates, nonunit tariffs, joint supplier/caller optimization,
+or physical/compiler admission. No recursive paid ranks or selected result
+change. General GL2 choices affecting the chain still require a newly stated
+endpoint family and its complete invoice. A useful first step is to identify
+which such choices are actually legal for the source consumer before trying to
+minimize their graph bound. An arbitrary matrix-family census is not admission.
+No predecessor exhaustive circuit search or selected scientific replay was run.
+
+## Provenance and credit
+
+Canonical base 721c03822c421b7f7fcbb2598993b947c4d88419, priority revision 8.
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5804#discussioncomment-19234839).
+This changes the generic BIT card to the actual full G20 boundary obligation.
+Credit Ali Romman/PR5840 (`6a043d0fc0199ee5b24c61f883f1943eaf6424be`) and retained
+G20/native/controller lineage; Charan ./PR5851; Nick Petalas/PR5942 for the
+18-wire component result; JoyboyBrian/PR6081 for the twelve-wire joint result
+and explicit full-boundary question; Bu, Fan and Joo for the general bound.
+PR6081 is context, not an executable or theorem dependency: the argument is
+included above. Original source bytes remain unchanged. Prepared by
+JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. No independent
+human review, formal-kernel acceptance or complete multiplication theorem is
+claimed.

research/g20-full-boundary-floor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/inputs/CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "73fa9f40a032f11dabf357eba69066fcf9bf0a02",
+      "sha256": "978536e852c0cfbc150f143e19d2cfddbb434bac6017d914974eb99f641593a8"
+    }
+  ]
+}

research/g20-full-boundary-floor/TASK.json

@@ -0,0 +1,64 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact 38-ADD minimum for each fixed full 32-wire PR5840 boundary with unrestricted cross-component gates.",
+  "scope_change_reason": "Explicit PR6081 open question extends the source-bound 12-wire result to the complete fixed boundary.",
+  "bottleneck_link": "Closes the scalar conversion resynthesis obligation; no recursive saving or supplier admission.",
+  "budget_minutes": 20,
+  "stop_rule": "Compute graph bound first; stop rather than run a large synthesis search if it falls short.",
+  "outcome": "completed",
+  "evidence": "Source-bound written lower bound 32-10+16=38, literal 38-gate witnesses, normal/optimized registered checks.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "Which chain-changing GL2 bases are legal for the actual G20 consumer, and can they lower the complete conversion invoice?",
+      "why_it_matters": "The fixed-endpoint optimum does not exclude changed endpoints.",
+      "first_step": "Derive the legal basis/target compatibility conditions from the source consumer before evaluating graph bounds.",
+      "blocked_by": "Complete endpoint family and paid conversion contract have not been established here."
+    }
+  ]
+}

research/g20-full-boundary-floor/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/g20-chain-exchange-floor/PROOF.md",
+    "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 20,
+      "checks": "Exact endpoint, independent support partitions, source pins and omission controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 20,
+      "checks": "Same explicit checks with Python assertions disabled"
+    }
+  ]
+}

research/g20-full-boundary-floor/verify.py

@@ -0,0 +1,95 @@
+#!/usr/bin/env python3
+"""Authenticate and check the exact full G20 boundary; no circuit search."""
+from hashlib import sha256
+import json
+from pathlib import Path
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+
+
+def require(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def apply(word, n):
+    rows = [1 << i for i in range(n)]
+    for d, s in word:
+        require(0 <= d < n and 0 <= s < n and d != s, 'invalid ADD')
+        rows[d] ^= rows[s]
+    return rows
+
+
+def partition(rows):
+    unseen = set(range(len(rows)))
+    parts = []
+    while unseen:
+        todo = [unseen.pop()]
+        part = []
+        while todo:
+            i = todo.pop()
+            part.append(i)
+            neighbors = {j for j in unseen if ((rows[i] >> j) | (rows[j] >> i)) & 1}
+            unseen -= neighbors
+            todo.extend(neighbors)
+        parts.append(sorted(part))
+    return sorted(parts)
+
+
+def independent_component_count(rows):
+    labels = list(range(len(rows)))
+    for i, row in enumerate(rows):
+        for j in range(len(rows)):
+            if row >> j & 1:
+                a, b = labels[i], labels[j]
+                labels = [a if label == b else label for label in labels]
+    return len(set(labels))
+
+
+def bound(rows):
+    return len(rows) - len(partition(rows)) + sum(not (row >> i & 1) for i, row in enumerate(rows))
+
+
+def main():
+    manifest = json.loads((PACKAGE / 'SOURCES.json').read_text())
+    for item in manifest['files']:
+        if item['usage'] == 'input':
+            require(sha256((ROOT / item['path']).read_bytes()).hexdigest() == item['sha256'], 'source mismatch')
+    source = json.loads((ROOT / 'research/g20-isolated-exchange-floor/inputs/CONTROLLER.json').read_text())['boundaries']
+    expected = [list(range(0, 16, 2)) + [31], list(range(1, 16, 2)) + [30], [16, 28], [17, 29], [18, 26], [19, 27], [20, 24], [21, 25], [22], [23]]
+    words = {}
+    rejected = 0
+    for side in ('left', 'right'):
+        word = []
+        for op, a, b in source[side + '_program']:
+            require(op in ('ADD', 'SWAP'), 'unknown opcode')
+            word.extend([(a, b)] if op == 'ADD' else [(a, b), (b, a), (a, b)])
+        words[side] = word
+        rows = apply(word, 32)
+        require(rows == source[side + '_rows'], 'literal endpoint mismatch')
+        require(partition(rows) == expected, 'support partition mismatch')
+        require(independent_component_count(rows) == 10, 'independent partition mismatch')
+        zero_diagonal = [i for i, row in enumerate(rows) if not (row >> i & 1)]
+        require(zero_diagonal == list(range(14, 22)) + list(range(24, 32)), 'diagonal mismatch')
+        require(bound(rows) == len(word) == 38, 'sharpness mismatch')
+        for k in range(len(word)):
+            require(apply(word[:k] + word[k + 1:], 32) != rows, 'omission admitted')
+            rejected += 1
+        # Independently execute each source input column as individual bits.
+        for column in range(32):
+            state = [int(i == column) for i in range(32)]
+            for d, s in word:
+                state[d] ^= state[s]
+            require(state == [(row >> column) & 1 for row in rows], 'column mismatch')
+        print(side, 'n=32 components=10 zero_diagonal=16 lower=38 witness=38')
+    require(apply(words['left'] + words['right'], 32) == [1 << i for i in range(32)], 'inverse mismatch')
+    require(bound([1 << i for i in range(32)]) == 0, 'identity control')
+    require(bound([2, 1]) == 3, 'swap control')
+    require(bound([3, 2]) == 1, 'ADD control')
+    require(bound([2, 1, 4]) == 3, 'untouched-wire control')
+    print('PASS_G20_FULL_BOUNDARY_FLOOR sides=2 floor=38 omitted_gates_rejected=' + str(rejected))
+
+
+if __name__ == '__main__':
+    main()