From 2f258ab31a018b069d77449a148fe80727a6b9a1 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:09:17 -0700 Subject: [PATCH] Prove source-bound joint G20 exchange floor with attributed connectivity bound --- research/g20-joint-exchange-floor/README.md | 106 +++++++++++ .../g20-joint-exchange-floor/SOURCES.json | 51 +++++ research/g20-joint-exchange-floor/TASK.json | 77 ++++++++ research/g20-joint-exchange-floor/VERIFY.json | 38 ++++ research/g20-joint-exchange-floor/verify.py | 176 ++++++++++++++++++ 5 files changed, 448 insertions(+) create mode 100644 research/g20-joint-exchange-floor/README.md create mode 100644 research/g20-joint-exchange-floor/SOURCES.json create mode 100644 research/g20-joint-exchange-floor/TASK.json create mode 100644 research/g20-joint-exchange-floor/VERIFY.json create mode 100644 research/g20-joint-exchange-floor/verify.py diff --git a/research/g20-joint-exchange-floor/README.md b/research/g20-joint-exchange-floor/README.md new file mode 100644 index 0000000000..9adba57d63 --- /dev/null +++ b/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. diff --git a/research/g20-joint-exchange-floor/SOURCES.json b/research/g20-joint-exchange-floor/SOURCES.json new file mode 100644 index 0000000000..d047be33c3 --- /dev/null +++ b/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." + } +} diff --git a/research/g20-joint-exchange-floor/TASK.json b/research/g20-joint-exchange-floor/TASK.json new file mode 100644 index 0000000000..3d14ab6d95 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/g20-joint-exchange-floor/VERIFY.json b/research/g20-joint-exchange-floor/VERIFY.json new file mode 100644 index 0000000000..4a20ec004f --- /dev/null +++ b/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" + } + ] +} diff --git a/research/g20-joint-exchange-floor/verify.py b/research/g20-joint-exchange-floor/verify.py new file mode 100644 index 0000000000..dd73a6d42e --- /dev/null +++ b/research/g20-joint-exchange-floor/verify.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +"""Source-bound exchange floor; exact finite corroboration, stdlib only.""" +from collections import Counter, deque +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +BLOCKS = ((16, 17, 28, 29), (18, 19, 26, 27), (20, 21, 24, 25)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def components(rows): + """Undirected support components, using a disjoint-set forest.""" + parent = list(range(len(rows))) + def root(x): + while parent[x] != x: + x = parent[x] + return x + for i, row in enumerate(rows): + for j in range(len(rows)): + if row >> j & 1: + parent[root(i)] = root(j) + return len({root(i) for i in range(len(rows))}) + + +def independent_components(rows): + """Separate adjacency-set traversal.""" + unseen = set(range(len(rows))) + count = 0 + while unseen: + stack = [unseen.pop()] + count += 1 + while stack: + i = stack.pop() + neighbors = {j for j in unseen if (rows[i] >> j | rows[j] >> i) & 1} + unseen -= neighbors + stack.extend(neighbors) + return count + + +def floor(rows): + return len(rows) - components(rows) + sum(not (row >> i & 1) for i, row in enumerate(rows)) + + +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 tuple(rows) + + +def apply_input(word, value): + for d, s in word: + value ^= ((value >> s) & 1) << d + return value + + +def block_maps(): + gl2 = [(a, b) for a in range(1, 4) for b in range(1, 4) if a != b] + return [tuple((a[0] << 2, a[1] << 2, b[0], b[1])) for a, b in product(gl2, repeat=2)] + + +def sum_blocks(blocks): + return tuple(row << (4 * k) for k, block in enumerate(blocks) for row in block) + + +def swap_word(pairs): + return tuple(gate for a, b in pairs for gate in ((a, b), (b, a), (a, b))) + + +def check_sources(): + manifest = json.loads((PACKAGE / 'SOURCES.json').read_text()) + for item in manifest['files']: + if item.get('usage') == 'input': + require(sha256((ROOT / item['path']).read_bytes()).hexdigest() == item['sha256'], 'source mismatch') + return json.loads((ROOT / 'research/g20-isolated-exchange-floor/inputs/CONTROLLER.json').read_text()) + + +def source_endpoint(controller): + wires = tuple(w for block in BLOCKS for w in block) + require(len(set(wires)) == 12, 'repeated wire') + index = {wire: i for i, wire in enumerate(wires)} + expected = sum_blocks([(4, 8, 1, 2)] * 3) + for side in ('left', 'right'): + pairs = [] + for op, a, b in controller['boundaries'][side + '_program']: + if a not in index and b not in index: + continue + require(a in index and b in index and op == 'SWAP', 'source component is not isolated swaps') + pairs.append((index[a], index[b])) + require(len(pairs) == 6, 'source swap count') + require(apply(swap_word(pairs), 12) == expected, 'source word endpoint') + full = controller['boundaries'][side + '_rows'] + projected = [] + mask = sum(1 << w for w in wires) + for wire in wires: + require(full[wire] & ~mask == 0, 'outside source coefficient') + projected.append(sum(((full[wire] >> w) & 1) << i for i, w in enumerate(wires))) + require(tuple(projected) == expected, 'source matrix endpoint') + return expected + + +def finite_lemma_check(): + identity = (1, 2, 4) + distances = {identity: 0} + queue = deque([identity]) + edges = 0 + while queue: + rows = queue.popleft() + for d in range(3): + for s in range(3): + if d == s: + continue + nxt = list(rows) + nxt[d] ^= nxt[s] + nxt = tuple(nxt) + require(abs(components(nxt) - components(rows)) <= 1, 'component step') + if components(nxt) < components(rows): + require(tuple((row >> i) & 1 for i, row in enumerate(nxt)) == + tuple((row >> i) & 1 for i, row in enumerate(rows)), 'link changes diagonal') + require(floor(nxt) <= floor(rows) + 1, 'bound step') + edges += 1 + if nxt not in distances: + distances[nxt] = distances[rows] + 1 + queue.append(nxt) + require(len(distances) == 168 and edges == 1008, 'GL3 coverage') + require(all(floor(rows) <= distance for rows, distance in distances.items()), 'distance lower bound') + return edges + + +def main(): + source = source_endpoint(check_sources()) + maps = block_maps() + require(len(set(maps)) == 36, 'local endpoint inventory') + hist = Counter() + witnesses = 0 + for blocks in product(maps, repeat=3): + rows = sum_blocks(blocks) + count = independent_components(rows) + require(count == sum(components(block) for block in blocks), 'direct-sum graph count') + require(all(not (row >> i & 1) for i, row in enumerate(rows)), 'endpoint diagonal') + lower = 24 - count + require(lower >= 18, 'exchange floor') + hist[lower] += 1 + if lower == 18: + require(all(row.bit_count() == 1 for row in rows), 'equality is not a permutation') + pairs = [(i, row.bit_length() - 1) for i, row in enumerate(rows) if i < row.bit_length() - 1] + word = swap_word(pairs) + require(len(word) == 18 and apply(word, 12) == rows, 'attaining word') + for i in range(12): + expected = sum(((row >> i) & 1) << j for j, row in enumerate(rows)) + require(apply_input(word, 1 << i) == expected, 'independent arbitrary-input column') + require(apply_input(tuple(reversed(word)), expected) == 1 << i, 'inverse column') + witnesses += 1 + require(dict(hist) == {18: 8, 19: 408, 20: 6936, 21: 39304}, 'floor histogram') + require(witnesses == 8 and floor(source) == 18, 'sharp source floor') + edges = finite_lemma_check() + # Controls distinguish the restricted endpoint family and a real gate defect. + word = swap_word([(i, i + 2) for i in (0, 1, 4, 5, 8, 9)]) + require(all(apply(word[:i] + word[i + 1:], 12) != source for i in range(18)), 'omission control') + require(floor(tuple(1 << i for i in range(12))) == 0, 'identity control') + mixed = sum_blocks([maps[0], maps[0], next(m for m in maps if components(m) == 1)]) + require(floor(mixed) > 18, 'nonmatching-bank control') + print('PASS_G20_JOINT_EXCHANGE_FLOOR maps=46656 floor=18 attaining=8 GL3_edges=' + str(edges) + ' no_new_kappa') + + +if __name__ == '__main__': + main()