From b313bad5735ebaa9e303b9813a29d949917e2c76 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 09:12:59 +0000 Subject: [PATCH] feat(research): cut clean rank-two compilation to ten CNOTs --- research/clean-rank-two-conjugators/PROOF.md | 79 +++++++++ research/clean-rank-two-conjugators/README.md | 107 ++++++++++++ .../clean-rank-two-conjugators/SOURCES.json | 36 ++++ research/clean-rank-two-conjugators/TASK.json | 69 ++++++++ .../clean-rank-two-conjugators/VERIFY.json | 38 ++++ research/clean-rank-two-conjugators/WORD.json | 15 ++ research/clean-rank-two-conjugators/verify.py | 162 ++++++++++++++++++ 7 files changed, 506 insertions(+) create mode 100644 research/clean-rank-two-conjugators/PROOF.md create mode 100644 research/clean-rank-two-conjugators/README.md create mode 100644 research/clean-rank-two-conjugators/SOURCES.json create mode 100644 research/clean-rank-two-conjugators/TASK.json create mode 100644 research/clean-rank-two-conjugators/VERIFY.json create mode 100644 research/clean-rank-two-conjugators/WORD.json create mode 100644 research/clean-rank-two-conjugators/verify.py diff --git a/research/clean-rank-two-conjugators/PROOF.md b/research/clean-rank-two-conjugators/PROOF.md new file mode 100644 index 0000000000..80e3e810f5 --- /dev/null +++ b/research/clean-rank-two-conjugators/PROOF.md @@ -0,0 +1,79 @@ +# Shared conjugators for a rank-two clean operation + +This contribution was produced by Nick Petalas. Apache-2.0. + +Work over any vector space in characteristic two and let g be a linear +involution. Put t=1+g, so t squared is zero. All identities below are formal +identities in F2[C2], hence hold without any finite-address assumption. +Each CNOT is one scalar role addition; each G applies g to the helper h. + +Write A1 for `h += c`, A2 for `h += d`, B1 for `a += h`, B2 for `b += h`, +C1 for `a += c` and C2 for `b += d`. Strings in this proof are chronological. +Set A12=A1 A2 and B12=B1 B2; these pairs commute internally. + +JoyboyBrian #5007 constructs the following three idempotents, with role +order a,b,c,d,h: + +```text +x1 = a+h, y1 = d*+h* +x2 = b+h, y2 = c*+h* +x3 = a+b+h, y3 = c*+d*+h* +``` + +Here stars denote coordinate covectors. Their sum is +`a c* + b d* + h h*`. The inherited construction and minimum retain +#5007's credit. Because t squared is zero, the three factors I+t xj yj +commute. Reorder them 1,3,2 and use #5007's literal conjugators: + +```text +B1 A2 G A2 B1 +B12 A12 G A12 B12 +B2 A1 G A1 B2 +``` + +The two boundary scalar strings simplify without moving any reflection: + +```text +A2 B1 B12 A12 = A2 B2 A2 A1 = B2 C2 A1 +A12 B12 B2 A1 = A2 A1 B1 A1 = A2 B1 C1 +``` + +The only noncommuting rewrite is `Ai Bi Ai = Bi Ci`. It follows directly +by applying the three scalar additions to arbitrary inputs. The other +rewrites cancel repeated involutions or commute disjoint-source additions. +The resulting complete stream is + +```text +B1 A2 G B2 C2 A1 G A2 B1 C1 G A1 B2 +``` + +There are ten CNOTs and three G calls. The complete factor product is +`I+t(a c*+b d*+h h*)`. Thus a and b acquire t times c and d, both sources +are restored and the full helper action is `h+t h=g(h)`. A clean zero +helper returns to zero. No data role starts clean, is erased or is discarded. + +For a proof independent of the conjugator notation, put t=1+g and track +the new stream. Immediately after the first G, h is `g(h0+d)` and a is +`a0+h0`. Immediately before the second G, h is `g(h0+d)+c`. Just after it, +h is `h0+d+g(c)` and b is `b0+g(h0)+t d`. Before the third G, h is +`h0+g(c)` and a has become `a0+t c`. The last two scalar additions restore +h to `g(h0)` and b to `b0+t d`. c and d are never destinations. This proves +the full five-input identity directly for any involutory linear g. + +At stationary complete prices the clean bill is `3R+10C+H`. The cited +dirty stream is the separate echo on each pair, + +```text +a += c; c <- g(c); a += c; c <- g(c) +b += d; d <- g(d); b += d; d <- g(d) +``` + +Its bill is `4R+4C`. Its two pieces use disjoint roles, so concatenation +creates no adjacent cancellation; no global scalar lower bound is claimed +for either stream. Subtracting the specified bills gives `-R+6C+H`, +establishing the strict comparison exactly when R>6C+H. The earlier +specified clean stream's sixteen CNOTs gave R>12C+H. Shared conjugators +remove six counted CNOTs while preserving all three reflections and every +input/output obligation. A common data-basis conjugation adds its complete +forward and inverse scalar costs to both bills and does not change this +comparison. No physical caller or primitive price is assumed available. diff --git a/research/clean-rank-two-conjugators/README.md b/research/clean-rank-two-conjugators/README.md new file mode 100644 index 0000000000..39c2c8ed18 --- /dev/null +++ b/research/clean-rank-two-conjugators/README.md @@ -0,0 +1,107 @@ +# Ten CNOTs for the three-reflection rank-two clean compiler + +This contribution was produced by Nick Petalas. + +The rank-two clean square-zero operation has a literal implementation with +three coordinate reflections and **ten scalar CNOTs**, improving the sixteen +CNOTs of JoyboyBrian's merged [#5007](https://github.com/CrocSwap/integer-mult-bounds/pull/5007). +This is a scoped algebraic construction with a written proof and exact finite +corroboration. No scalar-network minimum or new kappa is claimed. + +Let g be any linear involution in characteristic two. Four data roles +`a,b,c,d` are arbitrary and helper `h` starts at zero. The complete action is + +```text +a <- a + c + g(c) b <- b + d + g(d) +c <- c d <- d h <- 0 +``` + +The full five-input action, even when h is dirty, is the displayed data map +and `h <- g(h)`. Thus the clean return is exact; an arbitrary dirty helper +does not satisfy the restored-workspace contract. [WORD.json](WORD.json) +contains all thirteen primitives in chronological order, using role indices +`a,b,c,d,h = 0,1,2,3,4`. Every scalar XOR and inverse operation is included. +[PROOF.md](PROOF.md) derives the new stream by sharing scalar conjugators. + +At complete stationary coordinate-reflection price R, CNOT price C and +additional clean-resource reservation/return charge H, the new local bill is +`3R+10C+H`. The explicitly priced dirty rank-two stream in #5007 costs +`4R+4C`; its two disjoint four-operation pieces have no adjacent cancellations. +The new clean word is cheaper precisely when **R > 6C+H**, improving the +previous specified-word comparison `R > 12C+H`. This compares specified streams, +not globally optimal scalar networks. Common basis transport, if needed, must +be charged equally on both sides. No native R, C or H is supplied. + +## Evidence and reproduction + +From the repository root, CPython 3.12 and its standard library suffice: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/clean-rank-two-conjugators/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/clean-rank-two-conjugators/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clean-rank-two-conjugators +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clean-rank-two-conjugators --check-source-history +``` + +Substitute a local CPython 3.12 path elsewhere. Expected output includes +`PASS_CLEAN_RANK_TWO_CONJUGATORS reflections=3 CNOTs=10 no_new_kappa`. +The read-only verifier generates a receipt bound to every package file and +the cited live inputs. It does not import or execute predecessor code. + +The checker proves the complete five-input formal endpoint in F2[C2] by +coefficient arithmetic. A separate literal bit-array interpreter checks all +1,024 two-address states, including all 256 clean-helper states, and every +basis column for every involutory permutation on one through six addresses. +All thirteen individual primitive omissions and three boundary controls are +checked. These finite domains corroborate the field-uniform written identity; +they do not prove an unbounded statement by enumeration. + +## Scope, overlap and limitations + +This takes Open next question 2 of #5007, a changed compiler-side scope of +`bit-new-register-model`. The change matters because the exact reflection +count alone leaves scalar encoding and restoration costs unpaid. It does not +meet the card's native-supplier acceptance gate. The first verified improvement +is packaged without extending the search to other ranks or claiming optimality. + +Canonical base is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. +The prescribed selected-baseline command passed after its inputs were +materialized in this sparse checkout. It authenticates metadata only. +The initial overlap cache paginated 405 open PRs and 5,290 Discussion records +on October 27, 2026. Sparse local note coverage was incomplete; separate Git +searches covered main's complete README tree, with additional merged-PR +searches and the live #5007/#4912 bodies. No competing shared-conjugator +result was found. Unpublished work, arbitrary diffs and omitted history remain +limits; a no-match search is not a novelty certificate. + +Native reflection implementation, physical routing/frames/tapes/hosting, +the availability and price of the clean function, recursive admission and +the complete multiplication theorem remain unresolved. Lean, Docker, +the selected scientific replay and predecessor executables are unrun. +Independent human and formal proof-kernel review are unclaimed. + +The verifier uses bounded Python-managed allocations, a Power of Ten rule-3 +deviation. Width is fixed at five and address size is at most six. The largest +state enumeration has 1,024 entries; permutation enumeration is at most 720 +per size. Functions are below sixty lines, checks use explicit exceptions +under `-O`, and both registered runs treat warnings as errors. No external +solver, recursion, subprocess or generated code is used. + +## Open next questions + +Can an actual native caller supply the stationary primitive prices and one +returned clean role with `R > 6C+H`? Begin with one literal rank-two caller +and price every data movement, inverse scalar map and clean reservation. +Those native contracts and the complete invoice are the blockers. + +## Credit + +JoyboyBrian #5007 supplies the clean three-projector construction, its exact +reflection-call minimum and the explicit scalar-optimization handoff. +Nick Petalas #4912 supplies the dirty optimum and split compiler. ywz65 +#2716 supplies the involution-product identity and arbitrary-coupling compiler +context. Adam Gall #1911, eumemic #288, Ali Romman #468, woklerx #1443, +Gareth Davidson #1333, Arham Tahir #1589 and Cinna Davis #2290 retain the +register-model lineage credit. The new contribution is the shared-conjugator +ten-CNOT stream and its improved specified-word price comparison. New work +is Apache-2.0. diff --git a/research/clean-rank-two-conjugators/SOURCES.json b/research/clean-rank-two-conjugators/SOURCES.json new file mode 100644 index 0000000000..b1caa2e55d --- /dev/null +++ b/research/clean-rank-two-conjugators/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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/clean-square-zero-compiler/PROOF.md", + "usage": "input", + "git_blob": "3eaec47c2c249f3933d35f9693001b12bca80d42", + "sha256": "5638c02bdd988349fcfd02b6591ae80344c99e01f5f005740e4cea14c806675b" + }, + { + "path": "research/clean-square-zero-compiler/README.md", + "usage": "input", + "git_blob": "7135e70c617678b1d01efd785863640bb8ffa65b", + "sha256": "1e1b231edb1bed1fafb0068cc63988007d92c264ab34f316637b69ede7ad52e7" + }, + { + "path": "research/square-zero-idempotent-compiler/README.md", + "usage": "input", + "git_blob": "1fa5319015c2c79ac6819edf9f4d238fe7295993", + "sha256": "bec1e4187fd70cb9cebc447ec62da0676eda6f27f89aba0bdd1a7b17adce17ff" + } + ] +} diff --git a/research/clean-rank-two-conjugators/TASK.json b/research/clean-rank-two-conjugators/TASK.json new file mode 100644 index 0000000000..b4d44a0bc7 --- /dev/null +++ b/research/clean-rank-two-conjugators/TASK.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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": "Shared scalar conjugators lower the canonical rank-two returned-clean compiler to three coordinate reflections and ten CNOTs.", + "scope_change_reason": "Take JoyboyBrian PR5007 Open next question 2 as a small compiler side result. This prices a specified literal boundary and does not claim a new native supplier.", + "bottleneck_link": "Scalar preparation and restoration costs determine whether saving one reflection survives a complete primitive bill.", + "budget_minutes": 60, + "stop_rule": "Package the first proved lower CNOT count without searching larger ranks or claiming scalar optimality.", + "outcome": "completed", + "evidence": "PROOF.md proves the complete formal identity; verify.py independently checks literal finite address actions and failure controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a literal native caller supply complete prices satisfying R > 6C+H?", + "why_it_matters": "The lower formal scalar bill does not establish native savings or recursive admission.", + "first_step": "Bind one rank-two caller, every data movement and inverse scalar map, and the returned clean resource to stationary complete primitive prices.", + "blocked_by": "Native reflection/CNOT contracts and clean reservation/return price are not supplied." + } + ], + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit" + } +} diff --git a/research/clean-rank-two-conjugators/VERIFY.json b/research/clean-rank-two-conjugators/VERIFY.json new file mode 100644 index 0000000000..d9c7bc824c --- /dev/null +++ b/research/clean-rank-two-conjugators/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/clean-square-zero-compiler/PROOF.md", + "research/clean-square-zero-compiler/README.md", + "research/square-zero-idempotent-compiler/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New complete formal endpoint, all finite literal states and involutions, exact primitive bill and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New complete formal endpoint, all finite literal states and involutions, exact primitive bill and semantic rejection controls." + } + ] +} diff --git a/research/clean-rank-two-conjugators/WORD.json b/research/clean-rank-two-conjugators/WORD.json new file mode 100644 index 0000000000..351885e358 --- /dev/null +++ b/research/clean-rank-two-conjugators/WORD.json @@ -0,0 +1,15 @@ +[ + ["xor", 0, 4], + ["xor", 4, 3], + ["g", 4], + ["xor", 1, 4], + ["xor", 1, 3], + ["xor", 4, 2], + ["g", 4], + ["xor", 4, 3], + ["xor", 0, 4], + ["xor", 0, 2], + ["g", 4], + ["xor", 4, 2], + ["xor", 1, 4] +] diff --git a/research/clean-rank-two-conjugators/verify.py b/research/clean-rank-two-conjugators/verify.py new file mode 100644 index 0000000000..ed30d820a1 --- /dev/null +++ b/research/clean-rank-two-conjugators/verify.py @@ -0,0 +1,162 @@ +"""Exact checks for the new rank-two primitive stream. Apache-2.0.""" + +import hashlib +import itertools +import json +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +ROLES = 5 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def read_word(): + path = PACKAGE / "WORD.json" + need(path.stat().st_size <= 4096, "word size limit") + word = json.loads(path.read_text()) + need(type(word) is list and len(word) == 13, "expected thirteen primitives") + for gate in word: + need(type(gate) is list and gate, "invalid primitive") + need(gate[0] in ("xor", "g"), "unknown primitive") + need(len(gate) == (3 if gate[0] == "xor" else 2), "invalid arity") + need(all(type(i) is int and 0 <= i < ROLES for i in gate[1:]), + "invalid role") + if gate[0] == "xor": + need(gate[1] != gate[2], "self XOR is not invertible") + need(sum(g[0] == "xor" for g in word) == 10, "CNOT invoice") + need(sum(g[0] == "g" for g in word) == 3, "reflection invoice") + return word + + +def formal(word): + # An (identity coefficient, g coefficient) pair of binary input masks. + rows = [(1 << i, 0) for i in range(ROLES)] + for gate in word: + i = gate[1] + a, b = rows[i] + if gate[0] == "g": + rows[i] = (b, a) + else: + c, d = rows[gate[2]] + rows[i] = (a ^ c, b ^ d) + return tuple(rows) + + +def move(value, permutation): + return sum(((value >> i) & 1) << j for i, j in enumerate(permutation)) + + +def literal(word, state, permutation): + # Independent bit-array execution; no formal coefficient operations. + data = [list((row >> j) & 1 for j in range(len(permutation))) for row in state] + for gate in word: + target = gate[1] + if gate[0] == "xor": + source = data[gate[2]] + data[target] = [x ^ y for x, y in zip(data[target], source)] + else: + old = data[target][:] + for i, j in enumerate(permutation): + data[target][j] = old[i] + return tuple(sum(bit << j for j, bit in enumerate(row)) for row in data) + + +def target(state, permutation): + a, b, c, d, h = state + return (a ^ c ^ move(c, permutation), b ^ d ^ move(d, permutation), + c, d, move(h, permutation)) + + +def finite_actions(word): + dense = 0 + for state in itertools.product(range(4), repeat=ROLES): + need(literal(word, state, (1, 0)) == target(state, (1, 0)), + "complete two-address state mismatch") + dense += 1 + involutions, columns = 0, 0 + for size in range(1, 7): + for permutation in itertools.permutations(range(size)): + if any(permutation[permutation[i]] != i for i in range(size)): + continue + involutions += 1 + for role in range(ROLES): + for bit in range(size): + state = tuple((1 << bit) if i == role else 0 for i in range(ROLES)) + need(literal(word, state, permutation) == target(state, permutation), + "involutory-address full basis mismatch") + columns += 1 + return {"dense_two_address_states": dense, "involutions": involutions, + "literal_basis_columns": columns} + + +def controls(word, expected): + omissions = 0 + for i in range(len(word)): + need(formal(word[:i] + word[i + 1:]) != expected, + "primitive omission invisible") + omissions += 1 + need(literal(word, (0, 0, 0, 0, 1), (1, 0)) != (0, 0, 0, 0, 1), + "dirty helper incorrectly restored") + need(any(literal(word, tuple(1 if i == j else 0 for i in range(ROLES)), + (1, 2, 0)) != target(tuple(1 if i == j else 0 for i in range(ROLES)), + (1, 2, 0)) for j in range(ROLES)), + "noninvolutory substitution incorrectly accepted") + wrong_order = word[:] + wrong_order[1], wrong_order[2] = wrong_order[2], wrong_order[1] + need(formal(wrong_order) != expected, "noncommuting order control") + return {"primitive_omissions_rejected": omissions, "boundary_controls": 3} + + +def authenticate(): + path = PACKAGE / "SOURCES.json" + need(path.stat().st_size <= 65536, "source manifest size limit") + sources = json.loads(path.read_text()) + need(type(sources["files"]) is list and len(sources["files"]) <= 16, + "source manifest count limit") + hashes = {} + for source in sources["files"]: + if source["usage"] != "input": + continue + name = source["path"] + path = ROOT / name + need(path.stat().st_size <= 1048576, "source file size limit") + data = path.read_bytes() + digest = hashlib.sha256(data).hexdigest() + blob = hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + need(digest == source["sha256"] and blob == source["git_blob"], + "changed cited source: " + name) + hashes[name] = digest + for name in ("README.md", "PROOF.md", "WORD.json", "verify.py", "TASK.json", + "SOURCES.json", "VERIFY.json"): + path = PACKAGE / name + need(path.stat().st_size <= 1048576, "package file size limit") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return hashes + + +def main(): + need(len(sys.argv) == 1, "verifier takes no arguments") + hashes = authenticate() + word = read_word() + expected = ((5, 4), (10, 8), (4, 0), (8, 0), (0, 16)) + need(formal(word) == expected, "full formal F2[C2] endpoint") + report = finite_actions(word) + report.update(controls(word, expected)) + need(report == {"dense_two_address_states": 1024, "involutions": 119, + "literal_basis_columns": 3215, "primitive_omissions_rejected": 13, + "boundary_controls": 3}, "finite coverage changed") + print(json.dumps({"claim_type": "scoped construction", "scalar_CNOTs": 10, + "coordinate_reflections": 3, "checks": report, + "sha256": hashes}, sort_keys=True)) + print("PASS_CLEAN_RANK_TWO_CONJUGATORS reflections=3 CNOTs=10 no_new_kappa") + + +if __name__ == "__main__": + main()