diff --git a/research/coordinate-cnot-address-spectator/EXPECTED.json b/research/coordinate-cnot-address-spectator/EXPECTED.json new file mode 100644 index 0000000000..4a7b0f2dd3 --- /dev/null +++ b/research/coordinate-cnot-address-spectator/EXPECTED.json @@ -0,0 +1,77 @@ +{ + "cases": [ + { + "address_dimension": 3, + "ball_2_sha256": "c0c15abd8e4e9e9e45669cd232d913aa97e6dc58054049803ed6b53f7ecb485e", + "ball_2_size": 853, + "base_intersection": 0, + "controls": [ + "omit_call_0", + "omit_call_1", + "omit_call_2", + "omit_call_3", + "omit_call_4", + "omit_call_5", + "wrong_spectator_label", + "unrestored_address_spectator", + "nonfaithful_natural_representation", + "one_swap_positive", + "identity_positive", + "rank_two_unit_price_outside_alphabet" + ], + "edge_attempts_per_engine": 30708, + "edge_intersection": 0, + "exact_distance_layers_0_1_2": [ + 1, + 36, + 816 + ], + "formal_upper_bound": 6, + "generators": 36, + "independent_complete_ball_and_alphabet_equal": true, + "minimum_paid_calls": 6, + "projectors": 6, + "registers": 2, + "shifted_ball_2_sha256": "0bfac8b22348eff80833826ad3d9276f71539d95741b9e2f2d52de3e06fc281a" + }, + { + "address_dimension": 3, + "ball_2_sha256": "5d6c723221a0f5835265ad9fda0a500d718a43d5d963c89b570717c2644cbcb9", + "ball_2_size": 17515, + "base_intersection": 0, + "controls": [ + "omit_call_0", + "omit_call_1", + "omit_call_2", + "omit_call_3", + "omit_call_4", + "omit_call_5", + "wrong_spectator_label", + "unrestored_address_spectator", + "clean_only_dirty_register_fault", + "nonfaithful_natural_representation", + "one_swap_positive", + "identity_positive", + "rank_two_unit_price_outside_alphabet" + ], + "edge_attempts_per_engine": 2942520, + "edge_intersection": 0, + "exact_distance_layers_0_1_2": [ + 1, + 168, + 17346 + ], + "formal_upper_bound": 6, + "generators": 168, + "independent_complete_ball_and_alphabet_equal": true, + "minimum_paid_calls": 6, + "projectors": 28, + "registers": 3, + "shifted_ball_2_sha256": "1a21de159a506eac76ad7a99de349820ce98975c94fb68ddc7b5c3c5d4f16b02" + } + ], + "model": "M_r(F2[GL_3(F2)]); all six coordinate CNOTs; r=2,3", + "no_new_kappa": true, + "result": "finite_lower_bound_plus_formal_upper_bound", + "schema_version": 1 +} diff --git a/research/coordinate-cnot-address-spectator/OVERLAP.json b/research/coordinate-cnot-address-spectator/OVERLAP.json new file mode 100644 index 0000000000..c46fec0a73 --- /dev/null +++ b/research/coordinate-cnot-address-spectator/OVERLAP.json @@ -0,0 +1,115 @@ +{ + "schema_version": 1, + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912696", + "entry_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T01:13:06.664495+00:00", + "complete_pagination": true, + "records": 828 + }, + "discussions": { + "fetched_at": "2026-10-14T01:13:30.574789+00:00", + "complete_pagination": true, + "records": 162 + } + }, + "refined_claim_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T01:16:51.376284+00:00", + "complete_pagination": true, + "records": 828 + }, + "discussions": { + "fetched_at": "2026-10-14T01:17:16.267853+00:00", + "complete_pagination": true, + "records": 162 + } + }, + "pre_submission_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T01:34:09.157196+00:00", + "complete_pagination": true, + "records": 744 + }, + "discussions": { + "fetched_at": "2026-10-14T01:24:02.227375+00:00", + "complete_pagination": true, + "records": 169 + } + }, + "queries": [ + [ + "--task", + "bit-helper-contract" + ], + [ + "--task", + "bit-new-register-model" + ], + [ + "three swaps", + "three-SWAP", + "seven-call", + "coordinate-cnot" + ], + [ + "GL_3(F2)", + "three-dimensional coordinate", + "spectator coordinate", + "coordinate-CNOT" + ], + [ + "address spectator", + "GL_3(F2)", + "two swaps" + ], + [ + "address spectator", + "GL_3(F2)", + "two swaps", + "coordinate-CNOT" + ] + ], + "query_mode": "find_overlap.py --offline with cached public PR/Discussion records; no refresh or authenticated access", + "coverage_limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "warnings": [ + "open_prs: offline; cached data may miss current changes", + "discussions: offline; cached data may miss current changes" + ], + "predecessor_heads_rechecked_anonymously": "2026-10-14T01:32Z; git ls-remote confirmed PR1333 and PR1414 heads", + "nearest_work": [ + { + "pr": 1414, + "head": "9e1640094f649ba6db9742796825a8d6c238989b", + "difference": "Two GL2 address CNOTs, two swaps, arbitrary extra scalar registers. The new result permits all six GL3 CNOTs but covers exactly r=2,3." + }, + { + "pr": 1333, + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "difference": "All affine rank-one address labels are paid units, including the swap itself. The new result prices only coordinate CNOTs." + }, + { + "discussion": 1317, + "comment": 18912673, + "difference": "Concurrent three GL2 swaps at exactly r=3; our target is two GL3 swaps with a third address coordinate." + }, + { + "discussion": 1317, + "comment": 18912727, + "difference": "Concurrent two order-four GL3 targets at r=2, direct bill eight; our order-two swap target has a fixed third coordinate and direct bill six." + }, + { + "discussion": 1317, + "comment": 18912406, + "difference": "UT3(F2) central commutator targets with two labels, rather than GL3 coordinate swaps with six labels." + }, + { + "pr": 840, + "head": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "difference": "Native BIT dyadic-shear fusion and rational/modular addresses, not this finite formal nonabelian register alphabet." + } + ], + "other_card_passed_over": "bit-helper-contract: the immediate semantic-D and projected-cleanup questions already have PR1194/1311/1420 and this account's PR1306.", + "distinction_from_other_completed_account_work": "No repeat of PR677,790,794,1304,1306,1307,1372,1375,1379,1414,1415,1421. In particular the earlier two-swap theorem uses a smaller address alphabet; no source or result from it is claimed anew." +} diff --git a/research/coordinate-cnot-address-spectator/PROOF.md b/research/coordinate-cnot-address-spectator/PROOF.md new file mode 100644 index 0000000000..47c3541cd4 --- /dev/null +++ b/research/coordinate-cnot-address-spectator/PROOF.md @@ -0,0 +1,191 @@ +# Two swaps with an address spectator: a finite six-call certificate + +This proof establishes a minimum in an explicit finite register model. It +does not establish a new bit supplier or multiplication exponent. The lower +bound has a complete finite computation; the upper bound is a formal identity. + +## 1. Model and statement + +Let `G = GL_3(F2)` and `R = F2[G]`, the **formal group algebra**, with independent +symbols `[g]` for group elements. Let + +\[ + g_{ij}=I_3+E_{ij}\quad (i\ne j),\qquad + s=\begin{pmatrix}0&1&0\\1&0&0\\0&0&1\end{pmatrix}. +\] + +There are six allowed paid address labels `g_ij`. In particular, the four +labels involving coordinate 3 are available during the word, although that +coordinate must be restored at the endpoint. + +For `r` scalar registers, a paid unit is + +\[ + D_N(g)=I_r+([g]+1)N,\qquad + N=uv^T,\quad u,v\in\mathbb F_2^r,\quad v^Tu=1. +\] + +Thus `N` is a binary rank-one idempotent, and every occurrence costs one. +Free scalar `GL_r(F2)` changes of basis may appear anywhere. No address map +is free. There are no copies, erasures, clean allocations or translations. +Undo calls have the same unit price. The target is + +\[ + T_r=\operatorname{diag}([s],[s],1,\ldots,1). +\] + +Equality is required in `M_r(R)` on all arbitrary inputs. At `r=3`, the +additional scalar register is arbitrarily dirty and must be restored, with +no leakage into either active output. An extra **scalar register** differs +from the third **address coordinate** present in every register. + +**Finite-certificate theorem.** For exactly `r=2` and exactly `r=3`, the +minimum paid-call cost of `T_r` is **six**, even with free scalar mixing and +all six three-dimensional coordinate CNOTs available. + +This extends the allowed address alphabet of the two-dimensional two-swap +result in [PR1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414). +Its all-register conclusion is **not** inherited for the enlarged alphabet. +The result here makes no assertion for `r>=4` or address dimension `>=4`. + +## 2. Remove free scalar gates without changing the paid count + +For an invertible scalar matrix `B`, moving it past a paid factor conjugates +`N` to `B N B^-1`. This remains a binary rank-one idempotent. Any word is +therefore a product of paid factors followed by one scalar matrix `B_total`. + +Augmentation `R -> F2`, `[g] -> 1`, sends every paid factor and the target +to `I_r`. Hence `B_total=I_r`. It suffices to enumerate paid factors alone. +This is the normalization argument credited to Gareth Davidson's PR1333 and +reused in PR1414. It permits arbitrarily many free scalar gates; the finite +search does not silently bound their number. + +Every binary rank-one matrix has a unique presentation `uv^T` with `u,v` +nonzero: over `F2` there is no nontrivial scalar rescaling. Idempotence is +equivalent to `v^T u=1`. For each of the `2^r-1` choices of `u`, exactly +`2^(r-1)` choices of `v` satisfy that equation. The complete projector counts +are 6 and 28, giving 36 and 168 paid generators. + +## 3. A necessary representation suffices for exclusion + +Extend the natural address representation linearly to an algebra homomorphism + +\[ + \rho:R\longrightarrow M_3(\mathbb F_2),\qquad [g]\longmapsto g. +\] + +Its block extension sends a paid factor to + +\[ + \widehat D_N(g_{ij})=I_{3r}+N\otimes E_{ij}. +\] + +The target image swaps address coordinates 1 and 2 in registers 1 and 2, +fixing every other coordinate. Every formal identity must give this natural +matrix identity. Thus **nonexistence in the matrix image implies +nonexistence in the formal algebra**. + +The converse is not used. The representation is not faithful as an algebra: +the formal sum of the six elements of the embedded `GL_2(F2)` subgroup is +nonzero, while its natural image is zero. The verifier checks this explicit +kernel element and a false endpoint obtained by adding it to `T_r`. + +This is a necessary-condition relaxation of a fully specified formal model, +not an inference from finite payload trials to a universal identity. All +`3r` matrix coordinates are retained, including the address spectator and +the extra dirty scalar register. + +## 4. Complete five-call exclusion by radius-two balls + +Let `S` be the complete finite alphabet of natural matrix generators, and +let `B_k` contain all products of at most `k` generators. Each generator is +an involution: `E_ij^2=0` for `i!=j`. Consequently every `B_k` is closed under +inversion. + +A word of length at most five reaches `T = rho(T_r)` if and only if + +\[ + B_3\cap T B_2\ne\varnothing. +\] + +Indeed, split the word as `T=A B` with `A in B_3` and `B in B_2`. Then +`A=T B^-1`. Conversely, `A=T C` gives `T=A C^-1` of length at most five. +Words shorter than five are included because the balls contain the identity. + +The primary implementation constructs `B_2` by breadth-first traversal. +It checks `B_2 intersect T B_2` and then **every** pair `(x,g) in B_2 x S`, +testing whether `g x` belongs to `T B_2`. This streams all of `B_3`; it does +not need to store or deduplicate its third layer. Repeated edge endpoints +are harmless. There is no sampled prefix, symmetry quotient, timeout success, +heuristic pruning, or approximation. + +The independent implementation stores matrix columns, obtains projectors by +filtering all `2^(r*r)` binary matrices for rank one and idempotence, and +multiplies on the **right**. It checks `B_3 intersect B_2 T`, whose emptiness +is equivalent by the same splitting argument. The two implementations agree +on every generator, every state of `B_2`, and its exact distance layers. +Both full edge scans have zero intersections. + +| Scalar registers | Projectors | Paid generators | Distance layers 0,1,2 | `B_2` | Edges scanned per implementation | Hits | +|---|---:|---:|---|---:|---:|---:| +| 2 | 6 | 36 | 1, 36, 816 | 853 | 30,708 | 0 | +| 3 | 28 | 168 | 1, 168, 17,346 | 17,515 | 2,942,520 | 0 | + +The exact endpoint and alphabet equality are checked as sets, not inferred +from equal counts or hashes. `EXPECTED.json` also records deterministic +SHA256 digests. Matrices are encoded as consecutive `n`-bit rows with row +zero in the low bits (`n=3r`), sorted as unsigned integers, each serialized in +`ceil(n*n/8)` little-endian bytes before hashing. Shifted-ball hashes refer +to the primary **left** shift, not the independent right shift. + +## 5. Formal six-call attainment + +For every scalar idempotent `N`, formal expansion gives + +\[ + D_N(g)D_N(h)=D_N(gh). +\] + +Since `g_12 g_21 g_12=s`, apply that three-call sequence on `N=E_11` and +then on `N=E_22`. The full product is exactly `T_r` in `M_r(R)`. It needs +six paid calls, no free scalar gates, no additional roles, and no omitted +restoration. It is valid for any `r>=2` and on every `R`-module; only the +lower bound is restricted to `r=2,3`. + +The checker multiplies sparse **formal group coefficients**, where each +group label is its exact binary 3-by-3 matrix. It does not use the natural +representation to accept this witness. Every omitted call and a substituted +spectator label fail the full endpoint check. + +## 6. Scope and controls + +The paid count is a complete invoice for this deliberately optimistic +free-scalar model, not for a physical supplier. This certificate rules out +the proposed six-to-five saving in its domain. It does not price physical +scalar work or improve a recursive rank histogram or kappa. + +Controls cover omitted calls, a wrong spectator label, unrestored address +state, a fault visible only on a dirty third register, nonfaithful natural +equality, and forbidden rank-two projectors priced as units. Identity and +one-swap endpoints are positive controls. Source and receipt mutations, +natural/formal compatibility, free-scalar conjugation closure, and a +read-only relocated optimized replay are checked by the focused tests. + +Neither the written argument nor the finite checker has been Lean-checked +or independently reviewed by a human. No selected-supplier cold replay, +all-size physical compiler, hosting, precision/tape, or outer analytic +transfer has been run. No conclusion for arbitrary extra registers follows +from the finite counts. + +## Attribution + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Gareth Davidson (@bitplane), PR1333, posed the restricted coordinate-CNOT +question and supplied the broader affine rank-priced model and normalization. +This account's PR1414 supplies the two-dimensional two-swap result and its +higher-dimensional next question. Eumemic (PR288), Ali Romman (PR468) and +David Govea (PR720) are credited for the surrounding rational abelian +register-model lineage. No predecessor code is imported, no rational frame +is reduced modulo two, and no general rank principle or literature-priority +claim is made. New work is Apache-2.0. diff --git a/research/coordinate-cnot-address-spectator/README.md b/research/coordinate-cnot-address-spectator/README.md new file mode 100644 index 0000000000..15b3db71d9 --- /dev/null +++ b/research/coordinate-cnot-address-spectator/README.md @@ -0,0 +1,132 @@ +# A third address coordinate does not cheapen two swaps at two or three registers + +**Finite certificate: the minimum is six paid calls; no new kappa.** Two +coordinate-SWAP targets still cost six when all six coordinate CNOTs on +**three address coordinates** are allowed, for exactly two or three scalar +registers. Free scalar mixing is allowed. At three registers, the extra +register is arbitrary dirty input and is restored. + +This answers a bounded part of the higher-dimensional alphabet question in +this account's [PR1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414). +That predecessor permits only the two CNOTs on two address coordinates and +proves an all-register result. The present certificate adds the four gates +touching a third address coordinate, but its lower bound covers only `r=2,3`. +It is separate from the concurrent three-SWAP investigation in the original +two-dimensional alphabet. + +## Exact model and result + +Work in `M_r(F2[GL_3(F2)])`. A paid call is +`I+([I+E_ij]+1)N`, for all six `i!=j` and all binary rank-one idempotents +`N=uv^T`, `v^T u=1`. The target is `diag([s12],[s12],1,...,1)`, where `s12` +swaps address coordinates 1 and 2 and fixes coordinate 3. Equality is formal +group-algebra equality on arbitrary inputs. There are no free address maps, +translations, copies, erasures or clean allocations; undo calls are paid. + +[PROOF.md](PROOF.md) states the full contract and finite-coverage argument. +Free scalar `GL_r(F2)` mixing normalizes away by augmentation. A formal word +maps to binary matrices of size `3r` through the natural representation. +An exhaustive rejection in that representation proves rejection of formal +words. Natural matrix equality is **not** used to accept a formal identity. +The direct six-call upper bound is checked in the full group algebra. + +| Registers | Paid generators | Exact distance layers 0,1,2 | States within two calls | Edges scanned by each checker | Short target matches | +|---|---:|---|---:|---:|---:| +| 2 | 36 | 1, 36, 816 | 853 | 30,708 | 0 | +| 3 | 168 | 1, 168, 17,346 | 17,515 | 2,942,520 | 0 | + +Every word of length at most five splits into a prefix of at most three +calls and a suffix of at most two. Streaming every edge from the radius-two +ball therefore gives complete coverage without storing the third layer. +There is no symmetry reduction or sampling. Two code-disjoint implementations +agree on their entire generator sets and radius-two balls; both independently +reject every target intersection. The second enumerates all scalar matrices +and uses column operations and right multiplication, rather than the first +implementation's rank-one parametrization and left row updates. + +[EXPECTED.json](EXPECTED.json) records exact counts and deterministic state +hashes. The direct replay includes 25 positive, boundary and model controls +across the two register counts. These include all six omitted calls, a wrong +spectator label, unreturned address state, a dirty-only fault, a nonzero +formal element with zero natural image, and a forbidden rank-two unit-price +alphabet. The focused tests check algebra compatibility and free-scalar +conjugation, and reject real source and receipt corruptions. + +## Reproduce + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +python3 -I -B research/coordinate-cnot-address-spectator/verify.py +python3 -B scripts/research_package.py --package research/coordinate-cnot-address-spectator --check-only +python3 -B scripts/research_package.py --package research/coordinate-cnot-address-spectator +``` + +The direct replay prints: + +```text +PASS_COORDINATE_CNOT_ADDRESS_SPECTATOR minimum=6 registers=2,3 address_dimension=3 controls=25 no_new_kappa +``` + +The registered replay additionally runs the seven focused test groups, +including an isolated optimized replay from a read-only source export. +`verify.py --emit` recomputes and prints the deterministic receipt without +writing files. There are no solver, compiler, network or third-party package +dependencies. [VERIFY.json](VERIFY.json) declares the bounded replay. + +## Scope, provenance and overlap + +Base: `4040a0f46d67b41c36a472a7cd4af791fd4c36cc`. Task: +`bit-new-register-model`, priority revision 2, scope key +`7f5f4426ef796683c485`, chooser nonce `70587133f1c80395ae4658456ec59584`. +The claim is in [discussion #1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317). +[TASK.json](TASK.json) contains the refined task card and next questions. +[SOURCES.json](SOURCES.json) records exact provenance and contextual predecessor +heads; [OVERLAP.json](OVERLAP.json) records snapshot coverage and distinctions. +No pending implementation is imported. + +Gareth Davidson's [PR1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333) +allows all affine rank-one labels at unit price, including the swap itself; +its rank-floor theorem therefore uses a different paid alphabet. PR1414 +restricts to two-dimensional coordinate CNOTs. The concurrent `UT_3(F2)` +central-commutator investigation uses another group and target. The +[concurrent order-four GL3 claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912727) +uses two copies of a different target, with all three coordinates essential +and direct bill eight, instead of two order-two swaps with direct bill six. +None of those results is silently generalized here. + +The source-bound baseline confirms that the selected complex supplier remains +the binding side. This is a bit-mechanism cost screen, with no change to the +selected record, paid recursive histogram or exponent. It does not cover +arbitrary extra registers, more address coordinates, general nonabelian +targets or another scalar field. The proof is not Lean-checked or independently +human-reviewed. Physical realization, compiler, hosting, precision/tape and +outer analytic transfer are unrun; no selected-supplier cold replay is claimed. + +## Open next questions + +1. **Does six remain the minimum with arbitrary restored dirty registers?** + This would turn the finite screen into an all-register obstruction for the + enlarged alphabet. A feasible first step is a separately bounded `r=4` + natural-image census, or a rank argument for all five-call label patterns. + The blocker is the absence of a dimension-independent compression or + coefficient argument; these two finite cases do not supply one. +2. **Can a second address spectator change the cost?** Enlarge to all twelve + coordinate CNOTs in `GL_4(F2)` at `r=2`, keeping the same two-swap endpoint. + This tests whether the present obstruction survives another operation + alphabet. Recompute the full natural-image census, checking any surviving + candidates formally; a faithful group action alone cannot accept a group- + algebra identity. No higher-dimensional exclusion is inherited here. + +## Credit and license + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Credit Gareth Davidson (@bitplane), PR1333, for the restricted-alphabet +question and augmentation normalization, and this account's PR1414 for the +two-swap predecessor and explicit higher-dimensional question. Credit eumemic +(PR288), Ali Romman (PR468), and David Govea (PR720) for the rational abelian +register-model lineage. The two checkers were written separately within this +AI-assisted contribution; this is not independent human review. New work is +Apache-2.0; predecessor source files and licenses are unchanged. No literature- +priority or general rank-principle claim is made. diff --git a/research/coordinate-cnot-address-spectator/SOURCES.json b/research/coordinate-cnot-address-spectator/SOURCES.json new file mode 100644 index 0000000000..ac06c0265f --- /dev/null +++ b/research/coordinate-cnot-address-spectator/SOURCES.json @@ -0,0 +1,55 @@ +{ + "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; not imported or required for replay", + "files": [ + { + "path": "research/coordinate-cnot-register-bound/README.md", + "git_blob": "cdcc5a9e7f11ab3dbf7745a175ddcca208c68211", + "sha256": "e1666512fb71cf34c427c69ffb61a18b61e897a7f8f91f87820edf744e85a9fe" + }, + { + "path": "research/coordinate-cnot-register-bound/PROOF.md", + "git_blob": "68fee5b5ccff5329e27300e40dcbd483640dd6b7", + "sha256": "bcee89f92dcce8253bd7eae6e924ddff598c900da81979c6171a412f03d765e1" + } + ] + }, + { + "pr": 1333, + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "usage": "context only; not imported or required for replay", + "files": [ + { + "path": "research/binary-affine-register-bound/README.md", + "git_blob": "7b68583becf8be6f3cf666b05b0943e7eb99270c", + "sha256": "7951868efdf35fdb2aacdd302ca825cbde0586a5fae6df23aee78e29f30c332a" + } + ] + } + ] +} diff --git a/research/coordinate-cnot-address-spectator/TASK.json b/research/coordinate-cnot-address-spectator/TASK.json new file mode 100644 index 0000000000..e2726d0f1c --- /dev/null +++ b/research/coordinate-cnot-address-spectator/TASK.json @@ -0,0 +1,83 @@ +{ + "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": "Two SWAP targets in M_r(F2[GL_3(F2)]), all six coordinate-CNOT labels, r=2 or r=3, free scalar GL_r mixing and complete dirty restoration: exact six-call minimum.", + "scope_change_reason": "The card permits a specified nonabelian alphabet. Expand PR1414 from the two GL2 coordinate CNOTs to all six GL3 coordinate CNOTs; keep two SWAP targets and bound the scalar register counts. The concurrent three-SWAP GL2 question was passed over at overlap check.", + "bottleneck_link": "Scoped bit-mechanism cost screen: an optimistic free-scalar model already rejects a six-to-five paid-call saving. No physical supplier, paid recursive profile or kappa change is inferred; the selected complex side still binds.", + "budget_minutes": 60, + "stop_rule": "Complete both five-call matrix-image censuses, formally check the direct six-call witness and controls, and stop. If a matrix-image candidate occurs, require full formal coefficients. Session budget 60 minutes, reserve final quarter for checking; hand off incomplete coverage.", + "outcome": "negative-result", + "evidence": "PROOF.md and EXPECTED.json: exact balls of 853 and 17515 states, complete 30708 and 2942520 edge scans per implementation, zero target intersections, complete formal six-call upper bounds, 25 positive/boundary/model controls and seven focused test groups.", + "author": "commdata2338", + "ai_assistance": "Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. Two code-disjoint implementations within the same AI-assisted session; no independent human review.", + "open_questions": [ + { + "question": "Does six remain the minimum with arbitrary restored dirty scalar registers in the GL3 coordinate-CNOT alphabet?", + "why_it_matters": "Would extend this finite mechanism screen to an all-register obstruction.", + "first_step": "Run a separately bounded r=4 matrix-image census or classify five-call label patterns by rank.", + "blocked_by": "No dimension-independent scalar compression or coefficient argument is established." + }, + { + "question": "Can a second address spectator lower the two-SWAP cost?", + "why_it_matters": "Tests whether the operation-alphabet obstruction persists in higher dimension.", + "first_step": "At r=2 enumerate all twelve GL4 coordinate CNOTs through five calls and check any surviving candidates formally.", + "blocked_by": "The present certificate has no GL4 coverage; natural equality is insufficient for accepting a formal candidate." + } + ], + "chooser_nonce": "70587133f1c80395ae4658456ec59584", + "track": "bit-mechanisms", + "scope_key": "7f5f4426ef796683c485", + "refined_scope_key": "GL3F2-all-six-coordinate-CNOT/two-SWAP/r2-r3/five-call-census", + "claim_discussion": 1317, + "local_task_card": { + "base_and_predecessors": "Base 4040a0f46d67b41c36a472a7cd4af791fd4c36cc; PR1414 9e1640094f649ba6db9742796825a8d6c238989b; PR1333 7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2. Context only; no pending code dependency.", + "concrete_question": "Two SWAP targets in M_r(F2[GL_3(F2)]), all six coordinate-CNOT labels, r=2 or r=3, free scalar GL_r mixing and complete dirty restoration: exact six-call minimum.", + "changed_restriction": "Nonabelian binary address group instead of the rational abelian starting model; four more coordinate-CNOT labels than PR1414. No reduction of rational frames modulo two.", + "method_and_domain": "All rank-one binary idempotents and six coordinate labels, r=2,3; exact natural-image lower-bound relaxation, independent row/column traversals, full formal upper witness.", + "nearest_overlap": "PR1414: two GL2 CNOTs and arbitrary registers; PR1333: all affine rank-one address labels. Concurrent three-SWAP GL2 and UT3 central-commutator targets are different questions.", + "complete_budget": "Every paid call costs one, including undo calls; all scalar GL_r mixing is free only as an explicit optimistic relaxation. Direct bound six; required saving at most five.", + "success_and_falsification": "Complete short-word exclusion or a full formal shorter identity. Search positive controls, semantic endpoint/alphabet faults, source and receipt corruption, and independent exact state-set equality.", + "predecessor_credit": "commdata2338 PR1414; Gareth Davidson (@bitplane) PR1333; eumemic PR288; Ali Romman PR468; David Govea PR720.", + "artifact_and_reproduction": "research/coordinate-cnot-address-spectator; python3 -I -B research/coordinate-cnot-address-spectator/verify.py", + "unchecked": "r>=4, address dimension>=4, arbitrary nonabelian alphabets, Lean, independent human review, supplier compilation, hosting, precision/tape, full cold replay and outer transfer." + } +} diff --git a/research/coordinate-cnot-address-spectator/VERIFY.json b/research/coordinate-cnot-address-spectator/VERIFY.json new file mode 100644 index 0000000000..b013e67b38 --- /dev/null +++ b/research/coordinate-cnot-address-spectator/VERIFY.json @@ -0,0 +1,36 @@ +{ + "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 two-engine five-call exclusion, formal six-call witness and 25 positive/boundary/model controls." + }, + { + "argv": [ + "{python}", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_verify.py" + ], + "timeout_seconds": 180, + "checks": "Seven focused groups: algebra map, scalar conjugation, independent alphabet, receipt mutations, real source/receipt rejection and read-only relocated optimized replay." + } + ] +} diff --git a/research/coordinate-cnot-address-spectator/independent.py b/research/coordinate-cnot-address-spectator/independent.py new file mode 100644 index 0000000000..2c65a76ece --- /dev/null +++ b/research/coordinate-cnot-address-spectator/independent.py @@ -0,0 +1,104 @@ +"""Independent natural-image census using columns and right multiplication. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +Apache-2.0. Imports no implementation from the primary checker. +""" + + +def rank(rows): + pivots = {} + for row in rows: + while row: + top = row.bit_length() - 1 + if top in pivots: + row ^= pivots[top] + else: + pivots[top] = row + break + return len(pivots) + + +def scalar_product(left, right, r): + return tuple(sum(((sum(((left[i] >> k) & 1) * ((right[k] >> j) & 1) + for k in range(r))) % 2) << j for j in range(r)) + for i in range(r)) + + +def all_projectors(r): + # Enumerate ALL 2^(r*r) matrices; do not inherit the u,v parametrization. + mask = (1 << r) - 1 + return [rows for code in range(1 << (r * r)) + if rank(rows := tuple((code >> (i * r)) & mask for i in range(r))) == 1 + and scalar_product(rows, rows, r) == rows] + + +def to_rows_integer(columns): + n = len(columns) + return sum(((columns[j] >> i) & 1) << (i * n + j) for i in range(n) for j in range(n)) + + +def column_generators(r): + n = 3 * r + records = [] + for p in all_projectors(r): + for a in range(3): + for b in range(3): + if a == b: + continue + columns = [] + for col in range(n): + out = 1 << col + if col % 3 == b: + for row in range(r): + if p[row] >> (col // 3) & 1: + out ^= 1 << (3 * row + a) + columns.append(out) + changes = [(j, column ^ (1 << j)) for j, column in enumerate(columns) + if column != 1 << j] + vectors = {delta for _, delta in changes} + if len(vectors) != 1: + raise ValueError("generator difference is not rank one") + vector = vectors.pop() + sources = tuple(k for k in range(n) if vector >> k & 1) + destinations = tuple(j for j, _ in changes) + records.append((tuple(columns), sources, destinations)) + return records + + +def right_step(columns, record): + # Column operations compute M G, unlike the primary row updates G M. + row = 0 + for k in record[1]: + row ^= columns[k] + output = list(columns) + for k in record[2]: + output[k] ^= row + return tuple(output) + + +def right_target(columns): + result = list(columns) + result[0], result[1] = result[1], result[0] + result[3], result[4] = result[4], result[3] + return tuple(result) + + +def census(r): + records = column_generators(r) + ball = {tuple(1 << k for k in range(3 * r))} + front = set(ball) + layers = [1] + for _ in range(2): + nxt = {right_step(state, record) for state in front for record in records} - ball + layers.append(len(nxt)) + ball.update(nxt) + front = nxt + shifted = {right_target(state) for state in ball} + base_hits = len(ball & shifted) + edge_hits = 0 + for state in ball: + for record in records: + if right_step(state, record) in shifted: + edge_hits += 1 + return ({to_rows_integer(state) for state in ball}, layers, + {to_rows_integer(record[0]) for record in records}, (base_hits, edge_hits)) diff --git a/research/coordinate-cnot-address-spectator/test_verify.py b/research/coordinate-cnot-address-spectator/test_verify.py new file mode 100644 index 0000000000..6df00104f5 --- /dev/null +++ b/research/coordinate-cnot-address-spectator/test_verify.py @@ -0,0 +1,153 @@ +"""Mathematical and fail-closed checks for the scoped certificate. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +Apache-2.0. +""" +import contextlib +import copy +import importlib.util +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +spec = importlib.util.spec_from_file_location("spectator_verify", HERE / "verify.py") +V = importlib.util.module_from_spec(spec) +spec.loader.exec_module(V) +I = V.load_independent() + + +@contextlib.contextmanager +def exported_package(): + with tempfile.TemporaryDirectory(prefix="address-spectator-test-") as directory: + root = Path(directory) + package = root / "research" / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + for item in json.loads((HERE / "SOURCES.json").read_text())["files"]: + if item["usage"] == "input": + dest = root / item["path"] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(ROOT / item["path"], dest) + try: + yield root, package + finally: + # Restore only the temporary files this fixture created. + for path in root.rglob("*"): + path.chmod(0o755 if path.is_dir() else 0o644) + root.chmod(0o755) + + +def execute(package, root): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py")], + cwd=root, text=True, capture_output=True, timeout=120) + + +class CertificateChecks(unittest.TestCase): + def test_algebra_natural_map_and_dense_updates(self): + """Check the matrix-image implication on the complete two-call alphabet.""" + for r in (2, 3): + n = 3 * r + gates = V.generators(r) + eye = V.identity(n) + images = [V.step(eye, gate, n) for gate in gates] + # Dense input catches bit-packing mistakes hidden by the identity. + dense = sum(1 << (row * n + col) for row in range(n) for col in range(n) + if (row * 7 + col * 11 + row * col) % 5 < 3) + for gate, image in zip(gates, images): + self.assertEqual(V.step(dense, gate, n), V.matrix_product(image, dense, n)) + self.assertEqual(V.natural_image(V.formal_evaluate([gate], r), r), image) + for first, first_image in zip(gates, images): + formal = V.formal_evaluate([first], r) + for second in gates: + self.assertEqual(V.natural_image(V.formal_step(formal, second, r), r), + V.step(first_image, second, n)) + + def test_algebra_free_scalar_conjugation_closure(self): + for r in (2, 3): + mask = (1 << r) - 1 + invertibles = [code for code in range(1 << (r * r)) + if I.rank([(code >> (k * r)) & mask for k in range(r)]) == r] + projectors = {p for _, _, p in V.projectors(r)} + for basis in invertibles: + inverse = next(q for q in invertibles + if V.matrix_product(basis, q, r) == V.identity(r)) + for p in projectors: + transformed = V.matrix_product(V.matrix_product(basis, p, r), inverse, r) + self.assertIn(transformed, projectors) + self.assertEqual(len(invertibles), {2: 6, 3: 168}[r]) + + def test_independent_projectors_and_address_group(self): + # Independently enumerate all 512 possible binary address matrices. + address_group = {code for code in range(512) + if I.rank([(code >> (3 * row)) & 7 for row in range(3)]) == 3} + self.assertEqual(len(address_group), 168) + address_gates = [V.identity(3) ^ (1 << (i * 3 + j)) + for i in range(3) for j in range(3) if i != j] + reached = {V.identity(3)} + while True: + new = {V.matrix_product(a, b, 3) for a in reached for b in address_gates} + if new <= reached: + break + reached |= new + self.assertEqual(reached, address_group) + for r in (2, 3): + other = {sum(row << (k * r) for k, row in enumerate(rows)) + for rows in I.all_projectors(r)} + self.assertEqual(other, {p for _, _, p in V.projectors(r)}) + + def test_receipt_mutations(self): + expected = json.loads((HERE / "EXPECTED.json").read_text()) + mutants = [] + for key, value in (("edge_intersection", 1), ("generators", 167), + ("address_dimension", 2), ("registers", 4), + ("minimum_paid_calls", 5), ("edge_attempts_per_engine", 0), + ("ball_2_sha256", "0" * 64)): + mutant = copy.deepcopy(expected) + mutant["cases"][1][key] = value + mutants.append(mutant) + mutant = copy.deepcopy(expected) + mutant["cases"].pop() + mutants.append(mutant) + for mutant in mutants: + with self.assertRaisesRegex(ValueError, "receipt mismatch"): + V.check_receipt(expected, mutant) + + def test_real_receipt_corruption_rejected(self): + with exported_package() as (root, package): + path = package / "EXPECTED.json" + bad = json.loads(path.read_text()) + bad["cases"][1]["edge_intersection"] = 1 + path.write_text(json.dumps(bad)) + result = execute(package, root) + self.assertNotEqual(result.returncode, 0) + self.assertIn("receipt mismatch", result.stderr) + + def test_real_source_corruption_rejected(self): + with exported_package() as (root, package): + item = next(x for x in json.loads((package / "SOURCES.json").read_text())["files"] + if x["usage"] == "input") + path = root / item["path"] + path.write_bytes(path.read_bytes() + b"\nsource mutation\n") + result = execute(package, root) + self.assertNotEqual(result.returncode, 0) + self.assertIn("source pin mismatch", result.stderr) + + def test_read_only_relocated_optimized_replay(self): + with exported_package() as (root, package): + for path in root.rglob("*"): + path.chmod(0o555 if path.is_dir() else 0o444) + root.chmod(0o555) + result = execute(package, root) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_COORDINATE_CNOT_ADDRESS_SPECTATOR", result.stdout) + self.assertNotIn("Traceback", result.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/coordinate-cnot-address-spectator/verify.py b/research/coordinate-cnot-address-spectator/verify.py new file mode 100644 index 0000000000..9a47ec0557 --- /dev/null +++ b/research/coordinate-cnot-address-spectator/verify.py @@ -0,0 +1,307 @@ +#!/usr/bin/env python3 +"""Exact two-SWAP lower bound with a third address coordinate. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +Apache-2.0. No predecessor implementation is imported. + +The natural representation is used ONLY to reject short formal words. +The attaining word is checked separately in the formal group algebra. +""" +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ADDRESS_DIMENSION = 3 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + """Binary n-by-n matrix, consecutive n-bit rows, row zero first.""" + return sum(1 << (i * n + i) for i in range(n)) + + +def matrix_product(left, right, n): + result = 0 + mask = (1 << n) - 1 + for i in range(n): + selectors = (left >> (i * n)) & mask + row = 0 + while selectors: + bit = selectors & -selectors + row ^= (right >> ((bit.bit_length() - 1) * n)) & mask + selectors ^= bit + result |= row << (i * n) + return result + + +def projectors(r): + """All binary rank-one idempotents, with their unique binary u,v.""" + return [ + (u, v, sum(v << (k * r) for k in range(r) if u >> k & 1)) + for u in range(1, 1 << r) + for v in range(1, 1 << r) + if (u & v).bit_count() % 2 == 1 + ] + + +def generators(r): + n = r * ADDRESS_DIMENSION + return [ + { + "u": u, "v": v, "projector": p, "i": i, "j": j, + "source_shifts": tuple(n * (k * 3 + j) for k in range(r) if v >> k & 1), + "scatter": sum(1 << (n * (k * 3 + i)) for k in range(r) if u >> k & 1), + } + for u, v, p in projectors(r) + for i in range(3) for j in range(3) if i != j + ] + + +def step(state, gate, n): + """Left multiply by I + (uv^T) tensor E_ij, without a dense multiply.""" + row = 0 + for shift in gate["source_shifts"]: + row ^= state >> shift + # The repeated n-bit blocks do not overlap, so multiplication is XOR here. + return state ^ ((row & ((1 << n) - 1)) * gate["scatter"]) + + +def target_left(state, r, active=2): + """Left multiply by diag(s12,...,s12,I,...,I).""" + n = 3 * r + mask = (1 << n) - 1 + for k in range(active): + a, b = n * (3 * k), n * (3 * k + 1) + delta = ((state >> a) ^ (state >> b)) & mask + state ^= (delta << a) ^ (delta << b) + return state + + +def ball_two(r, gates): + n = 3 * r + seen = {identity(n)} + frontier = set(seen) + layers = [1] + for _ in range(2): + new = {step(state, gate, n) for state in frontier for gate in gates} - seen + layers.append(len(new)) + seen.update(new) + frontier = new + return seen, layers + + +def intersection_scan(r, gates, ball, active=2): + """Stream every B2 -> B3 edge; no truncation, sampling or heuristic pruning.""" + shifted = {target_left(state, r, active) for state in ball} + base_hits = len(ball & shifted) + edge_hits = 0 + for state in ball: + for gate in gates: + if step(state, gate, 3 * r) in shifted: + edge_hits += 1 + return base_hits, edge_hits + + +def digest_states(states, n): + width = (n * n + 7) // 8 + h = hashlib.sha256() + for state in sorted(states): + h.update(state.to_bytes(width, "little")) + return h.hexdigest() + + +def formal_step(state, gate, r): + """Full F2[GL3(F2)] coefficients: group-matrix label -> scalar matrix.""" + g = identity(3) ^ (1 << (gate["i"] * 3 + gate["j"])) + out = dict(state) + for label, coefficient in state.items(): + delta = matrix_product(gate["projector"], coefficient, r) + for new_label in (label, matrix_product(g, label, 3)): + out[new_label] = out.get(new_label, 0) ^ delta + return {label: coefficient for label, coefficient in out.items() if coefficient} + + +def direct_word(r): + gates = generators(r) + return [next(g for g in gates if g["u"] == g["v"] == 1 << k + and (g["i"], g["j"]) == pair) + for k in range(2) for pair in ((0, 1), (1, 0), (0, 1))] + + +def formal_target(r, active=2): + p = sum(1 << (k * r + k) for k in range(active)) + s = (1 << 1) | (1 << 3) | (1 << 8) + result = {s: p, identity(3): identity(r) ^ p} + return {g: c for g, c in result.items() if c} + + +def formal_evaluate(word, r): + state = {identity(3): identity(r)} + for gate in word: + state = formal_step(state, gate, r) + return state + + +def natural_image(formal, r): + n = 3 * r + out = 0 + for label, coefficient in formal.items(): + for row in range(r): + for col in range(r): + if coefficient >> (row * r + col) & 1: + for i in range(3): + for j in range(3): + if label >> (i * 3 + j) & 1: + out ^= 1 << ((row * 3 + i) * n + col * 3 + j) + return out + + +def check_sources(): + source = json.loads((HERE / "SOURCES.json").read_text()) + for item in source["files"]: + if item["usage"] == "input": + require(hashlib.sha256((ROOT / item["path"]).read_bytes()).hexdigest() + == item["sha256"], "source pin mismatch: " + item["path"]) + + +def load_independent(): + spec = importlib.util.spec_from_file_location("spectator_independent", HERE / "independent.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def controls(r, ball, gates): + """Boundary and model controls, not tests of implementation spelling.""" + n = 3 * r + word = direct_word(r) + target = formal_target(r) + names = [] + for k in range(6): + require(formal_evaluate(word[:k] + word[k + 1:], r) != target, + "omitted call was not rejected") + names.append("omit_call_" + str(k)) + bad = list(word) + bad[0] = next(g for g in gates if g["u"] == g["v"] == 1 and (g["i"], g["j"]) == (0, 2)) + require(formal_evaluate(bad, r) != target, "spectator substitution was not rejected") + names.append("wrong_spectator_label") + + # Forgetting the spectator's restoration would accept this altered endpoint. + spectator = next(g for g in gates if g["u"] == g["v"] == 1 and (g["i"], g["j"]) == (2, 0)) + bad_endpoint = formal_evaluate(word + [spectator], r) + require(bad_endpoint != target, "unrestored address coordinate accepted") + mask = sum(((1 << n) - 1) << (row * n) for row in range(n) if row % 3 != 2) + require((natural_image(bad_endpoint, r) ^ natural_image(target, r)) & mask == 0, + "spectator control does not preserve visible rows") + names.append("unrestored_address_spectator") + + if r == 3: + dirty_gate = next(g for g in gates if g["u"] == g["v"] == 4 and (g["i"], g["j"]) == (0, 1)) + leak = formal_evaluate(word + [dirty_gate], r) + require(leak != target, "dirty register not restored") + clean_columns = sum(1 << (row * n + col) for row in range(n) for col in range(6)) + require((natural_image(leak, r) ^ natural_image(target, r)) & clean_columns == 0, + "clean-only control fixture is invalid") + names.append("clean_only_dirty_register_fault") + + # A natural representation is not faithful on the group algebra. + a = identity(3) ^ (1 << 1) + b = identity(3) ^ (1 << 3) + group = {identity(3), a, b, matrix_product(a, b, 3), matrix_product(b, a, 3), + matrix_product(matrix_product(a, b, 3), a, 3)} + kernel = {g: 1 for g in group} + require(len(group) == 6 and kernel and natural_image(kernel, r) == 0, + "nonfaithfulness control is invalid") + altered = dict(target) + for label in kernel: + altered[label] = altered.get(label, 0) ^ 1 + altered = {g: c for g, c in altered.items() if c} + require(altered != target and natural_image(altered, r) == natural_image(target, r), + "natural equality incorrectly accepted as formal equality") + names.append("nonfaithful_natural_representation") + + one = target_left(identity(n), r, active=1) + require(one not in ball, "one swap incorrectly found within two calls") + p, q = intersection_scan(r, gates, ball, active=1) + require(p + q > 0, "positive one-swap endpoint not recovered") + require(identity(n) in ball, "identity missing from ball") + names.extend(["one_swap_positive", "identity_positive"]) + + p2 = sum(1 << (k * r + k) for k in range(2)) + enlarged = [dict(word[k], projector=p2) for k in range(3)] + require(formal_evaluate(enlarged, r) == target, "rank-two alphabet control invalid") + require(all(g["projector"] != p2 for g in gates), "rank-two projector admitted") + names.append("rank_two_unit_price_outside_alphabet") + return names + + +def compute_receipt(): + independent = load_independent() + rows = [] + for r in (2, 3): + gates = generators(r) + expected_projectors = (1 << (r - 1)) * ((1 << r) - 1) + require(len(projectors(r)) == expected_projectors, "incomplete projector domain") + require(len(gates) == 6 * expected_projectors, "incomplete gate domain") + for g in gates: + require(matrix_product(g["projector"], g["projector"], r) == g["projector"], + "non-idempotent paid projector") + require(step(step(identity(3 * r), g, 3 * r), g, 3 * r) == identity(3 * r), + "paid gate is not an involution") + ball, layers = ball_two(r, gates) + base_hits, edge_hits = intersection_scan(r, gates, ball) + require(base_hits == edge_hits == 0, "a natural-image short candidate exists; formal check required") + other_ball, other_layers, other_generators, other_hits = independent.census(r) + require(other_ball == ball and other_layers == layers, "independent complete ball mismatch") + require(other_generators == {step(identity(3 * r), g, 3 * r) for g in gates}, + "independent alphabet mismatch") + require(other_hits == (0, 0), "independent intersection mismatch") + target = formal_target(r) + require(formal_evaluate(direct_word(r), r) == target, "formal six-call witness failed") + require(natural_image(target, r) == target_left(identity(3 * r), r), "target representation mismatch") + control_names = controls(r, ball, gates) + rows.append({ + "registers": r, "address_dimension": 3, "projectors": expected_projectors, + "generators": len(gates), "exact_distance_layers_0_1_2": layers, + "ball_2_size": len(ball), "ball_2_sha256": digest_states(ball, 3 * r), + "shifted_ball_2_sha256": digest_states({target_left(s, r) for s in ball}, 3 * r), + "base_intersection": base_hits, "edge_intersection": edge_hits, + "edge_attempts_per_engine": len(ball) * len(gates), + "independent_complete_ball_and_alphabet_equal": True, + "formal_upper_bound": 6, "minimum_paid_calls": 6, + "controls": control_names, + }) + return {"schema_version": 1, "result": "finite_lower_bound_plus_formal_upper_bound", + "model": "M_r(F2[GL_3(F2)]); all six coordinate CNOTs; r=2,3", + "no_new_kappa": True, "cases": rows} + + +def check_receipt(actual, expected): + require(actual == expected, "receipt mismatch") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print recomputed receipt, do not write it") + args = parser.parse_args() + check_sources() + receipt = compute_receipt() + if args.emit: + print(json.dumps(receipt, indent=2, sort_keys=True)) + else: + check_receipt(receipt, json.loads((HERE / "EXPECTED.json").read_text())) + count = sum(len(case["controls"]) for case in receipt["cases"]) + print("PASS_COORDINATE_CNOT_ADDRESS_SPECTATOR minimum=6 registers=2,3 " + f"address_dimension=3 controls={count} no_new_kappa") + + +if __name__ == "__main__": + main()