From 9e1640094f649ba6db9742796825a8d6c238989b Mon Sep 17 00:00:00 2001 From: commdata2338 <199849969+commdata2338@users.noreply.github.com> Date: Tue, 13 Oct 2026 19:29:16 -0500 Subject: [PATCH] Research: six-call floor for two coordinate swaps with dirty registers In the formal F2[GL_2(F2)] register model with free scalar mixing, paid coordinate-CNOT address calls and any finite number of restored dirty registers, two coordinate-SWAP targets need exactly six paid calls: a sign-trace argument forces even length, coefficient ranks exclude four calls, and a six-call word attains the bound. Exhaustive formal censuses for two and three registers agree. This settles the smallest two-dimensional instance of PR #1333's restricted-alphabet question. No new kappa. Adds research/coordinate-cnot-register-bound/ only. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). --- .../EXPECTED.json | 269 ++++++++++++++++ .../OVERLAP.json | 122 ++++++++ .../coordinate-cnot-register-bound/PROOF.md | 221 +++++++++++++ .../coordinate-cnot-register-bound/README.md | 150 +++++++++ .../SOURCES.json | 44 +++ .../coordinate-cnot-register-bound/TASK.json | 87 ++++++ .../VALIDATION.md | 42 +++ .../VERIFY.json | 31 ++ .../independent.py | 216 +++++++++++++ .../test_verify.py | 116 +++++++ .../coordinate-cnot-register-bound/verify.py | 293 ++++++++++++++++++ 11 files changed, 1591 insertions(+) create mode 100644 research/coordinate-cnot-register-bound/EXPECTED.json create mode 100644 research/coordinate-cnot-register-bound/OVERLAP.json create mode 100644 research/coordinate-cnot-register-bound/PROOF.md create mode 100644 research/coordinate-cnot-register-bound/README.md create mode 100644 research/coordinate-cnot-register-bound/SOURCES.json create mode 100644 research/coordinate-cnot-register-bound/TASK.json create mode 100644 research/coordinate-cnot-register-bound/VALIDATION.md create mode 100644 research/coordinate-cnot-register-bound/VERIFY.json create mode 100644 research/coordinate-cnot-register-bound/independent.py create mode 100644 research/coordinate-cnot-register-bound/test_verify.py create mode 100644 research/coordinate-cnot-register-bound/verify.py diff --git a/research/coordinate-cnot-register-bound/EXPECTED.json b/research/coordinate-cnot-register-bound/EXPECTED.json new file mode 100644 index 0000000000..23c1950489 --- /dev/null +++ b/research/coordinate-cnot-register-bound/EXPECTED.json @@ -0,0 +1,269 @@ +{ + "censuses": [ + { + "active_targets": 2, + "ball2_sha256": "28080106e83ff37e778fafd6566b5e0bfcbff830f0d7a25dcaff4a80405e03f9", + "ball2_size": 93, + "ball3_sha256": "2ff2b469b406a15c94c8e16c55a6a5a6d79b4199af25c2c48e353170e21f14ba", + "ball3_size": 559, + "direct_six_call_word": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 5 + ], + [ + 1, + 1, + 1 + ], + [ + 2, + 2, + 1 + ], + [ + 2, + 2, + 5 + ], + [ + 2, + 2, + 1 + ] + ], + "exact_distance_layers_0_to_3": [ + 1, + 12, + 80, + 466 + ], + "independent_dense": { + "directed_transition_attempts": 1116, + "exact_distance_layers_0_to_3": [ + 1, + 12, + 80, + 466 + ], + "regular_dimension": 12 + }, + "intersections_through_five": 0, + "inverse_ball2_times_target_sha256": "3ae2db98c42806bbfa4c3b0b82016c363a4fed9f32fc11d51fb1650f7bd7cc8f", + "minimum_paid_calls": 6, + "paid_generators": 12, + "positive_identity_and_one_swap_minima": [ + 0, + 3 + ], + "registers": 2, + "restored_dirty_registers": 0, + "scalar_rank_one_idempotents": 6 + }, + { + "active_targets": 2, + "ball2_sha256": "05521fd538449613da5686c55be67e9d5b1b1996699108ee6a36d4fe16c49f5b", + "ball2_size": 1807, + "ball3_sha256": "20636f0fc14cad71957ddfdbdeea96a9601c2b6db37b5e914788c75b23fabce9", + "ball3_size": 47203, + "direct_six_call_word": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 5 + ], + [ + 1, + 1, + 1 + ], + [ + 2, + 2, + 1 + ], + [ + 2, + 2, + 5 + ], + [ + 2, + 2, + 1 + ] + ], + "exact_distance_layers_0_to_3": [ + 1, + 56, + 1750, + 45396 + ], + "independent_dense": { + "directed_transition_attempts": 101192, + "exact_distance_layers_0_to_3": [ + 1, + 56, + 1750, + 45396 + ], + "regular_dimension": 18 + }, + "intersections_through_five": 0, + "inverse_ball2_times_target_sha256": "20d752478e73028216184ca610ff5e901d07d7d48cd89b6989a9d3677abeb22f", + "minimum_paid_calls": 6, + "paid_generators": 56, + "positive_identity_and_one_swap_minima": [ + 0, + 3 + ], + "registers": 3, + "restored_dirty_registers": 1, + "scalar_rank_one_idempotents": 28 + } + ], + "checked_context_inputs": [ + "research/bit-three-register-lower-bound/README.md" + ], + "controls": [ + "omitted_call_0", + "omitted_call_1", + "omitted_call_2", + "omitted_call_3", + "omitted_call_4", + "omitted_call_5", + "wrong_address_label", + "unrestored_dirty_register", + "clean_only_dirty_leakage", + "nonidentity_scalar_augmentation", + "rank_two_projector_underpricing", + "uncharged_address_alphabet_expansion", + "nonfaithful_natural_representation", + "address_multiplication_order" + ], + "format": "coordinate-cnot-register-bound-v1", + "group_permutations": [ + [ + 0, + 1, + 2 + ], + [ + 0, + 2, + 1 + ], + [ + 1, + 0, + 2 + ], + [ + 1, + 2, + 0 + ], + [ + 2, + 0, + 1 + ], + [ + 2, + 1, + 0 + ] + ], + "labels": { + "a": 1, + "b": 5, + "identity": 0, + "swap": 2 + }, + "scalar_normalization_checks": { + "conjugations": 4704, + "gl3_matrices": 168, + "rank_one_idempotents": 28 + }, + "symbolic_proof_checks": { + "four_call_patterns": [ + { + "identity": "swap coefficient zero", + "word": "aaaa" + }, + { + "identity": "swap coefficient zero", + "word": "aaab" + }, + { + "identity": "swap coefficient has a common rank-one exterior factor", + "word": "aaba" + }, + { + "identity": "swap coefficient zero", + "word": "aabb" + }, + { + "identity": "swap coefficient has a common rank-one exterior factor", + "word": "abaa" + }, + { + "identity": "swap plus reverse-pair coefficient is N1 N2", + "word": "abab" + }, + { + "identity": "swap coefficient has a common rank-one exterior factor", + "word": "abba" + }, + { + "identity": "swap coefficient zero", + "word": "abbb" + }, + { + "identity": "swap coefficient zero", + "word": "baaa" + }, + { + "identity": "swap coefficient has a common rank-one exterior factor", + "word": "baab" + }, + { + "identity": "swap plus reverse-pair coefficient is N1 N2", + "word": "baba" + }, + { + "identity": "swap coefficient has a common rank-one exterior factor", + "word": "babb" + }, + { + "identity": "swap coefficient zero", + "word": "bbaa" + }, + { + "identity": "swap coefficient has a common rank-one exterior factor", + "word": "bbab" + }, + { + "identity": "swap coefficient zero", + "word": "bbba" + }, + { + "identity": "swap coefficient zero", + "word": "bbbb" + } + ], + "sign_homomorphism_products": 36, + "symbolic_label_patterns_through_four": 31 + } +} diff --git a/research/coordinate-cnot-register-bound/OVERLAP.json b/research/coordinate-cnot-register-bound/OVERLAP.json new file mode 100644 index 0000000000..36e93a819c --- /dev/null +++ b/research/coordinate-cnot-register-bound/OVERLAP.json @@ -0,0 +1,122 @@ +{ + "checked_at": "2026-10-14T00:18:57.227036+00:00", + "mode": "offline complete-pagination snapshots; later changes can be missing", + "entry_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T00:01:47.697042+00:00", + "complete_pagination": true, + "records": 861 + }, + "discussions": { + "fetched_at": "2026-10-14T00:02:09.289249+00:00", + "complete_pagination": true, + "records": 108 + } + }, + "final_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T00:12:16.081794+00:00", + "complete_pagination": true, + "records": 864 + }, + "discussions": { + "fetched_at": "2026-10-14T00:12:33.355089+00:00", + "complete_pagination": true, + "records": 119 + } + }, + "queries": [ + [ + "--task", + "bit-new-register-model" + ], + [ + "--task", + "bit-helper-contract" + ], + [ + "coordinate CNOT", + "coordinate-CNOT", + "swap target", + "binary-affine-register" + ], + [ + "--task", + "bit-new-register-model" + ], + [ + "coordinate CNOT", + "coordinate-CNOT", + "two swaps", + "six-call", + "binary-affine-register" + ] + ], + "nearest": [ + { + "number": 1333, + "title": "Research theorem: exact paid cost for binary affine register words", + "kind": "pr", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1333", + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "updated_at": "2026-10-13T22:57:25Z" + }, + { + "number": 1317, + "title": "Binary affine addresses: exact paid-call floor with arbitrary dirty registers", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317", + "updated_at": "2026-10-14T00:06:50Z" + }, + { + "number": 720, + "title": "Research theorem: nine-call bound for arbitrary invertible three-register targets", + "kind": "pr", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/720", + "head": "a942c0ae1b463710ca535c1fba1b07b6431b5a86", + "updated_at": "2026-10-13T04:45:45Z" + }, + { + "number": 1317, + "title": "Binary affine addresses: exact paid-call floor with arbitrary dirty registers", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18911765", + "updated_at": "2026-10-14T00:06:50Z" + }, + { + "number": 705, + "title": "Research: determinant obstruction for rank-homogeneous register paths (no kappa)", + "kind": "pr", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/705", + "head": "eeb0cd605415a73b792915aaa9185000f293c84a", + "updated_at": "2026-10-13T04:33:58Z" + }, + { + "number": 836, + "title": "Research: signed rank transport excludes unitary register mixers (no new kappa)", + "kind": "pr", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/836", + "head": "7ae9124f59694bb1e5acf2ae99c65e63c115b2f4", + "updated_at": "2026-10-13T06:52:56Z" + }, + { + "number": 800, + "title": "Research: weighted path valuations exclude a remaining eight-call Clifford word (no kappa)", + "kind": "pr", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/800", + "head": "d7d83e0a9b98f95a4443d1060336be267ac3fd80", + "updated_at": "2026-10-13T05:53:19Z" + }, + { + "number": 680, + "title": "Scoped negative result: certify 33 fixed Clifford register words (no kappa claim)", + "kind": "pr", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/680", + "head": "c3a5b6b7afec35d259c29bc2d8bb8516e975ad31", + "updated_at": "2026-10-13T03:49:15Z" + } + ], + "novelty_limit": "Titles/bodies, discussions, local top-level notes and ledger only; no exhaustive code-diff search or novelty certificate.", + "scope_difference": "PR1333 prices every affine homogeneous-rank-one address label as one unit, including the swap. This result restricts labels to the two coordinate CNOTs and proves exact cost six for two swaps with any finite number of restored dirty registers. Other listed register results concern rational abelian or Clifford/complex address alphabets.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18911765" +} diff --git a/research/coordinate-cnot-register-bound/PROOF.md b/research/coordinate-cnot-register-bound/PROOF.md new file mode 100644 index 0000000000..68fee5b5cc --- /dev/null +++ b/research/coordinate-cnot-register-bound/PROOF.md @@ -0,0 +1,221 @@ +# Two coordinate swaps cost exactly six calls + +This is a scoped theorem about a formal nonabelian register model. The proof +below holds for any finite number of restored dirty registers. The finite +censuses corroborate the proof and its implementation; they are not its +all-register justification. + +## 1. Complete model and statement + +Let `G = GL_2(F2)`, acting on two binary address coordinates, and let +`R = F2[G]` be its **formal group algebra**. Write + +\[ + a=\begin{pmatrix}1&1\\0&1\end{pmatrix},\qquad + b=\begin{pmatrix}1&0\\1&1\end{pmatrix},\qquad + s=\begin{pmatrix}0&1\\1&0\end{pmatrix}=aba=bab. +\] + +These are the two coordinate CNOTs and the coordinate swap. They are distinct +involutions; `ab != ba`. Products are matrix products, so the rightmost map +acts first. The six group elements are `1,a,b,ab,ba,s`. + +For any finite `r >= 2`, a register word is an `r` by `r` matrix over `R`. +The complete allowed alphabet is: + +* A free scalar basis change `B in GL_r(F2)`, embedded using the identity + group label. This grants all scalar XOR preparation and restoration for + free, an optimistic paid-call relaxation. +* A paid unit + \[ + D_N(g)=I+([g]+1)N,\qquad + g\in\{a,b\},\quad N=uv^T,\quad v^Tu=1, + \] + with binary `u,v`. Thus `N` is a rank-one idempotent. Each occurrence + costs one, including undo operations. + +There are no free address transformations, translations, copies, erasures, +or clean allocations. The `r-2` additional registers start arbitrarily dirty +and must be returned identically; no effect of their inputs may leak to an +active output. Their availability is otherwise free in this relaxation. + +Put `P=diag(1,1,0,...,0)`. The required endpoint is the formal identity + +\[ + T=\operatorname{diag}([s],[s],1,\ldots,1) + =I+([s]+1)P. \tag{1} +\] + +Equality in `M_r(R)` is required, not equality in the two-dimensional +address-matrix representation. In particular, it implies the boundary on +every `R`-module and arbitrary register inputs. + +**Theorem.** For every finite `r >= 2`, the minimum paid-call count for (1) +is exactly **six**. Arbitrarily many restored dirty registers and arbitrary +free scalar mixing do not reduce the direct `3+3` bill in this alphabet. + +This changes the address algebra of the rational abelian starting model. It +does not reduce rational frame entries modulo two and does not establish a +physical bit supplier or a multiplication exponent. + +## 2. Normalize free scalar operations + +Moving scalar basis changes to the right conjugates each `N` by an invertible +binary scalar matrix. Rank one and idempotence are preserved, and `g` remains +`a` or `b`. Any word becomes a product of the same number of paid units, +followed by one scalar matrix `B_total`. + +The augmentation `R -> F2`, `[g] -> 1`, sends every paid factor to `I` and +sends (1) to `I`. Consequently `B_total=I`. It suffices to consider products +of paid units alone. This does not normalize away address transformations; +none are available for free in the stated alphabet. + +## 3. The number of paid calls is even + +The action of `G` on its three nonzero address vectors identifies it with +`S_3`. Its sign homomorphism sends each of `a,b,s` to the nonidentity element +`t` of `C_2`. In characteristic two, + +\[ + \mathbb F_2[C_2]\cong\mathbb F_2[\epsilon]/(\epsilon^2),\qquad + t=1+\epsilon. +\] + +Apply this group-algebra homomorphism to the normalized word. Each paid factor +becomes `I+epsilon N_j`; the product is exactly +`I+epsilon sum_j N_j`, because `epsilon^2=0`. The target becomes +`I+epsilon P`. Thus + +\[ + \sum_j N_j=P. +\] + +Taking the binary trace gives + +\[ + \#\text{calls}\equiv\sum_j\operatorname{tr}N_j + =\operatorname{tr}P=0\pmod2, +\] + +since `tr(uv^T)=v^Tu=1`. Any improvement on six must therefore use zero, +two or four calls. The zero- and two-call words have no `[s]` coefficient: +`s` has length three in the generators `a,b`. + +## 4. Every four-call label pattern fails + +Write `x=[a]+1`, `y=[b]+1`. These commute with scalar matrices (not with +one another), and `x^2=y^2=0`. + +### At most three runs + +A maximal run of one repeated label collapses exactly: + +\[ + (I+xN_1)\cdots(I+xN_k)=I+x(N_1+\cdots+N_k), +\] + +and likewise for `y`. With one or two runs, the support cannot contain `s`. +With three runs the product has the form + +\[ + (I+xA)(I+yB)(I+xC) +\] + +or its label-reversed counterpart. Its `[s]` coefficient is exactly `ABC`. +Four calls distributed among three nonempty runs have run lengths a +permutation of `(2,1,1)`. At least one of the outer runs has length one, +so `A` or `C` is a rank-one original projector. Consequently `rank(ABC)<=1`, +whereas (1) has `[s]` coefficient `P` of rank two. This is a contradiction. + +### Four runs: `abab` or `baba` + +Consider `abab` and define the linear coefficient functional + +\[ + \lambda(f)=\operatorname{coeff}_{[s]}f+ + \operatorname{coeff}_{[ba]}f. +\] + +Applied entrywise to the product, direct formal expansion gives + +\[ + \lambda\big((I+xN_1)(I+yN_2)(I+xN_3)(I+yN_4)\big)=N_2N_3. \tag{2} +\] + +For completeness, among the sixteen selected subsets of positions, the +group-algebra monomial `yx` on positions `(2,3)` is the only one on which +`lambda` is one. Singletons and `xy` have neither coefficient; `x^2=y^2=0`; +both `xyx` and `yxy` contain `[s]` and `[ba]`, so their contributions cancel; +and `xyxy=xy`. This proves (2) without any commutativity assumption on the +`N_j`. The package independently expands these polynomials with noncommuting +formal scalar variables. + +For (1), `lambda(T)=P`. Equation (2) would therefore require +`P=N_2N_3`, which has rank at most one. For `baba`, use the same argument +with `a,b` interchanged and the functional `coeff_[s]+coeff_[ab]`. + +These cases exhaust the sixteen four-call label patterns. Combined with +parity, no word shorter than six reaches (1), for any `r`. + +## 5. Six calls attain the bound with the complete formal boundary + +For any scalar idempotent `N` and group elements `g,h`, expansion gives + +\[ + D_N(g)D_N(h)=D_N(gh). +\] + +Use `a,b,a` on `N=E_11`, followed by `a,b,a` on `N=E_22`. Since `aba=s`, +the product is exactly (1). Every other register is unchanged on arbitrary +dirty input. There are six paid calls, no additional role, no scalar basis +changes, and no omitted restoration operations. Free scalar work was granted +only in the lower-bound relaxation; the attaining word does not need it. + +Allowing `s` itself as a paid unit would instead cost two calls, as in the +broader affine rank-priced model of PR1333. Allowing a rank-two scalar +projector at unit price would cost three calls. Both are outside this +alphabet, and both appear as explicit scope controls in the verifier. + +## 6. What the finite replay does and does not prove + +For `r=2,3`, enumerate every binary rank-one idempotent and both labels. +Their counts are `6,28` and therefore `12,56` paid generators. Each generator +is an involution. A breadth-first traversal constructs exact formal balls +`B_2,B_3`. A word of length at most five reaches `T` exactly when + +\[ + \{p^{-1}T:p\in B_2\}\cap B_3\ne\varnothing. +\] + +Both intersections are empty. A shorter word can always be split into a +prefix of length at most two and suffix of length at most three; repeated +states are retained at their shortest distance. Thus deduplication does not +discard an endpoint or length. The six-call witness supplies the upper bound. + +A separate implementation enumerates all binary scalar matrices, filters +rank-one idempotents, and multiplies full `12x12` or `18x18` binary matrices +in the **faithful left regular representation** of the group algebra. It +generates the address group from actual binary `2x2` matrices, not the first +implementation's permutation table, and expands from the opposite side. +The complete state sets and exact distance layers agree, not just a few +columns or aggregate counts. The written argument in Sections 2-5 is what +extends the conclusion beyond those two finite register counts. + +This proof is not Lean-checked, and no independent human proof review is +claimed. Physical compilation, common-label realization, hosting, precision, +tape and analytic transfer remain outside this scoped result. + +## Attribution + +Gareth Davidson (@bitplane), PR1333 at +`7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2`, posed the restricted coordinate-CNOT +direction after proving the broader affine-rank-priced theorem. That theorem's +augmentation/free-scalar normalization is reused as an argument, with credit; +none of its implementation is imported. The contribution here is the +two-swap six-call obstruction in the restricted alphabet, including the +sign-trace and four-label coefficient argument and two independent finite +implementations. Eumemic (PR288), Ali Romman (PR468) and David Govea (PR720) +are credited for the surrounding register-model and rational-address work. +No new general rank principle or literature-priority claim is made. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. diff --git a/research/coordinate-cnot-register-bound/README.md b/research/coordinate-cnot-register-bound/README.md new file mode 100644 index 0000000000..cdcc5a9e7f --- /dev/null +++ b/research/coordinate-cnot-register-bound/README.md @@ -0,0 +1,150 @@ +# Two coordinate swaps need six paid coordinate-CNOT calls + +**Scoped theorem; no new kappa.** Two coordinate-SWAP targets require exactly +six paid coordinate-CNOT address calls, even with arbitrarily many restored +dirty registers and free scalar register mixing, in the explicit formal model +below. [PROOF.md](PROOF.md) gives the written all-register proof. Two independent +finite implementations corroborate its smallest cases. + +This answers the smallest two-dimensional gap instance of Gareth Davidson's +[PR1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333) first open +question. His broader affine rank-priced alphabet admits the swap as a single +unit and therefore prices these two targets at two. Restricting the alphabet +to the two coordinate CNOTs gives a direct bill of six; the result here proves +that mixing registers cannot lower it. The higher-dimensional question remains +open. + +## Exact alphabet and endpoint + +Let `R=F2[GL_2(F2)]` be the formal group algebra, with + +```text +a = [[1,1],[0,1]], b = [[1,0],[1,1]], s = aba = bab = [[0,1],[1,0]]. +``` + +For every finite `r>=2`, allow free scalar `GL_r(F2)` basis changes and paid +unit calls `I+([g]+1)N`, where `g` is **only a or b**, and `N=uv^T` is a binary +rank-one idempotent (`v^T u=1`). Require the complete formal boundary +`diag([s],[s],1,...,1)` on arbitrary register inputs. Every extra register is +dirty and restored. There are no free address maps, translations, copies, +erasures or clean allocations. Undo calls are charged. + +Free scalar normalization follows the augmentation argument credited to +PR1333. The new lower bound uses the sign quotient of `GL_2(F2)` to force an +even call count. Every four-call label pattern then fails a coefficient-rank +test: in the alternating case, the sum of the swap and reverse-pair +coefficients is a product of two rank-one projectors, whereas the target +requires rank two. Six direct calls attain the full formal endpoint with no +additional roles or scalar operations. + +This is an optimistic paid-call relaxation, not a physically admitted supplier. +The formal nonabelian address algebra differs from the retained rational +abelian three-register model; no rational entries are reduced modulo two. + +## Exact checks + +| Registers | Dirty extras | Paid generators | Exact distance layers 0,1,2,3 | Ball through 3 | Meets a two-call inverse ball at the target | +| --- | --- | --- | --- | --- | --- | +| 2 | 0 | 12 | 1, 12, 80, 466 | 559 | 0 | +| 3 | 1 | 56 | 1, 56, 1750, 45396 | 47203 | 0 | + +Every word of length at most five splits into a prefix of length at most two +and a suffix of length at most three. These empty intersections therefore +certify the finite lower bounds without enumerating all literal five-call +words. The six-call witnesses are checked in the full formal algebra. + +`verify.py` encodes all six formal coefficients per entry. `independent.py` +instead constructs binary address matrices, enumerates all scalar matrices +to find idempotents, and multiplies complete 12- or 18-dimensional matrices +in the faithful left regular representation. Their **entire state sets and +distance layers agree**. The second implementation performs 1,116 and 101,192 +directed transition attempts. No natural two-dimensional representation is +used to accept formal equality. + +The replay also checks all 31 label patterns through length four with +noncommuting scalar indeterminates, all 36 sign-homomorphism products, and +all 4,704 conjugations of the 28 projectors by `GL_3(F2)`. Identity and one-swap +meet-in-the-middle controls recover minima zero and three. Fourteen controls +cover each of six omitted calls, a wrong label, dirty-register restoration, +clean-only leakage, a nonidentity scalar residue, rank-two underpricing, +address-alphabet expansion, a nonfaithful representation, and multiplication +order. [EXPECTED.json](EXPECTED.json) records deterministic counts and state-set +hashes. These checks support, but do not replace, the written universal proof. + +## Reproduce + +Python 3.12 and the standard library suffice; no compiler or external package +is needed. From the repository root: + +```sh +python3 -I -B research/coordinate-cnot-register-bound/verify.py +python3 scripts/research_package.py --package research/coordinate-cnot-register-bound --check-only +python3 scripts/research_package.py --package research/coordinate-cnot-register-bound +``` + +Expected direct-replay line: + +```text +PASS_COORDINATE_CNOT_REGISTER_BOUND minimum=6 dirty_registers=arbitrary census_r=2,3 symbolic_patterns=31 controls=14 no_new_kappa +``` + +The registered replay also runs the six focused tests in `test_verify.py`, +including receipt/source corruption rejection and an unchanged read-only +relocated replay under isolated optimized Python. To inspect a newly computed +receipt without writing files, pass `--emit`. State hashes concatenate sorted +formal-state integers encoded in fixed-width little-endian bytes (3 bytes for +two registers, 7 for three). `SOURCES.json` pins the unchanged context input +and task/base provenance; PR1333 text has separate exact contextual pins and +is not a runtime dependency. No predecessor implementation is imported. + +[VALIDATION.md](VALIDATION.md) records the observed local checks and their scope. + +The all-register proof has not been checked in Lean or independently reviewed +by a human. There is no selected-supplier cold replay: physical compilation, +common-label realization, hosting, precision/tape and analytic transfer are +outside this result. The selected record and inherited assumptions are +unchanged. No multiplication-runtime claim follows. + +## Task and overlap + +Base: `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. Card: +`bit-new-register-model`, scope key `7084092dd726e7ba1f2f`, priority revision 2; +chooser nonce `30b6519a75b5dea27cbfaca91b7e00af`. The claim is in +[discussion #1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317). +The initial fixed `r=2,3` question was strengthened to all finite register +counts using the same target and alphabet. [TASK.json](TASK.json) records the +refinement and structured next questions; [OVERLAP.json](OVERLAP.json) records +the searched snapshot coverage and exact neighboring heads. + +PR1333 at `7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2` is the immediate +predecessor. PR468 and David Govea's PR720 at +`a942c0ae1b463710ca535c1fba1b07b6431b5a86` concern rational abelian targets; +they do not cover this alphabet. PR680/705/800/836 concern other formal +Clifford or complex register models. This account's PR1306 addresses XOR +compensation on a fixed dirty shear boundary, a different problem. Neither it +nor the existing helper-interface work is repeated here. + +## Open next questions + +1. **Three or more swaps in the same alphabet.** A general direct-sum bound + would say how far this obstruction scales. Start with three swaps: the + sign trace permits only odd lengths, so seek a seven-call identity or a + coefficient obstruction against the direct nine. Longer alternating words + and arbitrary dirty-register counts require a new argument; the present + four-call proof does not cover them. +2. **A three-dimensional coordinate-CNOT target with a rank/length gap.** + This tests the higher-dimensional branch of PR1333's question. First pin a + target in `GL_3(F2)` and certify its direct coordinate-CNOT length; then + test a two-role formal word below twice that length. Full formal equality + and the complete paid/restoration bill are required. The six-element + group argument here does not apply to that larger address group. + +## Credit and license + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Credit Gareth Davidson (@bitplane) for PR1333's question and augmentation +normalization; eumemic (PR288), Ali Romman (PR468) and David Govea (PR720) +for the surrounding register-model and rational-address work. No new general +rank principle or literature-priority claim is made. New work is Apache-2.0; +predecessor sources and notices remain unchanged. diff --git a/research/coordinate-cnot-register-bound/SOURCES.json b/research/coordinate-cnot-register-bound/SOURCES.json new file mode 100644 index 0000000000..d5d9ccd629 --- /dev/null +++ b/research/coordinate-cnot-register-bound/SOURCES.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "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" + } + ], + "research_context": [ + { + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "path": "research/binary-affine-register-bound/README.md", + "git_blob": "7b68583becf8be6f3cf666b05b0943e7eb99270c", + "sha256": "7951868efdf35fdb2aacdd302ca825cbde0586a5fae6df23aee78e29f30c332a", + "author": "Gareth Davidson (@bitplane)", + "usage": "Research context only; not a runtime dependency or imported implementation." + }, + { + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "path": "research/binary-affine-register-bound/PROOF.md", + "git_blob": "b1152a39b559f7a058489ec74231488e4f8edd83", + "sha256": "36a33434222798434b0a17476ae5f9bc8a2a3891871c46e77cc50ce2e132206b", + "author": "Gareth Davidson (@bitplane)", + "usage": "Research context only; not a runtime dependency or imported implementation." + } + ] +} diff --git a/research/coordinate-cnot-register-bound/TASK.json b/research/coordinate-cnot-register-bound/TASK.json new file mode 100644 index 0000000000..a1748f7e8e --- /dev/null +++ b/research/coordinate-cnot-register-bound/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "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": "Exact minimum of six paid coordinate-CNOT address calls for two coordinate-SWAP targets in M_r(F2[GL_2(F2)]), for every finite r>=2 with arbitrary restored dirty registers and free scalar GL_r(F2) mixing.", + "scope_change_reason": "The card permits a specified nonabelian operation family. PR1333 already settles the broader rank-priced affine model; its first open next question restricts paid labels to coordinate CNOTs. This takes the smallest two-target gap instance and strengthens the initial r=2,3 census to a written all-register proof on that same target.", + "bottleneck_link": "Scoped no-gain side result for a changed address model: in this smallest restricted-alphabet gap, extra dirty registers cannot reduce the direct paid-call bill. This is not a selected supplier or kappa improvement.", + "budget_minutes": 60, + "stop_rule": "Stop when the exact two-SWAP target is resolved or after one bounded pivot; at most 60 minutes with final quarter for validation. No broader register-model search.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-register sign-trace and coefficient-rank argument. EXPECTED.json binds exact r=2,3 formal/dense state-set equality, empty radius-2/radius-3 intersections, a six-call witness, 31 symbolic patterns, 4704 scalar conjugations and 14 boundary controls.", + "author": "commdata2338", + "ai_assistance": "Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. No subagents or independent human review.", + "open_questions": [ + { + "question": "Can three or more coordinate-SWAP targets share paid calls in this same two-label formal model?", + "why_it_matters": "The current obstruction closes exactly two targets; it does not prove a general 3w direct-sum law.", + "first_step": "For w=3, use the sign-trace parity s=1 mod2 and seek a coefficient-rank obstruction or an exact formal word with at most seven calls, versus the direct nine.", + "blocked_by": "The four-call coefficient proof does not cover longer alternating patterns; arbitrary dirty-register counts require a new argument." + }, + { + "question": "Does a genuinely three-dimensional coordinate-CNOT target with a rank-versus-word-length gap permit savings across two roles?", + "why_it_matters": "This is the higher-dimensional branch of PR1333 first open question, outside the two-dimensional target settled here.", + "first_step": "Choose a fixed GL_3(F2) target with certified coordinate-CNOT length above rank(A-I); pin its complete alphabet and compare exact two-role formal words to twice the direct length.", + "blocked_by": "Need a new sign/rank functional or a bounded exact search with full group-algebra equality and complete paid/restoration bill." + } + ], + "chooser": { + "nonce": "30b6519a75b5dea27cbfaca91b7e00af", + "track": "bit-mechanisms", + "scope_key": "7084092dd726e7ba1f2f", + "selected_method": "Derive a target-specific relaxation bound for that same explicit alphabet." + }, + "predecessors": [ + { + "pr": 1333, + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "author": "Gareth Davidson (@bitplane)", + "role": "Research lead and augmentation argument; no imported code." + }, + { + "pr": 720, + "head": "a942c0ae1b463710ca535c1fba1b07b6431b5a86", + "author": "David Govea", + "role": "Nearby abelian rational-register context; no imported code." + } + ], + "result_kind": "scoped-proof" +} diff --git a/research/coordinate-cnot-register-bound/VALIDATION.md b/research/coordinate-cnot-register-bound/VALIDATION.md new file mode 100644 index 0000000000..52f2e31fea --- /dev/null +++ b/research/coordinate-cnot-register-bound/VALIDATION.md @@ -0,0 +1,42 @@ +# Local validation + +At base `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`, using CPython **3.12.3** +and only the standard library: + +```sh +python3 -B scripts/research_baseline.py +python3 scripts/research_package.py --package research/coordinate-cnot-register-bound --check-only +python3 scripts/research_package.py --package research/coordinate-cnot-register-bound +``` + +The baseline returned `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; it checked +selected source bindings and arithmetic, not the selected supplier's cold +replay. The metadata check returned `PASS_PACKAGE_METADATA_AND_PINS`. + +The complete registered replay passed in approximately **8.1 seconds** in +this environment (timing is not an acceptance condition). Its direct command +returned: + +```text +PASS_COORDINATE_CNOT_REGISTER_BOUND minimum=6 dirty_registers=arbitrary census_r=2,3 symbolic_patterns=31 controls=14 no_new_kappa +``` + +The registered focused file ran **six tests**, all passing. Those tests cover +the exact noncommuting symbolic identity and a wrong-functional control; +fourteen boundary/scope controls; five receipt corruptions including an +integer-to-Boolean substitution; duplicate JSON fields; external receipt and +source corruption; and a byte-unchanged read-only minimal export under +`python3 -I -O -B`. The optimized replay performs the complete census and +symbolic checks, not a reduced smoke test. Temporary test exports are removed +after each test. + +The direct replay compares complete formal and faithful-regular state sets +for `r=2,3`, checks their exact distance layers, the empty target intersection, +positive identity/one-swap controls, and the six-call formal witnesses. It also +checks 31 symbolic label patterns, 36 sign products and 4,704 scalar projector +conjugations. All deterministic results are in `EXPECTED.json`. + +Not run: Lean, a selected-supplier cold replay, physical compilation, hosting, +common-label realization, precision/tape or analytic transfer. No independent +human proof review or hosted CI result is claimed. The all-register claim +rests on the written proof in `PROOF.md`, with these checks as corroboration. diff --git a/research/coordinate-cnot-register-bound/VERIFY.json b/research/coordinate-cnot-register-bound/VERIFY.json new file mode 100644 index 0000000000..394b034892 --- /dev/null +++ b/research/coordinate-cnot-register-bound/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": "Exact formal/dense complete state-set comparison, symbolic noncommuting coefficient identities, scalar conjugations, six-call formal witness and 14 semantic failure/scope controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Receipt/source mutation rejection, independent proof-polynomial controls, complete dirty-boundary and clean-only distinction, output-preserving isolated replay." + } + ] +} diff --git a/research/coordinate-cnot-register-bound/independent.py b/research/coordinate-cnot-register-bound/independent.py new file mode 100644 index 0000000000..0235a0b488 --- /dev/null +++ b/research/coordinate-cnot-register-bound/independent.py @@ -0,0 +1,216 @@ +"""Independent dense left-regular representation and symbolic proof checks. + +Group elements here are actual two-by-two binary matrices, not permutation +table entries. Register projectors are enumerated as matrices, not outer pairs. +Every regular-representation column is retained; this representation of the +formal group algebra is faithful. +""" + +import itertools + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def parity(n): + return n.bit_count() % 2 + + +def apply(rows, x): + return sum(parity(row & x) << i for i, row in enumerate(rows)) + + +def multiply(left, right): + """Exact matrix product from packed binary rows.""" + rows = [] + for mask in left: + out = 0 + for i, row in enumerate(right): + if mask >> i & 1: + out ^= row + rows.append(out) + return tuple(rows) + + +def rank(rows): + pivots = {} + for row in rows: + while row: + lead = row.bit_length()-1 + if lead in pivots: + row ^= pivots[lead] + else: + pivots[lead] = row + break + return len(pivots) + + +def unit(n): + return tuple(1 << i for i in range(n)) + + +def address_group(): + candidates = (rows for rows in itertools.product(range(4), repeat=2) + if rank(rows) == 2) + return tuple(sorted(candidates, key=lambda rows: tuple(apply(rows, x)-1 + for x in (1, 2, 3)))) + + +GROUP = address_group() +INDEX = {g: i for i, g in enumerate(GROUP)} +ID = (1, 2) +A = (3, 2) +B = (1, 3) +S = (2, 1) + + +def projectors(r): + return tuple(n for n in itertools.product(range(1 << r), repeat=r) + if rank(n) == 1 and multiply(n, n) == n) + + +def represented_gate(n, g): + r = len(n) + out = list(unit(6*r)) + for i in range(r): + for j in range(r): + if n[i] >> j & 1: + for h, matrix in enumerate(GROUP): + k = INDEX[multiply(g, matrix)] + out[6*i+h] ^= 1 << (6*j+h) + out[6*i+k] ^= 1 << (6*j+h) + return tuple(out) + + +def formal_encoding(rows, r): + """Recover coefficients from action on each register's identity basis.""" + eid = INDEX[ID] + out = 0 + for i in range(r): + for j in range(r): + coefficient = sum(((rows[6*i+k] >> (6*j+eid)) & 1) << k + for k in range(6)) + out |= coefficient << (6*(i*r+j)) + return out + + +def dense_ball(r): + gates = tuple(represented_gate(n, g) for n in projectors(r) for g in (A, B)) + states = {unit(6*r)} + layer = states.copy() + layers = [1] + attempts = 0 + for _ in range(3): + new = set() + for state in layer: + for gate in gates: + attempts += 1 + nxt = multiply(gate, state) + if nxt not in states: + new.add(nxt) + states.update(new) + layer = new + layers.append(len(new)) + encoded = {formal_encoding(state, r) for state in states} + require(len(encoded) == len(states), 'regular coefficient recovery not injective') + return encoded, {'exact_distance_layers_0_to_3': layers, + 'directed_transition_attempts': attempts, + 'regular_dimension': 6*r} + + +def coefficient_polynomials(labels): + """Expand product (I+([g]+1)N_i) over noncommuting indeterminates N_i. + +Each group coefficient is a set of monomials (tuples of scalar-factor +indices), with symmetric difference performing addition in F2. +""" + result = {g: set() for g in GROUP} + result[ID].add(()) + for i, label in enumerate(labels): + out = {g: set(poly) for g, poly in result.items()} + for g, poly in result.items(): + for monomial in poly: + term = monomial + (i,) + for h in (g, multiply(g, label)): + if term in out[h]: + out[h].remove(term) + else: + out[h].add(term) + result = out + return result + + +def proof_checks(): + # Address matrices act as all permutations of the three nonzero vectors. + require(len(GROUP) == 6 and GROUP[0] == ID, 'address group enumeration') + require(multiply(multiply(A, B), A) == S, 'aba is not swap') + require(multiply(multiply(B, A), B) == S, 'bab is not swap') + require(multiply(A, B) != multiply(B, A), 'lost noncommutativity') + cases = [] + for length in (0, 1, 2, 3, 4): + for labels in itertools.product((A, B), repeat=length): + poly = coefficient_polynomials(labels) + text = ''.join('a' if g == A else 'b' for g in labels) + if length <= 2: + require(not poly[S], 'short word unexpectedly supports swap') + method = 'swap coefficient zero' + elif length == 3: + if text in ('aba', 'bab'): + require(poly[S] == {(0, 1, 2)}, 'three-call coefficient identity') + method = 'swap coefficient has rank at most one' + else: + require(not poly[S], 'nonalternating triple supports swap') + method = 'swap coefficient zero' + elif text in ('abab', 'baba'): + other = multiply(labels[1], labels[0]) + require(poly[S] ^ poly[other] == {(1, 2)}, + 'alternating coefficient obstruction identity') + method = 'swap plus reverse-pair coefficient is N1 N2' + else: + # In three runs one block has length two; its expansion is a + # sum of two triple products with a common exterior factor. + if not poly[S]: + method = 'swap coefficient zero' + else: + terms = sorted(poly[S]) + require(all(len(t) == 3 for t in terms), 'run coefficient degree') + require(len(terms) == 2, 'run coefficient term count') + require(terms[0][0] == terms[1][0] or + terms[0][-1] == terms[1][-1], + 'rank-one exterior factor missing') + method = 'swap coefficient has a common rank-one exterior factor' + cases.append({'word': text, 'identity': method}) + # Verify the sign quotient on every group product. Encode 1 as zero parity, + # t=1+epsilon as one parity; epsilon^2=0 in characteristic two. + def sign(g): + values = [apply(g, x) for x in (1, 2, 3)] + return sum(values[i] > values[j] for i in range(3) + for j in range(i+1, 3)) % 2 + for g, h in itertools.product(GROUP, repeat=2): + require(sign(multiply(g, h)) == sign(g) ^ sign(h), 'sign is not a homomorphism') + require(sign(A) == sign(B) == sign(S) == 1, 'paid/target sign mismatch') + return {'symbolic_label_patterns_through_four': len(cases), + 'sign_homomorphism_products': 36, + 'four_call_patterns': [c for c in cases if len(c['word']) == 4]} + + +def scalar_checks(): + # All GL(3,2) conjugations preserve exactly the allowed projector set. + r = 3 + proj = set(projectors(r)) + invertible = [rows for rows in itertools.product(range(8), repeat=3) + if rank(rows) == 3] + inverses = {m: next(n for n in invertible if multiply(m, n) == unit(r)) + for m in invertible} + checks = 0 + for matrix in invertible: + for n in proj: + require(multiply(multiply(matrix, n), inverses[matrix]) in proj, + 'scalar conjugation leaves generator domain') + require(sum(n[i] >> i & 1 for i in range(r)) % 2 == 1, + 'rank-one idempotent trace is not one') + checks += 1 + return {'gl3_matrices': len(invertible), 'rank_one_idempotents': len(proj), + 'conjugations': checks} diff --git a/research/coordinate-cnot-register-bound/test_verify.py b/research/coordinate-cnot-register-bound/test_verify.py new file mode 100644 index 0000000000..4519fbe085 --- /dev/null +++ b/research/coordinate-cnot-register-bound/test_verify.py @@ -0,0 +1,116 @@ +#!/usr/bin/env python3 +"""Focused mathematical-boundary and package rejection tests (stdlib only).""" + +import copy +import hashlib +import importlib.util +import json +import shutil +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location('cnot_verify', PACKAGE/'verify.py') +VERIFY = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(VERIFY) + + +class CertificateTests(unittest.TestCase): + def test_symbolic_rank_obstruction(self): + d = VERIFY.INDEPENDENT + checks = d.proof_checks() + self.assertEqual(checks['symbolic_label_patterns_through_four'], 31) + # The reverse-pair choice is essential: using ab for abab does not + # give the single rank-one monomial used in the proof. + poly = d.coefficient_polynomials((d.A, d.B, d.A, d.B)) + good = poly[d.S] ^ poly[d.multiply(d.B, d.A)] + wrong = poly[d.S] ^ poly[d.multiply(d.A, d.B)] + self.assertEqual(good, {(1, 2)}) + self.assertNotEqual(wrong, good) + + def test_dirty_boundary_and_scope_controls(self): + controls = VERIFY.controls() + self.assertEqual(len(controls), 14) + self.assertEqual(len(set(controls)), 14) + self.assertIn('clean_only_dirty_leakage', controls) + self.assertIn('rank_two_projector_underpricing', controls) + + def test_complete_receipt_and_json_types(self): + expected = VERIFY.read_json(PACKAGE/'EXPECTED.json') + for mutate in ( + lambda x: x['censuses'][1].update(ball3_size=47202), + lambda x: x['censuses'][0]['exact_distance_layers_0_to_3'].__setitem__(0, True), + lambda x: x['censuses'][1].update(intersections_through_five=1), + lambda x: x['controls'].pop(), + lambda x: x.update(unchecked_extra_field=True), + ): + modified = copy.deepcopy(expected) + mutate(modified) + with self.assertRaisesRegex(ValueError, 'fresh receipt differs'): + VERIFY.compare_receipt(modified, expected) + + def test_duplicate_json_rejected(self): + with tempfile.TemporaryDirectory(prefix='cnot-json-') as work: + path = Path(work)/'duplicate.json' + path.write_text('{"minimum":6,"minimum":5}') + with self.assertRaisesRegex(ValueError, 'duplicate JSON key'): + VERIFY.read_json(path) + + def copied_package(self, root): + package = root/'research'/'coordinate-cnot-register-bound' + package.mkdir(parents=True) + for name in ('verify.py', 'independent.py', 'EXPECTED.json', 'SOURCES.json'): + shutil.copyfile(PACKAGE/name, package/name) + source = root/'research'/'bit-three-register-lower-bound'/'README.md' + source.parent.mkdir(parents=True) + shutil.copyfile(PACKAGE.parents[1]/source.relative_to(root), source) + return package, source + + def run_export(self, package, *flags): + return subprocess.run([sys.executable, '-I', '-B', *flags, str(package/'verify.py')], + cwd=package.parents[1], capture_output=True, text=True, + timeout=120, check=False) + + def test_read_only_relocated_optimized_replay(self): + with tempfile.TemporaryDirectory(prefix='cnot-relocate-') as work: + root = Path(work) + package, source = self.copied_package(root) + paths = list(package.iterdir())+[source] + before = {p.relative_to(root).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in paths} + try: + for p in paths: + p.chmod(0o444) + package.chmod(0o555) + result = self.run_export(package, '-O') + self.assertEqual(result.returncode, 0, result.stderr[-3000:]) + self.assertIn('PASS_COORDINATE_CNOT_REGISTER_BOUND', result.stdout) + after = {p.relative_to(root).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob('*') if p.is_file()} + self.assertEqual(before, after) + finally: + package.chmod(0o755) + for p in paths: + p.chmod(0o644) + + def test_external_receipt_and_source_corruption_rejected(self): + with tempfile.TemporaryDirectory(prefix='cnot-corruption-') as work: + package, source = self.copied_package(Path(work)) + expected = VERIFY.read_json(package/'EXPECTED.json') + expected['censuses'][1]['minimum_paid_calls'] = 5 + (package/'EXPECTED.json').write_text(json.dumps(expected)) + result = self.run_export(package) + self.assertNotEqual(result.returncode, 0) + self.assertIn('fresh receipt differs', result.stderr) + shutil.copyfile(PACKAGE/'EXPECTED.json', package/'EXPECTED.json') + source.write_text(source.read_text()+'\ncorrupted context source\n') + result = self.run_export(package) + self.assertNotEqual(result.returncode, 0) + self.assertIn('source pin mismatch', result.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/coordinate-cnot-register-bound/verify.py b/research/coordinate-cnot-register-bound/verify.py new file mode 100644 index 0000000000..02077ae7e1 --- /dev/null +++ b/research/coordinate-cnot-register-bound/verify.py @@ -0,0 +1,293 @@ +#!/usr/bin/env python3 +"""Exact formal F2[GL_2(F2)] coordinate-CNOT register census (stdlib only).""" + +import argparse +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location('cnot_independent', PACKAGE/'independent.py') +INDEPENDENT = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(INDEPENDENT) +GROUP = tuple(itertools.permutations(range(3))) +INDEX = {g: i for i, g in enumerate(GROUP)} +MUL = tuple(tuple(INDEX[tuple(p[q[i]] for i in range(3))] for q in GROUP) + for p in GROUP) +E = INDEX[(0, 1, 2)] +A = INDEX[(0, 2, 1)] +B = INDEX[(2, 1, 0)] +SWAP = INDEX[(1, 0, 2)] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def read_json(path): + def unique(pairs): + result = {} + for key, value in pairs: + require(key not in result, 'duplicate JSON key: '+key) + result[key] = value + return result + return json.loads(path.read_text(), object_pairs_hook=unique) + + +def compare_receipt(actual, expected): + # JSON types matter: Python equality alone equates True with 1. + encode = lambda x: json.dumps(x, sort_keys=True, separators=(',', ':'), allow_nan=False) + require(encode(actual) == encode(expected), 'fresh receipt differs from EXPECTED.json') + + +def translate(mask, g): + """Multiply a formal coefficient by [g] on the right.""" + out = 0 + for h in range(6): + if mask >> h & 1: + out ^= 1 << MUL[h][g] + return out + + +TRANSLATE = tuple(tuple(translate(mask, g) for mask in range(64)) + for g in range(6)) + + +def identity(r): + return sum(1 << (6 * (i*r+i) + E) for i in range(r)) + + +def entry(state, r, i, j): + return state >> (6*(i*r+j)) & 63 + + +def generators(r): + return tuple((u, v, g) + for u in range(1, 1 << r) + for v in range(1, 1 << r) + if (u & v).bit_count() % 2 + for g in (A, B)) + + +def append(state, r, gate): + """Right multiply by I+([g]+1)uv^T, retaining all formal coefficients.""" + u, v, g = gate + out = state + table = TRANSLATE[g] + for i in range(r): + val = 0 + for j in range(r): + if u >> j & 1: + val ^= entry(state, r, i, j) + val ^= table[val] + for j in range(r): + if v >> j & 1: + out ^= val << (6 * (i*r+j)) + return out + + +def word_state(r, word, gates): + out = identity(r) + for index in word: + out = append(out, r, gates[index]) + return out + + +def target(r, active=2): + return sum(1 << (6*(i*r+i) + (SWAP if i < active else E)) + for i in range(r)) + + +def right_target(state, r, active=2): + out = 0 + for i in range(r): + for j in range(r): + value = entry(state, r, i, j) + out |= (TRANSLATE[SWAP][value] if j < active else value) << (6*(i*r+j)) + return out + + +def digest(states, r): + width = (6*r*r + 7)//8 + h = hashlib.sha256() + for state in sorted(states): + h.update(state.to_bytes(width, 'little')) + return h.hexdigest() + + +def census(r): + gates = generators(r) + ball = {identity(r): ()} + layers = [[identity(r)]] + layer_counts = [1] + for depth in range(1, 4): + new = [] + for state in layers[-1]: + prefix = ball[state] + for k, gate in enumerate(gates): + nxt = append(state, r, gate) + if nxt not in ball: + ball[nxt] = prefix + (k,) + new.append(nxt) + layers.append(new) + layer_counts.append(len(new)) + # Every gate is an involution, so reversing a word gives its exact inverse. + ball2 = {state: word for state, word in ball.items() if len(word) <= 2} + shifted = {right_target(word_state(r, word[::-1], gates), r): word + for word in ball2.values()} + hits = sorted(set(shifted).intersection(ball)) + independent, independent_receipt = INDEPENDENT.dense_ball(r) + require(independent == set(ball), 'independent dense and formal balls differ') + require(independent_receipt['exact_distance_layers_0_to_3'] == layer_counts, + 'independent distance layers differ') + positive_minima = [] + for active in (0, 1): + positive_shifted = { + right_target(word_state(r, word[::-1], gates), r, active): word + for word in ball2.values()} + positive_hits = set(positive_shifted).intersection(ball) + minimum = min(len(positive_shifted[h])+len(ball[h]) for h in positive_hits) + require(minimum == 3*active, 'positive meet-in-the-middle control fails') + positive_minima.append(minimum) + direct = tuple(gates.index((1 << role, 1 << role, g)) + for role in range(2) for g in (A, B, A)) + require(word_state(r, direct, gates) == target(r), 'direct formal word fails') + return { + 'registers': r, + 'active_targets': 2, + 'restored_dirty_registers': r-2, + 'scalar_rank_one_idempotents': len(gates)//2, + 'paid_generators': len(gates), + 'exact_distance_layers_0_to_3': layer_counts, + 'ball2_size': len(ball2), + 'ball3_size': len(ball), + 'ball2_sha256': digest(ball2, r), + 'ball3_sha256': digest(ball, r), + 'inverse_ball2_times_target_sha256': digest(shifted, r), + 'intersections_through_five': len(hits), + 'minimum_paid_calls': 6 if not hits else min( + len(shifted[h])+len(ball[h]) for h in hits), + 'independent_dense': independent_receipt, + 'positive_identity_and_one_swap_minima': positive_minima, + 'direct_six_call_word': [list(gates[k]) for k in direct], + } + + +def controls(): + r = 3 + d = INDEPENDENT + names = [] + direct = tuple((1 << role, 1 << role, g) + for role in range(2) for g in (A, B, A)) + + def replay(word): + value = identity(r) + for gate in word: + value = append(value, r, gate) + return value + + # Every individual omission fails, with the complete dirty boundary tested. + for i in range(6): + require(replay(direct[:i]+direct[i+1:]) != target(r), 'omission accepted') + names.append(f'omitted_call_{i}') + wrong = list(direct) + wrong[1] = (1, 1, A) + require(replay(wrong) != target(r), 'wrong address label accepted') + names.append('wrong_address_label') + + # Correct active outputs alone do not imply restoration of a dirty helper. + unrestored = replay(direct+((4, 4, A),)) + require(all(entry(unrestored, r, i, j) == entry(target(r), r, i, j) + for i in range(2) for j in range(r)), 'dirty control active map') + require(unrestored != target(r), 'dirty helper change accepted') + names.append('unrestored_dirty_register') + + # A scalar trailing shear leaks dirty input into the first active output, + # but is invisible on the clean-only input subspace. + leakage = target(r) ^ (1 << (6*2+SWAP)) + require(all(entry(leakage, r, i, j) == entry(target(r), r, i, j) + for i in range(r) for j in range(2)), 'clean-only control') + require(leakage != target(r), 'dirty-to-active leakage accepted') + augmentation = tuple(sum(entry(leakage, r, i, j).bit_count()%2 << j + for j in range(r)) for i in range(r)) + require(augmentation != d.unit(r), 'nonidentity scalar residue accepted') + names.extend(['clean_only_dirty_leakage', 'nonidentity_scalar_augmentation']) + + # A rank-two projector makes the two swaps in three calls. It must be + # rejected as a unit call; its honest bill is two units per occurrence. + rank_two = (1, 2, 0) + wide = d.unit(18) + for g in (d.A, d.B, d.A): + wide = d.multiply(wide, d.represented_gate(rank_two, g)) + require(d.formal_encoding(wide, r) == target(r), 'rank-two scope fixture') + require(d.rank(rank_two) == 2 and rank_two not in d.projectors(r), + 'rank-two call underpricing accepted') + names.append('rank_two_projector_underpricing') + + # Adding S as an allowed address label makes the two-call word legal. + expanded = replay(((1, 1, SWAP), (2, 2, SWAP))) + require(expanded == target(r) and SWAP not in (A, B), 'expanded-label scope fixture') + names.append('uncharged_address_alphabet_expansion') + + # The natural 2D representation loses formal information. Its kernel + # contains the sum of all six group elements, even after augmentation. + kernel_rows = tuple(0 for _ in range(2)) + for matrix in d.GROUP: + kernel_rows = tuple(x ^ y for x, y in zip(kernel_rows, matrix)) + require(kernel_rows == (0, 0) and 6 % 2 == 0, 'natural-image kernel fixture') + alias = target(r) ^ (63 << 6) # add that kernel element at entry (0,1) + require(alias != target(r), 'natural-image alias accepted as formal equality') + names.append('nonfaithful_natural_representation') + + require(MUL[A][B] != MUL[B][A], 'noncommuting labels accidentally commute') + names.append('address_multiplication_order') + return names + + +def check_sources(): + sources = read_json(PACKAGE/'SOURCES.json') + checked = [] + for item in sources['files']: + if item['usage'] != 'input': + continue + path = Path(item['path']) + require(not path.is_absolute() and '..' not in path.parts, 'invalid source path') + actual = hashlib.sha256((PACKAGE.parents[1]/path).read_bytes()).hexdigest() + require(actual == item['sha256'], 'source pin mismatch: '+str(path)) + checked.append(str(path)) + require(checked == ['research/bit-three-register-lower-bound/README.md'], + 'source input inventory changed') + return checked + + +def build_result(): + return {'format': 'coordinate-cnot-register-bound-v1', + 'group_permutations': [list(p) for p in GROUP], + 'labels': {'identity': E, 'a': A, 'b': B, 'swap': SWAP}, + 'censuses': [census(r) for r in (2, 3)], + 'symbolic_proof_checks': INDEPENDENT.proof_checks(), + 'scalar_normalization_checks': INDEPENDENT.scalar_checks(), + 'controls': controls(), + 'checked_context_inputs': check_sources()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true', help='print freshly computed receipt') + args = parser.parse_args() + result = build_result() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + expected = read_json(PACKAGE/'EXPECTED.json') + compare_receipt(result, expected) + print('PASS_COORDINATE_CNOT_REGISTER_BOUND minimum=6 ' + 'dirty_registers=arbitrary census_r=2,3 symbolic_patterns=31 ' + f'controls={len(result["controls"])} no_new_kappa') + + +if __name__ == '__main__': + main()