From 69638b36c691d3e1b8463526fd68c849e8d1aef9 Mon Sep 17 00:00:00 2001 From: commdata2338 <199849969+commdata2338@users.noreply.github.com> Date: Tue, 13 Oct 2026 20:42:15 -0500 Subject: [PATCH] Research: certify nine-call minimum for three coordinate swaps On exactly three registers over the formal F2[GL_2(F2)] model, with free scalar GL_3(F2) mixing and paid coordinate-CNOT calls, three coordinate-SWAP targets need exactly nine calls: complete radius-three/four balls (47,203 and 1,094,640 states) never meet the target, sign-quotient parity excludes even lengths, and a nine-call formal word attains the bound. Two implementations agree. Answers the smallest-register case of PR #1414's three-swap question. No new kappa. Adds research/three-swap-cnot-census/ only. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). --- research/three-swap-cnot-census/EXPECTED.json | 120 ++++++ research/three-swap-cnot-census/OVERLAP.json | 95 +++++ research/three-swap-cnot-census/PROOF.md | 166 ++++++++ research/three-swap-cnot-census/README.md | 165 ++++++++ research/three-swap-cnot-census/SOURCES.json | 58 +++ research/three-swap-cnot-census/TASK.json | 86 +++++ research/three-swap-cnot-census/VERIFY.json | 31 ++ .../three-swap-cnot-census/independent.py | 156 ++++++++ .../three-swap-cnot-census/test_verify.py | 169 +++++++++ research/three-swap-cnot-census/verify.py | 355 ++++++++++++++++++ 10 files changed, 1401 insertions(+) create mode 100644 research/three-swap-cnot-census/EXPECTED.json create mode 100644 research/three-swap-cnot-census/OVERLAP.json create mode 100644 research/three-swap-cnot-census/PROOF.md create mode 100644 research/three-swap-cnot-census/README.md create mode 100644 research/three-swap-cnot-census/SOURCES.json create mode 100644 research/three-swap-cnot-census/TASK.json create mode 100644 research/three-swap-cnot-census/VERIFY.json create mode 100644 research/three-swap-cnot-census/independent.py create mode 100644 research/three-swap-cnot-census/test_verify.py create mode 100644 research/three-swap-cnot-census/verify.py diff --git a/research/three-swap-cnot-census/EXPECTED.json b/research/three-swap-cnot-census/EXPECTED.json new file mode 100644 index 0000000000..d292e052dd --- /dev/null +++ b/research/three-swap-cnot-census/EXPECTED.json @@ -0,0 +1,120 @@ +{ + "active_swaps": 3, + "ball_radius_four": 1094640, + "ball_radius_three": 47203, + "exact_distance_layers": [ + 1, + 56, + 1750, + 45396, + 1047437 + ], + "extra_dirty_registers": 0, + "formal_group_order": [ + [ + 0, + 1, + 2 + ], + [ + 0, + 2, + 1 + ], + [ + 1, + 0, + 2 + ], + [ + 1, + 2, + 0 + ], + [ + 2, + 0, + 1 + ], + [ + 2, + 1, + 0 + ] + ], + "formal_layer_sha256_7byte_little_endian": [ + "ecbddeeab2e0b6f4e4b9005377629d164dc6fd2416662299eb87a63d7206b81a", + "625fac19b641720950a656ef52b7542f38dc1cc979bd776c060e58301c705a47", + "35666ddd0745f0c315360a23fb1365ebbd73f68589b25757e1fcfc93a8a5836e", + "aff97ee994a75a5f6add28466ef05631ec1e5bb6ffa39d5eaa7cc4f09a66a0ca", + "64d641567b5ece05a3b8d7b5943005b4a331a07d9bf3d4da5cd9d0b13d6561f2" + ], + "independent_dense_transition_checks": 101192, + "independent_full_state_sets_equal": true, + "independent_target_intersections": [ + 0, + 0, + 0, + 0 + ], + "minimum_paid_calls": 9, + "paid_generators": 56, + "parity_homomorphism_products": 36, + "permitted_call_count_parity": "odd", + "positive_minimum_controls": [ + 0, + 3, + 6 + ], + "rank_one_idempotents": 28, + "registers": 3, + "regular_layer_sha256_41byte_little_endian": [ + "e8d84774982c75464b6c23c4295e2fcb1a2b4f50fe5681fc04f83cadfc94e1f5", + "f95a4899103e83b66d129cf1f767d88b82a32881578b7d4382c40a069d306099", + "e80f59882043b2842ec04929d8290449b5acc21333ca82417226510419c45186", + "989487d6e30ad7003cd78745c085472f8f5977ca4ad3bd708b0e2faaf7f97b48", + "cd071d15c60df520eac37f4c0f0b73e8583a983f1a6c7034e4dbd1b40dc4e9c4" + ], + "schema_version": 1, + "scope": "Finite certificate: exactly three registers in the stated formal alphabet; no new kappa.", + "semantic_controls": [ + "omit_call_0", + "omit_call_1", + "omit_call_2", + "omit_call_3", + "omit_call_4", + "omit_call_5", + "omit_call_6", + "omit_call_7", + "omit_call_8", + "wrong_label_0", + "wrong_label_1", + "wrong_label_2", + "wrong_label_3", + "wrong_label_4", + "wrong_label_5", + "wrong_label_6", + "wrong_label_7", + "wrong_label_8", + "omit_third_target", + "scalar_residue", + "expanded_address_alphabet", + "nonidempotent_scalar", + "rank_three_underpricing", + "natural_representation_kernel", + "noncommuting_order" + ], + "status": "PASS_THREE_SWAP_CNOT_CENSUS", + "target_intersections_by_left_distance": [ + 0, + 0, + 0, + 0 + ], + "transition_attempts_by_depth": [ + 56, + 3136, + 98000, + 2542176 + ] +} diff --git a/research/three-swap-cnot-census/OVERLAP.json b/research/three-swap-cnot-census/OVERLAP.json new file mode 100644 index 0000000000..0128a65e6e --- /dev/null +++ b/research/three-swap-cnot-census/OVERLAP.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "base_commit": "4040a0f46d67b41c36a472a7cd4af791fd4c36cc", + "queries": [ + [ + "--task", + "bit-helper-contract" + ], + [ + "--task", + "bit-new-register-model" + ], + [ + "three swaps", + "three-SWAP", + "coordinate-CNOT", + "coordinate-cnot-register-bound" + ], + [ + "three swaps", + "three-SWAP", + "three-swap-cnot-census", + "coordinate-CNOT" + ] + ], + "entry_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T01:13:06.664495+00:00", + "records": 828, + "complete_pagination": true + }, + "discussions": { + "fetched_at": "2026-10-14T01:13:30.574789+00:00", + "records": 162, + "complete_pagination": true + } + }, + "latest_checked_coverage": { + "discussions": { + "fetched_at": "2026-10-14T01:24:02.227375+00:00", + "complete_pagination": true, + "records": 169 + }, + "open_prs": { + "fetched_at": "2026-10-14T01:23:37.439709+00:00", + "complete_pagination": true, + "records": 776 + } + }, + "coverage_limit": "Offline shared snapshot. Open PRs include drafts; complete remote pagination is reported. Closed work is covered only by local notes/ledger; code diffs and arbitrary nested source are not searched. No match proves no novelty claim.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912673", + "nearest_prs": [ + { + "number": 1414, + "head": "9e1640094f649ba6db9742796825a8d6c238989b", + "difference": "Two swaps, arbitrary restored dirty-register count; leaves three swaps open. This result is three swaps at exactly r=3." + }, + { + "number": 1333, + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "difference": "All affine rank-one address maps are units; the swap itself is permitted there. Here only the two coordinate CNOTs are paid labels." + }, + { + "number": 720, + "head": "a942c0ae1b463710ca535c1fba1b07b6431b5a86", + "difference": "Arbitrary invertible rational targets in an abelian three-register model, not the present binary nonabelian address algebra." + } + ], + "concurrent_claims": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912406", + "object": "Two central-commutator targets over UT_3(F2), r=2,3.", + "difference": "Different group, target and eight-call baseline." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912696", + "object": "Two coordinate swaps over GL_3(F2), r=2,3, all six address CNOTs.", + "difference": "Different address dimension/alphabet and two targets, rather than three GL2 targets." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912727", + "object": "Two copies of the order-four GL_3(F2) target with rows (2,4,7), r=2.", + "difference": "Different group, target order, register count and eight-call baseline." + } + ], + "other_account_work": "The earlier copy-floor, feedback, hosting, receipt-binding, tape-boundary, Clifford-binding and bit-ledger results have different mathematical objects and are not repeated.", + "source_inspection": "PR1414 and PR1333 inspected by anonymous git fetch; exact heads and text hashes are in SOURCES.json. No pending implementation imported.", + "final_reviewed_at": "2026-10-14T01:31:55.869752+00:00", + "anonymous_head_recheck": { + "main": "92da4d718f1d4cf8de4e6ee947ddc7b180ce1c31", + "1414": "9e1640094f649ba6db9742796825a8d6c238989b", + "1333": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "note": "The two contextual heads are unchanged. Main advanced after the research base was selected; historical provenance remains at the recorded base." + } +} diff --git a/research/three-swap-cnot-census/PROOF.md b/research/three-swap-cnot-census/PROOF.md new file mode 100644 index 0000000000..a34fea8947 --- /dev/null +++ b/research/three-swap-cnot-census/PROOF.md @@ -0,0 +1,166 @@ +# Exact three-register, three-swap minimum + +This is a computer-assisted finite theorem for one explicit register count, +alphabet and endpoint. The enumeration in Section 4 is an essential premise +of its lower bound. It is not an arbitrary-register theorem. + +## 1. Formal model and normalization + +Let `G=GL_2(F2)` and `R=F2[G]`. Group symbols are formal and multiplication +retains their order. With column-vector address convention, put + +```text +a = [[1,1],[0,1]], b = [[1,0],[1,1]], s = aba = bab = [[0,1],[1,0]]. +``` + +The action on the three nonzero binary vectors identifies G with S3. +Registers are three arbitrary R-module inputs. Allowed words are 3x3 +matrices over R generated by free scalar `GL_3(F2)` changes and unit paid +factors + +`D_N(g)=I+([g]+1)N`, with `g in {a,b}`, `N=uv^T`, and `v^Tu=1` over F2. + +Every paid occurrence, including an undo, costs one. There are no other +operations or additional registers. The full formal endpoint is + +`T=diag([s],[s],[s])`. + +Free scalar changes can be moved to the right by conjugating the N matrices. +Conjugation preserves rank one and idempotence. The augmentation homomorphism +`R -> F2`, sending every group element to one, sends each paid factor and T +to I. It therefore forces the remaining scalar factor to be I. Thus it is +enough to enumerate products of paid factors alone. This argument is credited +to PR #1333 and its restricted-alphabet use in PR #1414. + +Every binary rank-one idempotent has the displayed form. There are seven +nonzero choices of u, and exactly four v with `v^Tu=1`; over F2 there is no +nontrivial scaling ambiguity. All **28** projectors, hence all **56** paid +generators, are included. Independently enumerating all 512 binary 3x3 +matrices gives exactly the same projectors. The focused tests check closure +under all 168 scalar invertible matrices (4,704 conjugations). + +Since a and b are involutions, `([g]+1)^2=0` in characteristic two. Scalar +coefficients commute with the group symbols, so `D_N(g)^2=I`. Reversing any +generator word gives its inverse with the same paid length. + +## 2. Parity rules out all even lengths + +The sign homomorphism `G -> C2` sends a, b and s to the nonidentity element t. +Over F2 its group algebra is `F2[epsilon]/(epsilon^2)`, with `t=1+epsilon`. +The induced map sends a normalized product of k paid factors to + +`product_j (I+epsilon N_j) = I+epsilon sum_j N_j`. + +The target maps to `I+epsilon I_3`, so `sum_j N_j=I_3`. Taking traces over +F2 and using `trace(uv^T)=v^Tu=1` gives + +`k mod 2 = trace(I_3) = 1`. + +Consequently a word with fewer than nine calls would have length 1, 3, 5 or +7. The same proof works for any number of restored dirty extras, but the +enumeration below does not. The checker verifies all 36 products in the sign +homomorphism and the projector trace premise. The general sign-trace method +is credited to PR #1414; here its target trace is odd instead of even. + +## 3. Why radius three against radius four is complete + +Let `B_d` be the set of distinct formal matrices expressible using at most +d allowed paid factors, including I. A breadth-first traversal computes +exact-distance layers `L_0={I}` and + +`L_(d+1) = {x f : x in L_d, f a paid generator} minus (L_0 union ... union L_d)`. + +Induction on word length proves completeness. If a word's prefix is already +reachable at a shorter distance, appending its last generator gives a path +no longer than the original, so deduplication cannot remove a required +endpoint. The implementation retains every new state. It applies no +symmetry quotient, heuristic, floating-point pruning or randomized sampling. + +Every word of length at most seven can be split as `p q`, with +`p in B_3` and `q in B_4`. It equals T precisely when `p^-1 T=q`. +The involutive alphabet gives `B_3^-1=B_3`, so + +`a word of length <=7 reaches T` iff `{x T : x in B_3} intersects B_4`. + +The right multiplication by T is an exact permutation of the six coefficients +in every matrix entry. It is not a natural-representation test. The second +implementation computes the corresponding product by generic 18x18 matrix +multiplication. + +## 4. Complete enumeration and independent representation + +The computed exact-distance layer counts at distances 0..4 are + +`1, 56, 1750, 45396, 1047437`. + +At depths 1..4 the numbers of directed transition attempts are + +`56, 3136, 98000, 2542176`. + +Thus `|B_3|=47203` and `|B_4|=1094640`. For each of the four left-distance +layers 0..3 the intersection count is **zero**. This establishes the needed +finite exclusion. Counts, full-layer hashes and independent comparisons are +bound in EXPECTED.json; replay recomputes rather than trusts them. + +The first implementation represents a formal matrix by 54 bits: six formal +coefficients in each of nine entries. It generates G as permutations and +multiplies on the right. Its rank-one update is ordinary matrix multiplication: +for a row m, `m D_N(g) = m + (m u)([g]+1)v^T`. The test suite checks all 56 +optimized maps on a full 54-vector binary basis against unoptimized formal +multiplication, so each optimized linear map agrees on every possible matrix. + +The separate implementation generates G as actual binary 2x2 matrices and +uses its left regular action on the six group elements. A formal scalar +`f=sum_g c_g[g]` acts by `L_f e_h=sum_g c_g e_(gh)`. This representation is +**faithful**: applying L_f to e_1 recovers every c_g. Applying it entrywise +to 3x3 matrices remains faithful, giving binary 18x18 matrices. Hence equality +of these represented matrices is equivalent to formal equality, unlike the +natural two-dimensional address representation. + +The second implementation enumerates all scalar matrices to find projectors, +uses left rather than right generator multiplication, and checks optimized +steps against dense 18x18 multiplication on all 101,192 transitions through +radius three. Left and right breadth-first traversals enumerate the same +word balls. Their complete exact-distance state sets agree through radius +four after conversion. Their target maps and zero intersection counts agree +separately. No shared search engine or predecessor implementation is used. + +The natural representation is deliberately falsified as an equality oracle: +the nonzero formal sum of all six elements of G maps to the zero 2x2 matrix +and has zero augmentation. Adding it to an off-diagonal entry preserves the +natural image of I but changes both the formal and regular matrices. + +## 5. Nine calls attain the complete boundary + +For any idempotent N and any group elements g,h, direct expansion gives + +`D_N(g) D_N(h) = D_N(gh)`. + +Use `a,b,a` on each of `N=E_11,E_22,E_33`. Each triple gives the swap on +one register, with the other two untouched, and their product is T. This is +nine paid calls with no extra register, scalar basis change or restoration +omission. The formal verifier multiplies all nine factors, and rejects every +single omitted factor and every single a/b label swap. + +Sections 2-4 exclude all shorter words; this explicit word supplies the upper +bound. Therefore the minimum is exactly **nine**, for **exactly three registers** +in the stated formal alphabet. + +## 6. Limits and attribution + +The result is exact finite algebra, not a probabilistic rank test or a claim +about arbitrary rational frames. Equality in the formal algebra holds on +every module of that algebra; the address group and register count remain +fixed. A fourth dirty register introduces projectors absent from this census +and is an open case. The result does not prove the same bound for arbitrary +workspace or an enlarged address alphabet. + +The scoped model and research question follow PR #1414, with augmentation +normalization and the broader research direction from Gareth Davidson's +PR #1333. Eumemic, Ali Romman and David Govea receive credit for the rational +register-model lineage. No new general group-algebra or rank principle is +claimed. No Lean build, independent human proof review, physical/compiler +admission, hosting, precision/tape or analytic transfer was performed. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +New work is Apache-2.0. diff --git a/research/three-swap-cnot-census/README.md b/research/three-swap-cnot-census/README.md new file mode 100644 index 0000000000..09353aa519 --- /dev/null +++ b/research/three-swap-cnot-census/README.md @@ -0,0 +1,165 @@ +# Three coordinate swaps need nine paid calls on three registers + +**Finite certificate; no new kappa.** In the formal `F2[GL_2(F2)]` model, +three coordinate-SWAP targets on **exactly three registers** require exactly +nine paid coordinate-CNOT calls, even with arbitrary free scalar `GL_3(F2)` +mixing. The complete boundary is checked for arbitrary inputs. Additional +dirty registers are outside this result. + +This resolves the first open question of this account's +[PR #1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414) for the +smallest register count. That predecessor proves **two** swaps need six calls +for any number of restored dirty registers. Its four-call coefficient proof +does not exclude seven-call words for three swaps. Here a complete new +radius-four census supplies that exclusion; no predecessor implementation is +imported. [PROOF.md](PROOF.md) gives the model, parity argument and coverage +proof. + +## Alphabet, complete bill and result + +Let `a=[[1,1],[0,1]]`, `b=[[1,0],[1,1]]`, and +`s=aba=bab=[[0,1],[1,0]]`. A paid unit is + +`D_N(g) = I + ([g]+1)N`, with `g in {a,b}` and `N=uv^T`, `v^T u=1` over F2. + +There are 28 scalar projectors and 56 paid generators. Free scalar invertible +basis changes are normalized by augmentation, leaving no final scalar residue. +There are no free address maps, copies, erasures, clean allocations or extra +registers. Every undo call costs one. Equality means equality of **all formal +group-algebra coefficients**, not equality in the natural address representation. + +The direct word `aba` on each of the three coordinate projectors has exactly +nine calls and endpoint `diag([s],[s],[s])`. It needs no scalar changes or +additional roles. A shorter word must have odd length: the sign quotient to +`F2[epsilon]/(epsilon^2)` gives `sum N_j=I_3`, whose trace is one. Therefore +excluding all words through seven excludes every possible saving. + +| Exact distance | Distinct formal states | Outgoing attempts used to reach this distance | +| ---: | ---: | ---: | +| 0 | 1 | 0 | +| 1 | 56 | 56 | +| 2 | 1,750 | 3,136 | +| 3 | 45,396 | 98,000 | +| 4 | 1,047,437 | 2,542,176 | + +The radius-three and radius-four balls contain **47,203** and **1,094,640** +states. The intersection `{x T : x in B_3} intersect B_4` is empty, with +`T=diag([s],[s],[s])`. The involutive alphabet makes each ball closed under +inversion, so this excludes every word of length at most seven. This is a +complete finite exclusion, not an unsuccessful heuristic search. + +Free scalar work is an optimistic relaxation of a physical implementation. +The certificate prevents a saving in this exact alphabet and register count; +it does not price or admit a replacement for the selected bit supplier. + +## Independent checks and controls + +`verify.py` packs the 54 formal binary coefficients and multiplies on the right. +`independent.py` independently constructs the group from binary 2x2 matrices, +enumerates all 512 binary 3x3 matrices to select projectors, and multiplies on +the left in the **faithful regular representation** (complete 18x18 matrices). +Every exact-distance state set agrees after conversion, not just the counts +or hashes. Both target intersections are computed separately. The second +implementation additionally checks all **101,192** transitions through radius +three using generic dense matrix multiplication. + +[EXPECTED.json](EXPECTED.json) records the exact layers, transition counts, +both sets of deterministic hashes and 25 semantic controls. The controls +reject nine omitted calls, nine wrong labels, a missing third target, +nonidentity scalar residue, an expanded address alphabet, a nonidempotent +scalar factor, rank-three underpricing, a natural-representation kernel and +commuted address labels. Positive minimum controls recover 0, 3 and 6 for +zero, one and two swaps in the same three-register domain. + +The seven tests also check 4,704 scalar conjugations, all 3,024 optimized +generator actions on a complete 54-vector formal basis, all four target maps +on that basis, same-cardinality wrong state sets, altered receipts and source +bytes, and an isolated optimized replay of a read-only relocated package. +The linear-basis test is exhaustive for each optimized transition map. The +read-only test also rejects a falsified minimum in the receipt under `-O`. + +## Reproduce + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +python3 -I -B research/three-swap-cnot-census/verify.py +python3 scripts/research_package.py --package research/three-swap-cnot-census --check-only +python3 scripts/research_package.py --package research/three-swap-cnot-census +``` + +Expected direct line: + +```text +PASS_THREE_SWAP_CNOT_CENSUS minimum=9 registers=3 ball3=47203 ball4=1094640 meet=0 controls=25 no_new_kappa +``` + +The registered hook runs the complete census and all seven focused tests. +Direct replay takes approximately eight seconds and 356 MiB in the measured +CPython 3.12.3 environment; these are verifier observations, not multiplication +performance claims. `--emit` prints a newly computed receipt after comparison +with the committed receipt and does not write files. Hashes concatenate each +sorted exact-distance layer as seven-byte formal or 41-byte regular integers, +little endian. Equality checks compare the actual sets before hashing. + +[SOURCES.json](SOURCES.json) pins the unchanged rational-model context README +as a live input, historical catalogue/selected-record provenance at the base, +and the inspected predecessor texts separately. No pending PR is a runtime +dependency. The direct verifier works from a source export; the package +metadata check uses Git history for historical provenance. + +## Scope, assignment and overlap + +Base: `4040a0f46d67b41c36a472a7cd4af791fd4c36cc`. Chooser nonce: +`f327083ac49b0ead4b280ae0236eac2d`, bit-mechanisms, priority revision 2, +task `bit-new-register-model`, scope key `7084092dd726e7ba1f2f`. +[TASK.json](TASK.json) records the refinement. The claim is in +[discussion #1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912673). + +Immediate predecessors are PR #1414 at +`9e1640094f649ba6db9742796825a8d6c238989b` and Gareth Davidson's +[PR #1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333) at +`7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2`. PR #1333 permits all affine +rank-one address maps as units, including the swap itself; its different +alphabet would price the three targets at three. PR #468/#720 concern +rational abelian addresses. No rational frame data are reduced modulo two. + +[OVERLAP.json](OVERLAP.json) records snapshot coverage and the neighboring +claims. The concurrent `UT_3(F2)` two-commutator question has a different group +and endpoint. The `GL_3(F2)` spectator-swap and order-four-target claims expand +the address group and generator alphabet; neither is this three-swap problem. + +The proof is written and computer-assisted, not Lean-checked or independently +human-reviewed. No fourth-register census, arbitrary-register theorem, +physical compilation, common-label realization, whole-call hosting, +precision/tape, analytic transfer or selected-supplier cold replay is claimed. +The selected result is unchanged. + +## Open next questions + +1. **Can a fourth, restored dirty register help these three swaps?** This + tests whether the finite obstruction persists under borrowed workspace. + Start with the same formal target `diag([s],[s],[s],1)` and alphabet; + prove a reduced-state coverage rule before extending the radius-three/four + search. The larger projector/state inventory blocks simply extrapolating + this three-register receipt. Existing parity still excludes even lengths. +2. **Can a coefficient argument exclude seven calls with arbitrary extra + registers?** Such a proof would extend this finite finding to a general + three-swap theorem. First expand the 128 seven-label patterns, combine + equal-label runs, and seek a coefficient functional whose target has rank + three but whose product expansion has rank at most two. Longer alternating + runs are not covered by PR #1414's four-call argument; this package does + not assert the required functional exists. + +## Credit and license + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Credit this account's PR #1414 for the restricted model, sign-trace method, +two-swap result and explicit three-swap question; Gareth Davidson (@bitplane), +PR #1333, for the restricted-alphabet research direction and augmentation +normalization; eumemic (PR #288), Ali Romman (PR #468) and David Govea (PR #720) +for the surrounding register-model work. The new contribution is the complete +three-register, three-swap exclusion and its independent exact census. +No claim of priority for general rank or group-algebra methods is made. +New work is Apache-2.0; predecessor sources and notices remain unchanged. diff --git a/research/three-swap-cnot-census/SOURCES.json b/research/three-swap-cnot-census/SOURCES.json new file mode 100644 index 0000000000..4aaafd63fe --- /dev/null +++ b/research/three-swap-cnot-census/SOURCES.json @@ -0,0 +1,58 @@ +{ + "schema_version": 1, + "base_commit": "4040a0f46d67b41c36a472a7cd4af791fd4c36cc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ], + "contextual_predecessors": [ + { + "pr": 1414, + "head": "9e1640094f649ba6db9742796825a8d6c238989b", + "usage": "context only; no imported code or assumed theorem", + "files": [ + { + "path": "research/coordinate-cnot-register-bound/README.md", + "git_blob": "cdcc5a9e7f11ab3dbf7745a175ddcca208c68211", + "sha256": "e1666512fb71cf34c427c69ffb61a18b61e897a7f8f91f87820edf744e85a9fe", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/9e1640094f649ba6db9742796825a8d6c238989b/research/coordinate-cnot-register-bound/README.md" + }, + { + "path": "research/coordinate-cnot-register-bound/PROOF.md", + "git_blob": "68fee5b5ccff5329e27300e40dcbd483640dd6b7", + "sha256": "bcee89f92dcce8253bd7eae6e924ddff598c900da81979c6171a412f03d765e1", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/9e1640094f649ba6db9742796825a8d6c238989b/research/coordinate-cnot-register-bound/PROOF.md" + } + ] + }, + { + "pr": 1333, + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "usage": "context only; no imported code or assumed theorem", + "files": [ + { + "path": "research/binary-affine-register-bound/README.md", + "git_blob": "7b68583becf8be6f3cf666b05b0943e7eb99270c", + "sha256": "7951868efdf35fdb2aacdd302ca825cbde0586a5fae6df23aee78e29f30c332a", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2/research/binary-affine-register-bound/README.md" + } + ] + } + ] +} diff --git a/research/three-swap-cnot-census/TASK.json b/research/three-swap-cnot-census/TASK.json new file mode 100644 index 0000000000..5f15692cb3 --- /dev/null +++ b/research/three-swap-cnot-census/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 2, + "base_commit": "4040a0f46d67b41c36a472a7cd4af791fd4c36cc", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "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.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "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." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "Exactly three coordinate-SWAP targets on exactly three registers over formal F2[GL_2(F2)], with all 56 rank-one-idempotent coordinate-CNOT calls and free scalar GL_3(F2) changes. Certify the minimum paid count by exact radius-three/four coverage and odd-length parity.", + "scope_change_reason": "The card permits a specified nonabelian operation family. PR1414 explicitly leaves three swaps open after proving the two-swap result. This takes that new target multiplicity and fixes the register count to three, rather than repeating its two-swap theorem or the rational abelian starting model.", + "bottleneck_link": "A saving below nine would show that free scalar mixing can reduce the direct paid bill in this restricted nonabelian family. The complete exclusion blocks that candidate at exactly three registers before physical synthesis; it makes no claim about the selected paid moment or kappa.", + "budget_minutes": 60, + "stop_rule": "Complete balls of radius three/four and check the nine-call witness, or report exact partial coverage if the bounded search fails. Reserve the final session portion for verification. No extension to extra registers or an enlarged address alphabet in this package.", + "outcome": "negative-result", + "evidence": "PROOF.md plus EXPECTED.json: exact minimum nine; B3=47203, B4=1094640, zero target intersections. Independent full 18x18 state sets agree at every distance; 101192 dense transition checks and 25 semantic controls. VERIFY.json registers the complete replay and seven focused tests.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in reasoning, implementation, verification and writing. No independent human proof review or Lean verification is claimed.", + "open_questions": [ + { + "question": "Can one additional restored dirty register lower the three-swap bill?", + "why_it_matters": "Tests whether the finite obstruction survives borrowing workspace.", + "first_step": "Use exactly r=4, target diag([s],[s],[s],1), and the same a/b alphabet. Prove any symmetry reduction before a larger radius-three/four census.", + "blocked_by": "The present enumeration contains only r=3 projectors and states; its counts cannot be extrapolated." + }, + { + "question": "Can a coefficient-rank argument exclude seven calls for three swaps with arbitrary extra registers?", + "why_it_matters": "Would replace the register-count-dependent census by a broader scoped theorem.", + "first_step": "Expand the 128 seven-label patterns and seek a rank-at-most-two coefficient combination that is rank three on the target.", + "blocked_by": "Longer alternating runs are not covered by PR1414's four-call coefficient argument; no suitable functional is established here." + } + ], + "scope_key": "7084092dd726e7ba1f2f", + "refined_scope_key": "coordinate-CNOT/GL2F2/three-SWAP/exactly-three-registers/length<=7-plus-parity", + "chooser_nonce": "f327083ac49b0ead4b280ae0236eac2d", + "track": "bit-mechanisms", + "selected_method": "Derive a target-specific relaxation bound for that same explicit alphabet.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912673", + "predecessor_heads": { + "1414": "9e1640094f649ba6db9742796825a8d6c238989b", + "1333": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2" + }, + "runtime_dependencies": "Python 3.12 standard library; no pending PR implementation imported.", + "full_paid_budget": "Nine paid calls, no extra registers, no scalar changes in the attaining word. Free scalar preparation and restoration are granted for the lower-bound relaxation; every paid undo is counted.", + "unchanged_inputs": "The selected frontier, rational-model source and frozen predecessor packages are unchanged.", + "passed_over": [ + { + "task_id": "bit-helper-contract", + "scope_key": "bfb61f829a81535adeae", + "reason": "Immediate semantic-D and feedback/cleanup scopes are covered by PR1194/1311, this account's PR1306 and PR1420. PR1414 supplies a precise distinct next question." + } + ] +} diff --git a/research/three-swap-cnot-census/VERIFY.json b/research/three-swap-cnot-census/VERIFY.json new file mode 100644 index 0000000000..347fc5c5cf --- /dev/null +++ b/research/three-swap-cnot-census/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete formal radius-four census, independent faithful-regular state sets and target intersection, parity premises, nine-call witness, positive minima and 25 semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 180, + "checks": "Seven focused tests: exact algebra, all 4704 scalar conjugations, 3024 formal transition basis checks, 216 target basis checks, set/receipt/source corruptions and isolated optimized read-only relocation." + } + ] +} diff --git a/research/three-swap-cnot-census/independent.py b/research/three-swap-cnot-census/independent.py new file mode 100644 index 0000000000..cc41307f55 --- /dev/null +++ b/research/three-swap-cnot-census/independent.py @@ -0,0 +1,156 @@ +"""Separate faithful-regular census from actual binary address matrices. + +Enumerates all 512 scalar matrices to select rank-one idempotents, uses LEFT +multiplication of complete 18x18 binary matrices, and checks optimized steps +against dense row multiplication through radius three. Imports no producer code. +Prepared for commdata2338 with substantial OpenAI Codex assistance. Apache-2.0. +""" +import itertools + + +def rank(rows): + basis = {} + for row in rows: + while row: + bit = row.bit_length() - 1 + if bit in basis: + row ^= basis[bit] + else: + basis[bit] = row + break + return len(basis) + + +def small_product(left, right): + result = [] + for row in left: + new = 0 + for j, source in enumerate(right): + if (row >> j) & 1: + new ^= source + result.append(new) + return tuple(result) + + +def address_permutation(matrix): + return tuple(sum(((row & vector).bit_count() % 2) << i + for i, row in enumerate(matrix)) - 1 for vector in (1, 2, 3)) + + +def address_group(): + return tuple(sorted((m for m in itertools.product(range(4), repeat=2) + if rank(m) == 2), key=address_permutation)) + + +def scalar_idempotents(): + result = [] + for rows in itertools.product(range(8), repeat=3): + if rank(rows) == 1 and small_product(rows, rows) == rows: + u = sum((row != 0) << i for i, row in enumerate(rows)) + v = next(row for row in rows if row) + result.append((rows, u, v)) + return tuple(result) + + +def multiply(left, right, size=18): + """Generic dense binary matrix multiplication; no group-algebra shortcut.""" + row_mask = (1 << size) - 1 + right_rows = [(right >> (size * i)) & row_mask for i in range(size)] + result = 0 + for i in range(size): + row = (left >> (size * i)) & row_mask + output = 0 + while row: + bit = row & -row + output ^= right_rows[bit.bit_length() - 1] + row ^= bit + result |= output << (size * i) + return result + + +def identity(): + return sum(1 << (19 * i) for i in range(18)) + + +def target(): + group = address_group() + index = {m: i for i, m in enumerate(group)} + swap = (2, 1) + result = 0 + for register in range(3): + for h, matrix in enumerate(group): + row = index[small_product(swap, matrix)] + result |= 1 << (18 * (6 * register + row) + 6 * register + h) + return result + + +def census(radius=4): + group = address_group() + index = {m: i for i, m in enumerate(group)} + idempotents = scalar_idempotents() + if len(group) != 6 or len(idempotents) != 28: + raise ValueError("independent generator inventory") + row_mask = (1 << 18) - 1 + chunk_mask = (1 << 108) - 1 + labels = ((3, 2), (1, 3)) + permutations = [tuple(index[small_product(g, h)] for h in group) for g in labels] + dense_generators = [] + grouped = [] + for permutation in permutations: + row_moves = tuple((18 * source, 18 * destination) + for destination, source in enumerate(permutation)) + by_v = [] + for v in range(1, 8): + us = [] + for rows, u, actual_v in idempotents: + if actual_v != v: + continue + gen = identity() + for i in range(3): + for j in range(3): + if (rows[i] >> j) & 1: + for h in range(6): + gen ^= 1 << (18 * (6 * i + h) + 6 * j + h) + gen ^= 1 << (18 * (6 * i + h) + 6 * j + permutation[h]) + us.append((u, gen)) + dense_generators.append(gen) + by_v.append((v, us)) + grouped.append((row_moves, by_v)) + if len(set(dense_generators)) != 56: + raise ValueError("duplicate independent generators") + seen = {identity()} + levels = [seen.copy()] + attempts = [] + dense_checks = 0 + for depth in range(1, radius + 1): + new = set() + attempts.append(len(levels[-1]) * 56) + for word in levels[-1]: + r0 = word & chunk_mask + r1 = (word >> 108) & chunk_mask + r2 = word >> 216 + combos = (0, r0, r1, r0 ^ r1, r2, r0 ^ r2, r1 ^ r2, r0 ^ r1 ^ r2) + for row_moves, by_v in grouped: + for v, us in by_v: + chunk = combos[v] + transformed = 0 + for source, destination in row_moves: + transformed |= ((chunk >> source) & row_mask) << destination + delta = chunk ^ transformed + for u, gen in us: + changed = word + if u & 1: + changed ^= delta + if u & 2: + changed ^= delta << 108 + if u & 4: + changed ^= delta << 216 + if depth <= 3: + if changed != multiply(gen, word): + raise ValueError("optimized/dense regular transition mismatch") + dense_checks += 1 + if changed not in seen: + new.add(changed) + seen.update(new) + levels.append(new) + return levels, attempts, dense_checks diff --git a/research/three-swap-cnot-census/test_verify.py b/research/three-swap-cnot-census/test_verify.py new file mode 100644 index 0000000000..d1a3fa0c5c --- /dev/null +++ b/research/three-swap-cnot-census/test_verify.py @@ -0,0 +1,169 @@ +"""Focused algebra, completeness-binding and isolated replay controls. + +Prepared for commdata2338 with substantial OpenAI Codex assistance. Apache-2.0. +""" +import copy +import importlib.util +import itertools +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +PACKAGE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("three_swap_verify", PACKAGE / "verify.py") +verify = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verify) +independent = verify.load_independent() + + +def inverse(rows): + work = [row | (1 << (3 + i)) for i, row in enumerate(rows)] + for column in range(3): + pivot = next(i for i in range(column, 3) if (work[i] >> column) & 1) + work[column], work[pivot] = work[pivot], work[column] + for i in range(3): + if i != column and (work[i] >> column) & 1: + work[i] ^= work[column] + return tuple(row >> 3 for row in work) + + +class CensusTests(unittest.TestCase): + def test_algebra_and_faithfulness(self): + tables = verify.to_regular_tables() + for g in range(6): + for h in range(6): + x, y = 1 << g, 1 << h # (0,0) matrix entry only + self.assertEqual( + verify.to_regular(verify.formal_product(x, y), tables), + independent.multiply(verify.to_regular(x, tables), + verify.to_regular(y, tables))) + for g in (verify.A, verify.B): + for u, v in verify.PROJECTORS: + f = verify.factor(g, u, v) + self.assertEqual(verify.formal_product(f, f), verify.IDENTITY) + images = {verify.to_regular(1 << bit, tables) for bit in range(54)} + self.assertEqual(len(images), 54) + self.assertNotIn(0, images) + self.assertEqual(len(verify.controls(independent, tables)), 25) + + def test_scalar_normalization_inventory(self): + all_n = {rows for rows, _, _ in independent.scalar_idempotents()} + direct_n = {tuple(v if (u >> i) & 1 else 0 for i in range(3)) + for u, v in verify.PROJECTORS} + self.assertEqual(all_n, direct_n) + gl = [rows for rows in itertools.product(range(8), repeat=3) + if independent.rank(rows) == 3] + self.assertEqual(len(gl), 168) + checks = 0 + for basis in gl: + inv = inverse(basis) + self.assertEqual(independent.small_product(basis, inv), (1, 2, 4)) + for n in all_n: + conjugate = independent.small_product( + independent.small_product(basis, n), inv) + self.assertIn(conjugate, all_n) + checks += 1 + self.assertEqual(checks, 4704) + + def test_optimized_formal_steps_on_complete_linear_basis(self): + tables = verify.transition_tables() + factors = [verify.factor(g, u, v) for g in (verify.A, verify.B) + for u, v in verify.PROJECTORS] + checks = 0 + # Both maps are F2-linear in the current formal matrix; these 54 + # input vectors span every possible current matrix, including dirty ones. + for bit in range(54): + state = 1 << bit + for table, factor in zip(tables, factors, strict=True): + self.assertEqual(verify.apply_table(state, table), + verify.formal_product(state, factor)) + checks += 1 + self.assertEqual(checks, 3024) + for swaps in range(4): + for bit in range(54): + state = 1 << bit + self.assertEqual(verify.right_target(state, swaps), + verify.formal_product(state, verify.diagonal_target(swaps))) + + def test_full_state_set_guard(self): + tables = verify.to_regular_tables() + identity = verify.to_regular(verify.IDENTITY, tables) + verify.same_states({verify.IDENTITY}, {identity}, tables) + with self.assertRaisesRegex(ValueError, "cardinality"): + verify.same_states({verify.IDENTITY}, set(), tables) + with self.assertRaisesRegex(ValueError, "full state sets"): + verify.same_states({verify.IDENTITY}, {identity ^ 1}, tables) + + def test_receipt_mutations(self): + good = json.loads((PACKAGE / "EXPECTED.json").read_text()) + verify.compare_receipt(good, copy.deepcopy(good)) + for key in ("minimum_paid_calls", "registers", "exact_distance_layers", + "target_intersections_by_left_distance", + "formal_layer_sha256_7byte_little_endian", "semantic_controls"): + bad = copy.deepcopy(good) + del bad[key] + with self.assertRaisesRegex(ValueError, "receipt differs"): + verify.compare_receipt(good, bad) + + def test_live_source_rejection(self): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + inputs = [item for item in manifest["files"] if item["usage"] == "input"] + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + for item in inputs: + p = root / item["path"] + p.parent.mkdir(parents=True, exist_ok=True) + p.write_bytes((verify.ROOT / item["path"]).read_bytes()) + with patch.object(verify, "ROOT", root): + verify.check_inputs() + p = root / inputs[0]["path"] + p.write_bytes(p.read_bytes() + b"\nchanged-source\n") + with self.assertRaisesRegex(ValueError, "source pin mismatch"): + verify.check_inputs() + + def test_isolated_optimized_readonly_replay_and_bad_receipt(self): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + package = root / "research" / PACKAGE.name + shutil.copytree(PACKAGE, package, ignore=shutil.ignore_patterns("__pycache__")) + for item in manifest["files"]: + if item["usage"] == "input": + dest = root / item["path"] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.ROOT / item["path"], dest) + files = [p for p in root.rglob("*") if p.is_file()] + directories = [p for p in root.rglob("*") if p.is_dir()] + command = [sys.executable, "-I", "-O", "-B", str(package / "verify.py")] + try: + for p in files: + p.chmod(0o444) + for p in directories: + p.chmod(0o555) + passed = subprocess.run(command, cwd=root, capture_output=True, + text=True, timeout=120, check=False) + self.assertEqual(passed.returncode, 0, passed.stderr) + self.assertIn("minimum=9 registers=3", passed.stdout) + finally: + for p in directories: + p.chmod(0o755) + for p in files: + p.chmod(0o644) + expected = package / "EXPECTED.json" + corrupt = json.loads(expected.read_text()) + corrupt["minimum_paid_calls"] = 7 + expected.write_text(json.dumps(corrupt)) + rejected = subprocess.run(command, cwd=root, capture_output=True, + text=True, timeout=120, check=False) + self.assertNotEqual(rejected.returncode, 0) + self.assertIn("receipt differs", rejected.stderr) + self.assertEqual(list(root.rglob("__pycache__")), []) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/three-swap-cnot-census/verify.py b/research/three-swap-cnot-census/verify.py new file mode 100644 index 0000000000..c89e04ebf1 --- /dev/null +++ b/research/three-swap-cnot-census/verify.py @@ -0,0 +1,355 @@ +#!/usr/bin/env python3 +"""Exact three-swap census over F2[GL_2(F2)]; standard library only. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +Apache-2.0. No implementation is imported from a predecessor package. +""" +from __future__ import annotations + +import argparse +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +GROUP = tuple(itertools.permutations(range(3))) +GROUP_INDEX = {p: i for i, p in enumerate(GROUP)} +MUL = tuple(tuple(GROUP_INDEX[tuple(p[q[x]] for x in range(3))] + for q in GROUP) for p in GROUP) +E = GROUP_INDEX[(0, 1, 2)] +A = GROUP_INDEX[(0, 2, 1)] +B = GROUP_INDEX[(2, 1, 0)] +S = MUL[MUL[A][B]][A] +IDENTITY = sum(1 << (6 * (3 * i + i) + E) for i in range(3)) +TARGET = sum(1 << (6 * (3 * i + i) + S) for i in range(3)) +ROW_MASK = (1 << 18) - 1 +PROJECTORS = tuple((u, v) for u in range(1, 8) for v in range(1, 8) + if (u & v).bit_count() % 2) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_independent(): + spec = importlib.util.spec_from_file_location( + "three_swap_independent", PACKAGE / "independent.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def coefficient_product(x, y): + result = 0 + for i in range(6): + for j in range(6): + if (x >> i) & (y >> j) & 1: + result ^= 1 << MUL[i][j] + return result + + +def formal_product(left, right): + """Unoptimized full formal matrix multiplication, used for controls.""" + result = 0 + for i in range(3): + for j in range(3): + value = 0 + for k in range(3): + value ^= coefficient_product( + (left >> (6 * (3 * i + k))) & 63, + (right >> (6 * (3 * k + j))) & 63) + result |= value << (6 * (3 * i + j)) + return result + + +def factor(g, u, v, *, validate=True): + if validate: + require(g in (A, B), "address label outside a/b alphabet") + require((u, v) in PROJECTORS, "not a rank-one scalar idempotent") + result = IDENTITY + for i in range(3): + for j in range(3): + if (u >> i) & (v >> j) & 1: + result ^= ((1 << E) ^ (1 << g)) << (6 * (3 * i + j)) + return result + + +def word_product(word): + result = IDENTITY + for g, u, v in word: + result = formal_product(result, factor(g, u, v)) + return result + + +def direct_word(swaps=3): + return tuple((g, 1 << i, 1 << i) for i in range(swaps) + for g in (A, B, A)) + + +def diagonal_target(swaps): + return sum(1 << (6 * (3 * i + i) + (S if i < swaps else E)) + for i in range(3)) + + +def permute_coefficient(value, label): + return sum(((value >> h) & 1) << MUL[h][label] for h in range(6)) + + +def right_target(word, swaps=3): + """Right multiplication by the complete diagonal swap target.""" + return sum((permute_coefficient((word >> (6 * j)) & 63, S) + if j % 3 < swaps else (word >> (6 * j)) & 63) << (6 * j) + for j in range(9)) + + +def transition_tables(): + selectors = {u: bytearray(1 << 18) for u in range(1, 8)} + for row in range(1 << 18): + x, y, z = row & 63, (row >> 6) & 63, row >> 12 + for u in range(1, 8): + selectors[u][row] = ((x if u & 1 else 0) + ^ (y if u & 2 else 0) + ^ (z if u & 4 else 0)) + tables = [] + for g in (A, B): + for u, v in PROJECTORS: + delta = [] + for c in range(64): + d = c ^ permute_coefficient(c, g) + delta.append(sum(d << (6 * j) for j in range(3) + if (v >> j) & 1)) + tables.append((selectors[u], delta)) + return tables + + +def apply_table(word, table): + pick, delta = table + return (word ^ delta[pick[word & ROW_MASK]] + ^ (delta[pick[(word >> 18) & ROW_MASK]] << 18) + ^ (delta[pick[word >> 36]] << 36)) + + +def formal_census(radius=4): + require(0 <= radius <= 4, "registered census radius must be 0..4") + tables = transition_tables() + seen = {IDENTITY} + levels = [seen.copy()] + attempts = [] + for _ in range(radius): + new = set() + attempts.append(len(levels[-1]) * len(tables)) + for word in levels[-1]: + r0, r1, r2 = word & ROW_MASK, (word >> 18) & ROW_MASK, word >> 36 + for pick, delta in tables: + state = (word ^ delta[pick[r0]] ^ (delta[pick[r1]] << 18) + ^ (delta[pick[r2]] << 36)) + if state not in seen: + new.add(state) + seen.update(new) + levels.append(new) + return levels, attempts + + +def to_regular_tables(): + """Faithful left regular image, 18 rows of 18 bits (324 bits).""" + tables = [] + for i in range(3): + for j in range(3): + contributions = [] + for c in range(64): + matrix = 0 + for g in range(6): + if (c >> g) & 1: + for h in range(6): + matrix ^= 1 << (18 * (6 * i + MUL[g][h]) + 6 * j + h) + contributions.append(matrix) + tables.append(contributions) + return tables + + +def to_regular(word, tables): + result = 0 + for j in range(9): + result ^= tables[j][(word >> (6 * j)) & 63] + return result + + +def same_states(formal, regular, tables): + require(len(formal) == len(regular), "independent layer cardinality differs") + require({to_regular(w, tables) for w in formal} == regular, + "independent full state sets differ") + + +def state_digest(states, width): + digest = hashlib.sha256() + for value in sorted(states): + digest.update(value.to_bytes(width, "little")) + return digest.hexdigest() + + +def sign(g): + p = GROUP[g] + return sum(p[i] > p[j] for i in range(3) for j in range(i + 1, 3)) % 2 + + +def augmentation(word): + return sum((((word >> (6 * j)) & 63).bit_count() % 2) << j + for j in range(9)) + + +def controls(independent, tables): + names = [] + word = direct_word() + require(word_product(word) == TARGET, "nine-call positive witness failed") + for j in range(9): + require(word_product(word[:j] + word[j + 1:]) != TARGET, + "omitted-call mutation accepted") + names.append(f"omit_call_{j}") + for j, (g, u, v) in enumerate(word): + altered = word[:j] + ((B if g == A else A, u, v),) + word[j + 1:] + require(word_product(altered) != TARGET, "wrong-label mutation accepted") + names.append(f"wrong_label_{j}") + require(diagonal_target(2) != TARGET, "third dirty input was ignored") + names.append("omit_third_target") + scalar_cnot = IDENTITY ^ (1 << (6 * 1 + E)) + residual = formal_product(TARGET, scalar_cnot) + require(residual != TARGET and augmentation(residual) != augmentation(TARGET), + "nonidentity free scalar residue accepted") + names.append("scalar_residue") + for bad in ((S, 1, 1), (A, 1, 2)): + try: + factor(*bad) + except ValueError: + pass + else: + raise ValueError("illegal generator accepted") + names.extend(["expanded_address_alphabet", "nonidempotent_scalar"]) + bulk_a = sum(1 << (6 * (3 * i + i) + A) for i in range(3)) + bulk_b = sum(1 << (6 * (3 * i + i) + B) for i in range(3)) + allowed = {factor(g, u, v) for g in (A, B) for u, v in PROJECTORS} + require(bulk_a not in allowed and bulk_b not in allowed, + "rank-three projector underpriced") + require(formal_product(formal_product(bulk_a, bulk_b), bulk_a) == TARGET, + "rank-three scope control was not a real counterexample") + names.append("rank_three_underpricing") + natural_sum = 0 + for matrix in independent.address_group(): + natural_sum ^= matrix[0] | (matrix[1] << 2) + require(natural_sum == 0, "natural-image kernel control changed") + false_identity = IDENTITY ^ (63 << 6) + require(false_identity != IDENTITY + and to_regular(false_identity, tables) != to_regular(IDENTITY, tables) + and augmentation(false_identity) == augmentation(IDENTITY), + "nonfaithful representation accepted a false formal identity") + names.append("natural_representation_kernel") + require(formal_product(factor(A, 1, 1), factor(B, 1, 1)) + != formal_product(factor(B, 1, 1), factor(A, 1, 1)), + "address multiplication incorrectly commutes") + names.append("noncommuting_order") + return names + + +def check_inputs(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + checked = [] + for item in manifest["files"]: + if item["usage"] == "input": + require(hashlib.sha256((ROOT / item["path"]).read_bytes()).hexdigest() + == item["sha256"], "live source pin mismatch: " + item["path"]) + checked.append(item["path"]) + require(checked, "live source inventory is empty") + return checked + + +def compare_receipt(actual, expected): + require(actual == expected, "computed receipt differs from EXPECTED.json") + + +def compute(): + check_inputs() + independent = load_independent() + tables = to_regular_tables() + require(len(PROJECTORS) == 28, "projector inventory") + require(all(sign(MUL[g][h]) == (sign(g) ^ sign(h)) + for g in range(6) for h in range(6)), "sign is not a homomorphism") + require(all(sign(g) == 1 for g in (A, B, S)), "wrong sign labels") + require(all((u & v).bit_count() % 2 == 1 for u, v in PROJECTORS), "trace parity") + require(augmentation(TARGET) == augmentation(IDENTITY), "target augmentation") + formal, attempts = formal_census() + regular, regular_attempts, dense_checks = independent.census() + require(attempts == regular_attempts, "transition attempt coverage differs") + for x, y in zip(formal, regular, strict=True): + same_states(x, y, tables) + require(to_regular(TARGET, tables) == independent.target(), "target binding") + ball4 = set().union(*formal) + ball3 = set().union(*formal[:4]) + meet_counts = [sum(right_target(x) in ball4 for x in layer) + for layer in formal[:4]] + require(sum(meet_counts) == 0, "found a word of length at most seven") + reg_ball4 = set().union(*regular) + reg_target = independent.target() + reg_meets = [sum(independent.multiply(x, reg_target) in reg_ball4 for x in layer) + for layer in regular[:4]] + require(reg_meets == meet_counts, "independent target intersections differ") + minimum_controls = [] + for swaps in (0, 1, 2): + best = 99 + for d, layer in enumerate(formal[:4]): + for state in layer: + other = right_target(state, swaps) + for f, second in enumerate(formal[:4]): + if other in second: + best = min(best, d + f) + require(best == 3 * swaps, "positive minimum control failed") + require(word_product(direct_word(swaps)) == diagonal_target(swaps), + "positive formal boundary failed") + minimum_controls.append(best) + names = controls(independent, tables) + return { + "schema_version": 1, + "status": "PASS_THREE_SWAP_CNOT_CENSUS", + "registers": 3, + "active_swaps": 3, + "extra_dirty_registers": 0, + "minimum_paid_calls": 9, + "formal_group_order": [list(p) for p in GROUP], + "rank_one_idempotents": len(PROJECTORS), + "paid_generators": 2 * len(PROJECTORS), + "exact_distance_layers": [len(x) for x in formal], + "transition_attempts_by_depth": attempts, + "ball_radius_three": len(ball3), + "ball_radius_four": len(ball4), + "target_intersections_by_left_distance": meet_counts, + "independent_target_intersections": reg_meets, + "formal_layer_sha256_7byte_little_endian": [state_digest(x, 7) for x in formal], + "regular_layer_sha256_41byte_little_endian": [state_digest(x, 41) for x in regular], + "independent_full_state_sets_equal": True, + "independent_dense_transition_checks": dense_checks, + "parity_homomorphism_products": 36, + "permitted_call_count_parity": "odd", + "positive_minimum_controls": minimum_controls, + "semantic_controls": names, + "scope": "Finite certificate: exactly three registers in the stated formal alphabet; no new kappa.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print the computed receipt without writing files") + args = parser.parse_args() + receipt = compute() + compare_receipt(receipt, json.loads((PACKAGE / "EXPECTED.json").read_text())) + if args.emit: + print(json.dumps(receipt, indent=2, sort_keys=True)) + else: + print("PASS_THREE_SWAP_CNOT_CENSUS minimum=9 registers=3 " + f"ball3={receipt['ball_radius_three']} ball4={receipt['ball_radius_four']} " + f"meet=0 controls={len(receipt['semantic_controls'])} no_new_kappa") + + +if __name__ == "__main__": + main()