diff --git a/research/g20-full-boundary-floor/README.md b/research/g20-full-boundary-floor/README.md new file mode 100644 index 0000000000..f3c067180b --- /dev/null +++ b/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. diff --git a/research/g20-full-boundary-floor/SOURCES.json b/research/g20-full-boundary-floor/SOURCES.json new file mode 100644 index 0000000000..ce3c296c3e --- /dev/null +++ b/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" + } + ] +} diff --git a/research/g20-full-boundary-floor/TASK.json b/research/g20-full-boundary-floor/TASK.json new file mode 100644 index 0000000000..fc37517945 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/g20-full-boundary-floor/VERIFY.json b/research/g20-full-boundary-floor/VERIFY.json new file mode 100644 index 0000000000..072f4b8690 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/g20-full-boundary-floor/verify.py b/research/g20-full-boundary-floor/verify.py new file mode 100644 index 0000000000..90a84324b2 --- /dev/null +++ b/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()