From 246cd6b3a795a346bc6a741661ddcdb2d6359103 Mon Sep 17 00:00:00 2001 From: ross Date: Wed, 14 Oct 2026 18:51:48 +1100 Subject: [PATCH] Prove coordinate-CNOT label saturation and sharpen four-swap bound --- .../coordinate-cnot-label-saturation/PROOF.md | 166 ++ .../README.md | 171 ++ .../RESULT.json | 1980 +++++++++++++++++ .../SOURCES.json | 24 + .../TASK.json | 166 ++ .../VERIFY.json | 42 + .../independent.py | 217 ++ .../test_package.py | 124 ++ .../verify.py | 420 ++++ 9 files changed, 3310 insertions(+) create mode 100644 research/coordinate-cnot-label-saturation/PROOF.md create mode 100644 research/coordinate-cnot-label-saturation/README.md create mode 100644 research/coordinate-cnot-label-saturation/RESULT.json create mode 100644 research/coordinate-cnot-label-saturation/SOURCES.json create mode 100644 research/coordinate-cnot-label-saturation/TASK.json create mode 100644 research/coordinate-cnot-label-saturation/VERIFY.json create mode 100644 research/coordinate-cnot-label-saturation/independent.py create mode 100644 research/coordinate-cnot-label-saturation/test_package.py create mode 100644 research/coordinate-cnot-label-saturation/verify.py diff --git a/research/coordinate-cnot-label-saturation/PROOF.md b/research/coordinate-cnot-label-saturation/PROOF.md new file mode 100644 index 0000000000..bbe3fbd941 --- /dev/null +++ b/research/coordinate-cnot-label-saturation/PROOF.md @@ -0,0 +1,166 @@ +# Saturating one coordinate-CNOT label forces the direct bill + +This is a written theorem for the formal register model of commdata2338's +PR1414/1491 and Cinna Davis's PR1541. The finite checks corroborate the +argument; they are not its all-register justification. No physical supplier +or multiplication exponent is claimed. + +## Model and statement + +Let `G=GL_2(F2)`, with `a=[[1,1],[0,1]]`, `b=[[1,0],[1,1]]` and +`s=aba=bab=[[0,1],[1,0]]`. For finite `r>=t>=1`, work in the **formal** +algebra `M_r(F2[G])`. One paid unit is + +`D_N(g)=I+([g]+1)N`, where `g` is only `a` or `b`, `N=uv^T`, and `v^T u=1`. + +Free scalar `GL_r(F2)` basis changes are allowed. Every address call, +including an undo, costs one. No other address maps, copies, erasures, +overwrites or clean allocation are available. The complete target is + +`T=I+([s]+1)P`, with `P=diag(I_t,0)`. + +All inputs are arbitrary. Every extra register is restored and may not leak +into active outputs. Equality is in the group algebra, not merely its +natural two-dimensional address representation. The direct bill is `3t`: +use `bab` or `aba` on each active coordinate projector. + +**Label-saturation theorem.** Write `n_a,n_b` for the paid label counts. +Every such word has `n_a,n_b>=t`. If `n_a=t`, then `n_b>=2t`; symmetrically, +if `n_b=t`, then `n_a>=2t`. At equality `(t,2t)` or `(2t,t)`, every normalized +paid projector satisfies `PN=N=NP`: the paid factors do not couple the +restored dirty complement. This last claim concerns normalized paid factors, +not the original placement of free scalar operations. + +## 1. Credited reductions + +Move all scalar basis changes to the right, conjugating each projector. +Augmentation `[g]->1` sends each paid factor and the target to `I`, so the +remaining scalar factor is `I`. Rank-one idempotence is preserved. This is +the normalization used by Gareth Davidson's PR1333 and the later CNOT work. + +The sign quotient `G=S3 -> C2`, over +`F2[C2]=F2[epsilon]/(epsilon^2)`, sends each `a,b,s` to `1+epsilon`. +The normalized formal identity therefore gives + +`sum_all N_i=P`, and hence `n_a+n_b = t (mod 2)`. + +The matrix-sum identity is stronger than its trace consequence and is needed +below. This is the sign argument of PR1414, reused with credit. + +Order coordinates by the two address components in the natural +representation. Chronological **left** multiplication gives + +`a: [[I,N],[0,I]]`, `b: [[I,0],[N,I]]`, + +and the target is `[[I+P,P],[P,I+P]]`. Only an `a` call changes the top block +row, with image in its vector `u`; only a `b` call changes the bottom block +row. The two final off-diagonal blocks `P` imply + +`im P <= span(u_a)` and `im P <= span(u_b)`. + +Thus each label occurs at least `t` times. This is the image-span step of +PR1541. A formal identity implies the represented identity; the converse is +not assumed. + +## 2. Exactly t a calls make the top block row rigid + +Suppose `n_a=t`. The `t` vectors `u_a` are a basis of `im P`. Conjugate by a +scalar basis change on `im P`, extended by the identity on `ker P`, so that +the image vectors, in occurrence order, are `e_1,...,e_t`. This conjugation +commutes with `P` and does not change the target or either count. + +Write the running natural matrix as `[[A,B],[C,D]]`. Each active top row +is changed by exactly one call; all other top rows are unchanged. Top row +`i` is initially `[e_i^T,0]` and finally `[0,e_i^T]`. Before its unique call +it equals its initial row, and after that call it equals its final row. +Both have the same row sum. Consequently + +`A+B=I` at **every** chronological cut. + +A `b` call with projector `N_j` changes `C+D` by +`N_j(A+B)=N_j`. Initially and finally `C+D=I`, so + +`sum_b N_j=0`. + +Combine this with the full sign identity to obtain `sum_a N_i=P`. But +`N_i=e_i v_i^T`, so comparison of its distinct rows gives `v_i=e_i`. +Every `a` projector is therefore precisely `E_ii` in this basis. + +At the unique `a` call on row `i`, the needed top-row change is +`[e_i^T,e_i^T]`. Since its covector is `e_i`, bottom row `i` at that instant +is exactly this row. Its two block halves sum to zero. On the other hand, + +`C+D=I+sum_(b before a_i) N_j`. + +Taking row `i` gives + +`e_i^T = sum_(b before a_i) e_i^T N_j`. + +Each summand is a scalar multiple of `v_j^T`. Thus **every active coordinate +covector belongs to the span of the b covectors**. This chronological step, +together with the zero sum, is the additional ingredient. + +## 3. A zero rank-one sum must pay for both spans + +Let `m=n_b`, let `U` be the `r by m` matrix with columns `u_j`, and let `V` +be the `m by r` matrix with rows `v_j^T`, over the `b` calls. We have + +`UV=sum_b N_j=0`, `rank U>=t`, and `rank V>=t`. + +Since `im V` is contained in `ker U`, rank-nullity gives + +`m >= rank U + rank V >= 2t`. + +This proves saturation. Exchanging the two address coordinates exchanges +`a` and `b` while fixing `s`, giving the symmetric statement. + +If `m=2t`, both ranks are exactly `t`. Their column and row spans contain, +respectively, the active coordinate space and its covector space, so those +spans equal the active spaces. Each `b` image and covector has no dirty +component. The `a` projectors are already `E_ii`. Undoing the scalar change +that commutes with `P` gives `PN=N=NP` for every normalized paid factor. + +The proof uses no upper bound on `r` or `t`, no finite search, and no +assumption that different projectors commute. + +## 4. Consequences and the unresolved case + +* **Three swaps cost nine with arbitrary finite dirty workspace.** A word + below nine has odd length and at least three of each label, so only seven + remains, with counts `(3,4)` or `(4,3)`. Saturation rules both out. Three + direct `bab` words attain nine in the full formal algebra. This is an + analytic alternative proof of PR1541's theorem; that predecessor retains + priority for the arbitrary-workspace result and its checked SAT proof. +* **Four swaps need at least ten.** Below twelve, parity and the label floor + leave totals eight or ten. Saturation excludes `(4,4)`, `(4,6)` and + `(6,4)`. Only `(5,5)` at total ten remains. The direct twelve-call word + attains the upper bound. This covers arbitrary finite dirty workspace and + strengthens the `r=4`, `{8,10,12}` boundary reported in PR1705. It does + **not** prove the four-swap minimum is twelve or supply a ten-call word. + +For completeness, PR1541's compression step reduces that remaining ten-call +case to at most six roles: put `L=span(u_a)+span(u_b)`. Both spans contain +`im P`, so `dim L<=n_a+n_b-t=6`. Every paid projector preserves `L`, and its +restriction remains rank-one idempotent because its image vector lies in +`L` and its covector evaluates to one on that vector. Restrict the full +formal identity to `L` and choose a basis of `im P` plus `L intersect ker P`. +This gives four active swaps and at most two dirty roles, with the same ten +paid calls. Compression is credited to PR1541, not claimed as new here. + +More generally, every potential saving below `3t` must have both counts at +least `t+1`, as well as the retained sign parity. The theorem only screens +this fixed two-label formal model; it does not exclude other alphabets. + +## Credit and limits + +Credit commdata2338 (PR1414/1491), Gareth Davidson (PR1333), Cinna Davis +(PR1541), and Aaron Wang (PR1705), with exact heads in TASK.json. Eumemic +(PR288), Ali Romman (PR468), and David Govea (PR720) supply surrounding +rational/register-model lineage. This proof does not import the rational +three-register obstruction into the nonabelian model. + +Prepared for Ross Richardson with substantial OpenAI Codex assistance. +Apache-2.0. The written proof has not been checked by a proof assistant or +independently reviewed by a human. Physical compiler/common-label realization, +hosting, precision/tape, full selected cold replay and analytic transfer +remain outside this contribution. No new kappa. diff --git a/research/coordinate-cnot-label-saturation/README.md b/research/coordinate-cnot-label-saturation/README.md new file mode 100644 index 0000000000..5ae3de1d1b --- /dev/null +++ b/research/coordinate-cnot-label-saturation/README.md @@ -0,0 +1,171 @@ +# Coordinate-CNOT label saturation with arbitrary dirty workspace + +**Scoped written theorem; no new kappa.** For `t` coordinate-SWAP targets in +the formal `F2[GL_2(F2)]` register model, exactly `t` calls of one coordinate-CNOT +label force at least `2t` calls of the other. This holds for any finite number +of restored dirty registers and free scalar mixing. At the saturated `3t` +boundary, the normalized paid factors do not couple the dirty complement. + +The [proof](PROOF.md) gives an analytic alternative to the finite step in +Cinna Davis's [PR1541](https://github.com/CrocSwap/integer-mult-bounds/pull/1541) +three-swap theorem, and strengthens Aaron Wang's +[PR1705](https://github.com/CrocSwap/integer-mult-bounds/pull/1705) four-swap +boundary: + +| Target | Established consequence | +| --- | --- | +| Three swaps, arbitrary finite dirty workspace | Exactly nine calls; predecessor result now has a short analytic proof | +| Four swaps, arbitrary finite dirty workspace | Minimum is **ten or twelve**; a ten-call word must use **five of each label** | +| Remaining ten-call case | PR1541's credited compression reduces it to at most six roles: four active and two dirty | + +There is **no ten-call construction or exclusion** here. PR1705 excluded +two, four and six calls at exactly four registers and left `{8,10,12}`. +The new saturation lemma excludes eight and the unbalanced ten-call counts, +without a larger state census. The earlier three-swap result retains its +predecessors' priority. + +## Exact model and complete optimistic bill + +The only paid address labels are +`a=[[1,1],[0,1]]` and `b=[[1,0],[1,1]]`; `s=aba=bab` is the swap. +Each unit call is `I+([g]+1)uv^T`, with binary `v^T u=1`. Free scalar +`GL_r(F2)` mixing is normalized by augmentation. The endpoint is +`diag([s],...,[s],1,...,1)` as a **full formal group-algebra matrix**. +Every dirty input has its prescribed output; every undo call is charged. +No other address maps, copies, erasures or clean allocation are allowed. + +The direct upper bill is `3t`, with no extra roles or scalar preparation. +Scalar work and workspace are favorably free in the lower-bound model. +An actual supplier would still need its physical/compiler, hosting, +precision/tape and analytic costs. This replaces the rational abelian +starting model with a specified nonabelian binary alphabet; it does not +reduce rational frame entries modulo two. + +## Why the new inequality holds + +If there are only `t` a-calls, their image vectors form a basis of the active +space. In that basis, each active top block row changes exactly once, from +its input row to its output row. Its two block halves therefore always sum +to the same row. The b-call projectors must sum to zero. + +The full sign-quotient matrix equation then forces every a-projector to be +a coordinate projector. At each a-call, its bottom row forces an active +coordinate covector into the span of the b covectors. The b image vectors +already span the active space. Writing their zero sum as `UV=0` gives +`n_b >= rank(U)+rank(V) >= 2t`. + +The chronological covector step matters: four legal rank-one projectors +can sum to zero with image rank three but covector rank one. This explicit +near miss rejects a tempting one-span-only argument. The full sign equation +also cannot be replaced by its parity consequence. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -B scripts/research_package.py --package research/coordinate-cnot-label-saturation +``` + +Or run the three checks directly: + +```sh +python3.12 -I -B research/coordinate-cnot-label-saturation/verify.py +python3.12 -I -B research/coordinate-cnot-label-saturation/independent.py +python3.12 -I -O -B research/coordinate-cnot-label-saturation/test_package.py +``` + +Expected markers are `PASS_COORDINATE_CNOT_LABEL_SATURATION`, +`PASS_INDEPENDENT_LABEL_SATURATION`, and five passing package test groups. +`verify.py --write` explicitly regenerates the deterministic RESULT.json; +normal replay is read-only. There is no SAT solver, heuristic pruning, +floating-point acceptance or dependency installation. + +The two implementations share the stated mathematical model and receipt +format but no executable code. The primary engine multiplies formal +coefficients using actual binary address matrices. The second constructs +permutations and their faithful regular operators, enumerating scalar +projectors separately. Both were written by one Codex agent in this session. + +## Finite evidence and failure controls + +The written argument establishes the universal statement. The following +bounded computations corroborate it and test the implementation: + +* Complete exact-length, label-count-indexed formal censuses through five + calls on one register and six on two. The two-register layer sizes are + `1,12,82,496,2640,13552,58408`. These are **not** shortest-distance layer + sizes: the same matrix at different label counts is deliberately retained. + Both engines independently obtain the same canonical complete-set hashes. +* A complete `3+3` join enumerates all **1,296 literal six-call two-swap + words**, with a-count histogram `{2:324,3:648,4:324}`. The primary checker + verifies the normalization, every relevant chronological cut, both ranks + and equality-case workspace restriction on all **648 saturated words**. + The independent engine agrees on the complete sorted-word digest. +* Twenty-five positive words cover `t=1..5`, both saturated labels, changed + active bases, and zero or one dirty extra. Five deliberately touch and + restore that extra using two additional paid calls. Full faithful forward + and reverse replay covers **1,080 columns** and rejects **235 individual + paid-call omissions**. +* Fifteen primary controls cover six omissions, dirty leakage, a missing + target, changed/expanded labels, an illegal scalar projector, Boolean + input, the one-span and trace-only near misses, and a natural-representation + alias. The last is a nonzero formal off-diagonal perturbation with zero + natural image; it is not asserted to be a cheaper word. +* Five package test groups exercise optimized read-only relocation, changed + and missing source bytes, false theorem/cut/count receipts, both-engine + word/census/attainer corruption, duplicate/nonfinite JSON and missing input + inventory. Integer receipt fields reject Boolean and floating aliases. + +The independent operator engine corroborates finite evidence. It does not +formalize the universal proof or independently derive its ten-call bound. + +## Provenance, overlap and scope + +Base: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. Selected record SHA256: +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +Task `bit-new-register-model`, refined to a target-specific relaxation; +OS chooser nonce `8e7454be62cc38c3ccc7edd6bd6d2bc2`. The alternative +helper-contract card was not chosen because its immediate interface question +is already covered by PR1194/1311 and subsequent feedback work. + +[TASK.json](TASK.json) records exact predecessor heads, the scope and overlap +coverage. [SOURCES.json](SOURCES.json) pins the original task/selection and the +unchanged PR1414 proof text. The later PR1541/1705 heads are contextual sources; +no pending implementation or certificate is imported. Their credited +compression argument is restated in PROOF.md. + +[Discussion #1715](https://github.com/CrocSwap/integer-mult-bounds/discussions/1715) +holds the claim and handoff. The overlap search covers open PR bodies, local +top-level package notes and the ledger, plus Discussion bodies/comments. +It excludes arbitrary diffs/nested code and is not a novelty certificate. + +Selected-source binding and package verification are separate from complete +selected cold replay. No full supplier replay, new recursive profile, +physical adoption, Lean proof, independent human review, measured runtime +gain or stronger multiplication exponent is claimed. Existing frozen sources +and the selected frontier are unchanged. + +## Open next questions + +**Does the balanced ten-call four-swap word exist?** It is the sole remaining +potential saving below twelve in this alphabet. First encode all `5+5` label +patterns with at most six roles, using the credited compression, a full +formal endpoint and a proof-producing solver. The blocker is the remaining +noncommuting projector interaction; neither this theorem nor the small +censuses decide it. A valid word would still need all physical supplier costs. +This question is also structured in TASK.json. + +## Credit and license + +Credit **commdata2338 / PR1414 and PR1491** for the coordinate-CNOT model, +sign quotient and two/three-swap results; **Gareth Davidson / PR1333** for +scalar normalization and the restricted-alphabet question; **Cinna Davis / +PR1541** for the arbitrary-workspace three-swap theorem and role compression; +and **Aaron Wang / PR1705** for the four-register boundary and explicit +unfinished search. Eumemic / PR288, Ali Romman / PR468 and David Govea / PR720 +retain the surrounding rational/register-model credit. + +Prepared for **Ross Richardson**, with substantial **OpenAI Codex assistance** +in reasoning, implementation, verification and writing. One agent; no +independent human or proof-assistant review. New work is Apache-2.0. diff --git a/research/coordinate-cnot-label-saturation/RESULT.json b/research/coordinate-cnot-label-saturation/RESULT.json new file mode 100644 index 0000000000..bf45e4f46c --- /dev/null +++ b/research/coordinate-cnot-label-saturation/RESULT.json @@ -0,0 +1,1980 @@ +{ + "schema_version": 1, + "scope": "written saturation theorem; finite corroboration only; no_new_kappa", + "sources": [ + "bcee89f92dcce8253bd7eae6e924ddff598c900da81979c6171a412f03d765e1" + ], + "screen": { + "1": { + "0": [], + "1": [], + "2": [], + "3": [ + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ] + }, + "2": { + "0": [], + "1": [], + "2": [], + "3": [], + "4": [], + "5": [], + "6": [ + [ + 2, + 4 + ], + [ + 3, + 3 + ], + [ + 4, + 2 + ] + ] + }, + "3": { + "0": [], + "1": [], + "2": [], + "3": [], + "4": [], + "5": [], + "6": [], + "7": [], + "8": [], + "9": [ + [ + 3, + 6 + ], + [ + 4, + 5 + ], + [ + 5, + 4 + ], + [ + 6, + 3 + ] + ] + }, + "4": { + "0": [], + "1": [], + "2": [], + "3": [], + "4": [], + "5": [], + "6": [], + "7": [], + "8": [], + "9": [], + "10": [ + [ + 5, + 5 + ] + ], + "11": [], + "12": [ + [ + 4, + 8 + ], + [ + 5, + 7 + ], + [ + 6, + 6 + ], + [ + 7, + 5 + ], + [ + 8, + 4 + ] + ] + }, + "5": { + "0": [], + "1": [], + "2": [], + "3": [], + "4": [], + "5": [], + "6": [], + "7": [], + "8": [], + "9": [], + "10": [], + "11": [], + "12": [], + "13": [ + [ + 6, + 7 + ], + [ + 7, + 6 + ] + ], + "14": [], + "15": [ + [ + 5, + 10 + ], + [ + 6, + 9 + ], + [ + 7, + 8 + ], + [ + 8, + 7 + ], + [ + 9, + 6 + ], + [ + 10, + 5 + ] + ] + }, + "6": { + "0": [], + "1": [], + "2": [], + "3": [], + "4": [], + "5": [], + "6": [], + "7": [], + "8": [], + "9": [], + "10": [], + "11": [], + "12": [], + "13": [], + "14": [ + [ + 7, + 7 + ] + ], + "15": [], + "16": [ + [ + 7, + 9 + ], + [ + 8, + 8 + ], + [ + 9, + 7 + ] + ], + "17": [], + "18": [ + [ + 6, + 12 + ], + [ + 7, + 11 + ], + [ + 8, + 10 + ], + [ + 9, + 9 + ], + [ + 10, + 8 + ], + [ + 11, + 7 + ], + [ + 12, + 6 + ] + ] + } + }, + "witnesses": [ + { + "targets": 1, + "registers": 1, + "saturated_label": "a", + "word": [ + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ], + "trace": { + "opposite_count": 2, + "image_rank": 1, + "covector_rank": 1, + "cuts_sha256": "d5d6e4fe39493d265009ec3c6610ac4cb1a3a5f2ebae523140203eaa7ccecf96" + } + }, + { + "targets": 1, + "registers": 1, + "saturated_label": "b", + "word": [ + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ] + ], + "trace": { + "opposite_count": 2, + "image_rank": 1, + "covector_rank": 1, + "cuts_sha256": "d5d6e4fe39493d265009ec3c6610ac4cb1a3a5f2ebae523140203eaa7ccecf96" + } + }, + { + "targets": 1, + "registers": 2, + "saturated_label": "a", + "word": [ + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ], + "trace": { + "opposite_count": 2, + "image_rank": 1, + "covector_rank": 1, + "cuts_sha256": "5b1b199daa74a4626e723be701623367482d2d4d49506518f39185cb0d2a658c" + } + }, + { + "targets": 1, + "registers": 2, + "saturated_label": "b", + "word": [ + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ] + ], + "trace": { + "opposite_count": 2, + "image_rank": 1, + "covector_rank": 1, + "cuts_sha256": "5b1b199daa74a4626e723be701623367482d2d4d49506518f39185cb0d2a658c" + } + }, + { + "targets": 1, + "registers": 2, + "saturated_label": "a", + "word": [ + [ + "b", + 3, + 2 + ], + [ + "b", + 3, + 2 + ], + [ + "b", + 1, + 1 + ], + [ + "a", + 1, + 1 + ], + [ + "b", + 1, + 1 + ] + ], + "trace": { + "opposite_count": 4, + "image_rank": 2, + "covector_rank": 2, + "cuts_sha256": "8e0ab881e021f1d8ea2a2e34e9e04db2a0363496c2f086407739c43dece87a19" + } + }, + { + "targets": 2, + "registers": 2, + "saturated_label": "a", + "word": [ + [ + "b", + 1, + 3 + ], + [ + "a", + 1, + 3 + ], + [ + "b", + 1, + 3 + ], + [ + "b", + 3, + 2 + ], + [ + "a", + 3, + 2 + ], + [ + "b", + 3, + 2 + ] + ], + "trace": { + "opposite_count": 4, + "image_rank": 2, + "covector_rank": 2, + "cuts_sha256": "3e243ab9a6e6fbc63801634f4980c198e2593488f5f91f5d38931c6462a2417b" + } + }, + { + "targets": 2, + "registers": 2, + "saturated_label": "b", + "word": [ + [ + "a", + 1, + 3 + ], + [ + "b", + 1, + 3 + ], + [ + "a", + 1, + 3 + ], + [ + "a", + 3, + 2 + ], + [ + "b", + 3, + 2 + ], + [ + "a", + 3, + 2 + ] + ], + "trace": { + "opposite_count": 4, + "image_rank": 2, + "covector_rank": 2, + "cuts_sha256": "3e243ab9a6e6fbc63801634f4980c198e2593488f5f91f5d38931c6462a2417b" + } + }, + { + "targets": 2, + "registers": 3, + "saturated_label": "a", + "word": [ + [ + "b", + 1, + 3 + ], + [ + "a", + 1, + 3 + ], + [ + "b", + 1, + 3 + ], + [ + "b", + 3, + 2 + ], + [ + "a", + 3, + 2 + ], + [ + "b", + 3, + 2 + ] + ], + "trace": { + "opposite_count": 4, + "image_rank": 2, + "covector_rank": 2, + "cuts_sha256": "4d5f7e1dbd748ecf4bc511efe71cbf3625c5c948dc5fee4194264eb1220a4ef6" + } + }, + { + "targets": 2, + "registers": 3, + "saturated_label": "b", + "word": [ + [ + "a", + 1, + 3 + ], + [ + "b", + 1, + 3 + ], + [ + "a", + 1, + 3 + ], + [ + "a", + 3, + 2 + ], + [ + "b", + 3, + 2 + ], + [ + "a", + 3, + 2 + ] + ], + "trace": { + "opposite_count": 4, + "image_rank": 2, + "covector_rank": 2, + "cuts_sha256": "4d5f7e1dbd748ecf4bc511efe71cbf3625c5c948dc5fee4194264eb1220a4ef6" + } + }, + { + "targets": 2, + "registers": 3, + "saturated_label": "a", + "word": [ + [ + "b", + 5, + 4 + ], + [ + "b", + 5, + 4 + ], + [ + "b", + 1, + 3 + ], + [ + "a", + 1, + 3 + ], + [ + "b", + 1, + 3 + ], + [ + "b", + 3, + 2 + ], + [ + "a", + 3, + 2 + ], + [ + "b", + 3, + 2 + ] + ], + "trace": { + "opposite_count": 6, + "image_rank": 3, + "covector_rank": 3, + "cuts_sha256": "f4557e0e2581b237cdbb939303652617426df2fcc465b5baf52924b3f621eeba" + } + }, + { + "targets": 3, + "registers": 3, + "saturated_label": "a", + "word": [ + [ + "b", + 1, + 7 + ], + [ + "a", + 1, + 7 + ], + [ + "b", + 1, + 7 + ], + [ + "b", + 3, + 6 + ], + [ + "a", + 3, + 6 + ], + [ + "b", + 3, + 6 + ], + [ + "b", + 6, + 4 + ], + [ + "a", + 6, + 4 + ], + [ + "b", + 6, + 4 + ] + ], + "trace": { + "opposite_count": 6, + "image_rank": 3, + "covector_rank": 3, + "cuts_sha256": "ab285e8ba722b47b8f050f9f2299a3c02e9d9c0b309c3ec178e4a3e4fe675822" + } + }, + { + "targets": 3, + "registers": 3, + "saturated_label": "b", + "word": [ + [ + "a", + 1, + 7 + ], + [ + "b", + 1, + 7 + ], + [ + "a", + 1, + 7 + ], + [ + "a", + 3, + 6 + ], + [ + "b", + 3, + 6 + ], + [ + "a", + 3, + 6 + ], + [ + "a", + 6, + 4 + ], + [ + "b", + 6, + 4 + ], + [ + "a", + 6, + 4 + ] + ], + "trace": { + "opposite_count": 6, + "image_rank": 3, + "covector_rank": 3, + "cuts_sha256": "ab285e8ba722b47b8f050f9f2299a3c02e9d9c0b309c3ec178e4a3e4fe675822" + } + }, + { + "targets": 3, + "registers": 4, + "saturated_label": "a", + "word": [ + [ + "b", + 1, + 7 + ], + [ + "a", + 1, + 7 + ], + [ + "b", + 1, + 7 + ], + [ + "b", + 3, + 6 + ], + [ + "a", + 3, + 6 + ], + [ + "b", + 3, + 6 + ], + [ + "b", + 6, + 4 + ], + [ + "a", + 6, + 4 + ], + [ + "b", + 6, + 4 + ] + ], + "trace": { + "opposite_count": 6, + "image_rank": 3, + "covector_rank": 3, + "cuts_sha256": "45998bb8f549ff69f14a710f25219ca7029c82a7f46df19f2b8617e34ab92a06" + } + }, + { + "targets": 3, + "registers": 4, + "saturated_label": "b", + "word": [ + [ + "a", + 1, + 7 + ], + [ + "b", + 1, + 7 + ], + [ + "a", + 1, + 7 + ], + [ + "a", + 3, + 6 + ], + [ + "b", + 3, + 6 + ], + [ + "a", + 3, + 6 + ], + [ + "a", + 6, + 4 + ], + [ + "b", + 6, + 4 + ], + [ + "a", + 6, + 4 + ] + ], + "trace": { + "opposite_count": 6, + "image_rank": 3, + "covector_rank": 3, + "cuts_sha256": "45998bb8f549ff69f14a710f25219ca7029c82a7f46df19f2b8617e34ab92a06" + } + }, + { + "targets": 3, + "registers": 4, + "saturated_label": "a", + "word": [ + [ + "b", + 9, + 8 + ], + [ + "b", + 9, + 8 + ], + [ + "b", + 1, + 7 + ], + [ + "a", + 1, + 7 + ], + [ + "b", + 1, + 7 + ], + [ + "b", + 3, + 6 + ], + [ + "a", + 3, + 6 + ], + [ + "b", + 3, + 6 + ], + [ + "b", + 6, + 4 + ], + [ + "a", + 6, + 4 + ], + [ + "b", + 6, + 4 + ] + ], + "trace": { + "opposite_count": 8, + "image_rank": 4, + "covector_rank": 4, + "cuts_sha256": "f6d63fcb93c709dea9d879b70c576aa2e7d992ad7c8b44be3d47a47269719fa2" + } + }, + { + "targets": 4, + "registers": 4, + "saturated_label": "a", + "word": [ + [ + "b", + 1, + 15 + ], + [ + "a", + 1, + 15 + ], + [ + "b", + 1, + 15 + ], + [ + "b", + 3, + 14 + ], + [ + "a", + 3, + 14 + ], + [ + "b", + 3, + 14 + ], + [ + "b", + 6, + 12 + ], + [ + "a", + 6, + 12 + ], + [ + "b", + 6, + 12 + ], + [ + "b", + 12, + 8 + ], + [ + "a", + 12, + 8 + ], + [ + "b", + 12, + 8 + ] + ], + "trace": { + "opposite_count": 8, + "image_rank": 4, + "covector_rank": 4, + "cuts_sha256": "b1d4f9692747ecc2a78696e958d63c3d0267b8ca63eec8fd395226587ecbc348" + } + }, + { + "targets": 4, + "registers": 4, + "saturated_label": "b", + "word": [ + [ + "a", + 1, + 15 + ], + [ + "b", + 1, + 15 + ], + [ + "a", + 1, + 15 + ], + [ + "a", + 3, + 14 + ], + [ + "b", + 3, + 14 + ], + [ + "a", + 3, + 14 + ], + [ + "a", + 6, + 12 + ], + [ + "b", + 6, + 12 + ], + [ + "a", + 6, + 12 + ], + [ + "a", + 12, + 8 + ], + [ + "b", + 12, + 8 + ], + [ + "a", + 12, + 8 + ] + ], + "trace": { + "opposite_count": 8, + "image_rank": 4, + "covector_rank": 4, + "cuts_sha256": "b1d4f9692747ecc2a78696e958d63c3d0267b8ca63eec8fd395226587ecbc348" + } + }, + { + "targets": 4, + "registers": 5, + "saturated_label": "a", + "word": [ + [ + "b", + 1, + 15 + ], + [ + "a", + 1, + 15 + ], + [ + "b", + 1, + 15 + ], + [ + "b", + 3, + 14 + ], + [ + "a", + 3, + 14 + ], + [ + "b", + 3, + 14 + ], + [ + "b", + 6, + 12 + ], + [ + "a", + 6, + 12 + ], + [ + "b", + 6, + 12 + ], + [ + "b", + 12, + 8 + ], + [ + "a", + 12, + 8 + ], + [ + "b", + 12, + 8 + ] + ], + "trace": { + "opposite_count": 8, + "image_rank": 4, + "covector_rank": 4, + "cuts_sha256": "52ae4e940b7f2441298902670aec9ee481fe58dc67b9211427785900f1bfca97" + } + }, + { + "targets": 4, + "registers": 5, + "saturated_label": "b", + "word": [ + [ + "a", + 1, + 15 + ], + [ + "b", + 1, + 15 + ], + [ + "a", + 1, + 15 + ], + [ + "a", + 3, + 14 + ], + [ + "b", + 3, + 14 + ], + [ + "a", + 3, + 14 + ], + [ + "a", + 6, + 12 + ], + [ + "b", + 6, + 12 + ], + [ + "a", + 6, + 12 + ], + [ + "a", + 12, + 8 + ], + [ + "b", + 12, + 8 + ], + [ + "a", + 12, + 8 + ] + ], + "trace": { + "opposite_count": 8, + "image_rank": 4, + "covector_rank": 4, + "cuts_sha256": "52ae4e940b7f2441298902670aec9ee481fe58dc67b9211427785900f1bfca97" + } + }, + { + "targets": 4, + "registers": 5, + "saturated_label": "a", + "word": [ + [ + "b", + 17, + 16 + ], + [ + "b", + 17, + 16 + ], + [ + "b", + 1, + 15 + ], + [ + "a", + 1, + 15 + ], + [ + "b", + 1, + 15 + ], + [ + "b", + 3, + 14 + ], + [ + "a", + 3, + 14 + ], + [ + "b", + 3, + 14 + ], + [ + "b", + 6, + 12 + ], + [ + "a", + 6, + 12 + ], + [ + "b", + 6, + 12 + ], + [ + "b", + 12, + 8 + ], + [ + "a", + 12, + 8 + ], + [ + "b", + 12, + 8 + ] + ], + "trace": { + "opposite_count": 10, + "image_rank": 5, + "covector_rank": 5, + "cuts_sha256": "2491dcbe19e550dfe9f99aface8df8d57089364534a73e809056974b933c42e7" + } + }, + { + "targets": 5, + "registers": 5, + "saturated_label": "a", + "word": [ + [ + "b", + 1, + 31 + ], + [ + "a", + 1, + 31 + ], + [ + "b", + 1, + 31 + ], + [ + "b", + 3, + 30 + ], + [ + "a", + 3, + 30 + ], + [ + "b", + 3, + 30 + ], + [ + "b", + 6, + 28 + ], + [ + "a", + 6, + 28 + ], + [ + "b", + 6, + 28 + ], + [ + "b", + 12, + 24 + ], + [ + "a", + 12, + 24 + ], + [ + "b", + 12, + 24 + ], + [ + "b", + 24, + 16 + ], + [ + "a", + 24, + 16 + ], + [ + "b", + 24, + 16 + ] + ], + "trace": { + "opposite_count": 10, + "image_rank": 5, + "covector_rank": 5, + "cuts_sha256": "fe17ac973842cab87ccb042ec2144831a355593342496e9be3c620f15f46d3c0" + } + }, + { + "targets": 5, + "registers": 5, + "saturated_label": "b", + "word": [ + [ + "a", + 1, + 31 + ], + [ + "b", + 1, + 31 + ], + [ + "a", + 1, + 31 + ], + [ + "a", + 3, + 30 + ], + [ + "b", + 3, + 30 + ], + [ + "a", + 3, + 30 + ], + [ + "a", + 6, + 28 + ], + [ + "b", + 6, + 28 + ], + [ + "a", + 6, + 28 + ], + [ + "a", + 12, + 24 + ], + [ + "b", + 12, + 24 + ], + [ + "a", + 12, + 24 + ], + [ + "a", + 24, + 16 + ], + [ + "b", + 24, + 16 + ], + [ + "a", + 24, + 16 + ] + ], + "trace": { + "opposite_count": 10, + "image_rank": 5, + "covector_rank": 5, + "cuts_sha256": "fe17ac973842cab87ccb042ec2144831a355593342496e9be3c620f15f46d3c0" + } + }, + { + "targets": 5, + "registers": 6, + "saturated_label": "a", + "word": [ + [ + "b", + 1, + 31 + ], + [ + "a", + 1, + 31 + ], + [ + "b", + 1, + 31 + ], + [ + "b", + 3, + 30 + ], + [ + "a", + 3, + 30 + ], + [ + "b", + 3, + 30 + ], + [ + "b", + 6, + 28 + ], + [ + "a", + 6, + 28 + ], + [ + "b", + 6, + 28 + ], + [ + "b", + 12, + 24 + ], + [ + "a", + 12, + 24 + ], + [ + "b", + 12, + 24 + ], + [ + "b", + 24, + 16 + ], + [ + "a", + 24, + 16 + ], + [ + "b", + 24, + 16 + ] + ], + "trace": { + "opposite_count": 10, + "image_rank": 5, + "covector_rank": 5, + "cuts_sha256": "de5c2e889e24a3effbed1f9f4b02bb392f3b677655c22601e2117f7f301030e3" + } + }, + { + "targets": 5, + "registers": 6, + "saturated_label": "b", + "word": [ + [ + "a", + 1, + 31 + ], + [ + "b", + 1, + 31 + ], + [ + "a", + 1, + 31 + ], + [ + "a", + 3, + 30 + ], + [ + "b", + 3, + 30 + ], + [ + "a", + 3, + 30 + ], + [ + "a", + 6, + 28 + ], + [ + "b", + 6, + 28 + ], + [ + "a", + 6, + 28 + ], + [ + "a", + 12, + 24 + ], + [ + "b", + 12, + 24 + ], + [ + "a", + 12, + 24 + ], + [ + "a", + 24, + 16 + ], + [ + "b", + 24, + 16 + ], + [ + "a", + 24, + 16 + ] + ], + "trace": { + "opposite_count": 10, + "image_rank": 5, + "covector_rank": 5, + "cuts_sha256": "de5c2e889e24a3effbed1f9f4b02bb392f3b677655c22601e2117f7f301030e3" + } + }, + { + "targets": 5, + "registers": 6, + "saturated_label": "a", + "word": [ + [ + "b", + 33, + 32 + ], + [ + "b", + 33, + 32 + ], + [ + "b", + 1, + 31 + ], + [ + "a", + 1, + 31 + ], + [ + "b", + 1, + 31 + ], + [ + "b", + 3, + 30 + ], + [ + "a", + 3, + 30 + ], + [ + "b", + 3, + 30 + ], + [ + "b", + 6, + 28 + ], + [ + "a", + 6, + 28 + ], + [ + "b", + 6, + 28 + ], + [ + "b", + 12, + 24 + ], + [ + "a", + 12, + 24 + ], + [ + "b", + 12, + 24 + ], + [ + "b", + 24, + 16 + ], + [ + "a", + 24, + 16 + ], + [ + "b", + 24, + 16 + ] + ], + "trace": { + "opposite_count": 12, + "image_rank": 6, + "covector_rank": 6, + "cuts_sha256": "25c8eaafc2b43153e991e413d25bfba5f38e7c773e14b129f30ddc2086bddbc9" + } + } + ], + "controls": [ + "omitted_paid_call_0", + "omitted_paid_call_1", + "omitted_paid_call_2", + "omitted_paid_call_3", + "omitted_paid_call_4", + "omitted_paid_call_5", + "unrestored_dirty_extra", + "missing_target", + "expanded_paid_alphabet", + "nilpotent_scalar_factor", + "boolean_projector", + "wrong_address_label", + "one_span_does_not_suffice", + "trace_parity_is_not_matrix_sign", + "natural_alias" + ], + "censuses": [ + { + "registers": 1, + "depth": 5, + "layers": [ + { + "length": 0, + "states_with_label_count": 1, + "sha256": "b413f47d13ee2fe6c845b2ee141af81de858df4ec549a58b7970bb96645bc8d2", + "target_hits": [] + }, + { + "length": 1, + "states_with_label_count": 2, + "sha256": "7a834b278ea57eb327d270ce90232066be8c10053945ae9ab7b9be7cda9c1f5f", + "target_hits": [] + }, + { + "length": 2, + "states_with_label_count": 4, + "sha256": "c5f7698ce8d523a813f7443d503f5e50b49e84234792f41c5ed622ef5c3b82f7", + "target_hits": [] + }, + { + "length": 3, + "states_with_label_count": 6, + "sha256": "7e1d6b800dc6a5b634d53b817246ea3e814a9f3ea8ddf198ce59ecb9e81ec084", + "target_hits": [ + { + "targets": 1, + "counts": [ + 1, + 2 + ] + }, + { + "targets": 1, + "counts": [ + 2, + 1 + ] + } + ] + }, + { + "length": 4, + "states_with_label_count": 9, + "sha256": "e8266b53a0c149b7a39c4d783c2698f1028e0c495d48d8312f464cf9eab6abc8", + "target_hits": [] + }, + { + "length": 5, + "states_with_label_count": 12, + "sha256": "9b79a7b57b3ad795cffa0f52df6ed43e2296aa31ef48e23d25ee388a5104b54e", + "target_hits": [ + { + "targets": 1, + "counts": [ + 1, + 4 + ] + }, + { + "targets": 1, + "counts": [ + 2, + 3 + ] + }, + { + "targets": 1, + "counts": [ + 3, + 2 + ] + }, + { + "targets": 1, + "counts": [ + 4, + 1 + ] + } + ] + } + ] + }, + { + "registers": 2, + "depth": 6, + "layers": [ + { + "length": 0, + "states_with_label_count": 1, + "sha256": "4bd6c93a61bd69fd69e05335e0ad50f67aadcd8568faded29f3a466f45a66a0c", + "target_hits": [] + }, + { + "length": 1, + "states_with_label_count": 12, + "sha256": "09270f6b2a1ef79354be944833b3cf79348e79254c082e589721800d9ded836c", + "target_hits": [] + }, + { + "length": 2, + "states_with_label_count": 82, + "sha256": "df38bad2b90ec6b7a626aba3e35a5a830b7d58329dbe0f7964b20f55b829edfb", + "target_hits": [] + }, + { + "length": 3, + "states_with_label_count": 496, + "sha256": "704ade1316fa95110e91b6a0eba3757757e6504861537e3a1509c5619b9065ef", + "target_hits": [ + { + "targets": 1, + "counts": [ + 1, + 2 + ] + }, + { + "targets": 1, + "counts": [ + 2, + 1 + ] + } + ] + }, + { + "length": 4, + "states_with_label_count": 2640, + "sha256": "9913c1c0c869c0b30b39b4ed26c63258a9a4151e0a39089f568d2abef4b42490", + "target_hits": [] + }, + { + "length": 5, + "states_with_label_count": 13552, + "sha256": "662b7382688b7ab9ce44c98e2e3f6fbba68a7f8606c517de595197decf27cdc8", + "target_hits": [ + { + "targets": 1, + "counts": [ + 1, + 4 + ] + }, + { + "targets": 1, + "counts": [ + 2, + 3 + ] + }, + { + "targets": 1, + "counts": [ + 3, + 2 + ] + }, + { + "targets": 1, + "counts": [ + 4, + 1 + ] + } + ] + }, + { + "length": 6, + "states_with_label_count": 58408, + "sha256": "881e8b505850eb42ab21861e66bc379ac28570d2dc1aa34585aa8dbc2e31c195", + "target_hits": [ + { + "targets": 2, + "counts": [ + 2, + 4 + ] + }, + { + "targets": 2, + "counts": [ + 3, + 3 + ] + }, + { + "targets": 2, + "counts": [ + 4, + 2 + ] + } + ] + } + ] + } + ], + "two_swap_attainers": { + "half_words_each": 1728, + "total": 1296, + "by_a_count": { + "2": 324, + "3": 648, + "4": 324 + }, + "saturated_proof_traces": 648, + "words_sha256": "ede299ad4b2e840a929e8cf0f794326df2080355cd197e29f54f8b3d989dec4c" + }, + "three_swap_minimum": 9, + "four_swap_remaining_counts_below_twelve": [ + [ + 5, + 5 + ] + ], + "four_swap_minimum_interval": [ + 10, + 12 + ], + "four_swap_ten_call_workspace_cap": 6 +} diff --git a/research/coordinate-cnot-label-saturation/SOURCES.json b/research/coordinate-cnot-label-saturation/SOURCES.json new file mode 100644 index 0000000000..7414fa77f1 --- /dev/null +++ b/research/coordinate-cnot-label-saturation/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/coordinate-cnot-register-bound/PROOF.md", + "usage": "input", + "git_blob": "68fee5b5ccff5329e27300e40dcbd483640dd6b7", + "sha256": "bcee89f92dcce8253bd7eae6e924ddff598c900da81979c6171a412f03d765e1" + } + ] +} diff --git a/research/coordinate-cnot-label-saturation/TASK.json b/research/coordinate-cnot-label-saturation/TASK.json new file mode 100644 index 0000000000..f2ee8d3b73 --- /dev/null +++ b/research/coordinate-cnot-label-saturation/TASK.json @@ -0,0 +1,166 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "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": "Formal F2[GL2(F2)] coordinate-CNOT calls for t coordinate-SWAP targets, arbitrary finite dirty register count; prove or falsify the label-saturation implication n_a=t => n_b>=2t and its symmetric counterpart. Apply to t=3 and t=4.", + "scope_change_reason": "The selected card explicitly permits a specified nonabelian family and a target-specific relaxation. PR1414/1491/1541 establish earlier coordinate-SWAP cases; PR1705 leaves four targets at 8, 10 or 12 calls. This investigates a uniform missing label-count inequality, not a repeated bounded census.", + "bottleneck_link": "A lower bound screens a fully restored paid-call mechanism before larger search; scalar mixing and workspace are optimistically free, but every address call and undo is charged. No selected bit profile or kappa change follows.", + "budget_minutes": 60, + "stop_rule": "Stop after a proof or counterexample to saturation and its t=3,4 consequences. No 10-call four-swap synthesis or larger SAT search. Freeze scope by 08:12 UTC and reserve final quarter for replay and handoff.", + "outcome": "negative-result", + "evidence": "PROOF.md: uniform label-saturation theorem and equality-case workspace rigidity; RESULT.json: two complete finite censuses, 1296 two-swap attainers with 648 saturation traces, 25 larger witnesses, 15 primary controls; independent regular-operator replay and five package test groups pass.", + "author": "Ross Richardson, with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in reasoning, implementation, verification and writing; one agent, no human or Lean proof review.", + "open_questions": [ + { + "question": "Can a ten-call word implement four swaps with exactly five calls of each label?", + "why_it_matters": "This is the only potentially improving label count if the proposed saturation implication holds.", + "first_step": "Use the credited q-t role compression to reduce to at most six roles and construct a source-bound proof-producing search.", + "blocked_by": "The saturation lemma does not decide the balanced 5+5 case; full formal endpoint and dirty workspace are required." + } + ], + "chooser_nonce": "8e7454be62cc38c3ccc7edd6bd6d2bc2", + "catalogue_scope_key": "7084092dd726e7ba1f2f", + "scope_key": "GL2-coordinate-CNOT/label-saturation/arbitrary-dirty-roles/t3-t4", + "predecessors": [ + { + "pr": 1414, + "head": "9e1640094f649ba6db9742796825a8d6c238989b", + "credit": "commdata2338: model, two-swap theorem, sign quotient" + }, + { + "pr": 1541, + "head": "194724d87505ec2517fdca1c1884da12398f4c33", + "credit": "Cinna Davis: arbitrary-workspace three-swap theorem and q-t compression" + }, + { + "pr": 1705, + "head": "ad6b7d641b3e8576a95add7981fa75b6a8278fbc", + "credit": "Aaron Wang: four-register four-swap finite bounds" + }, + { + "pr": 1491, + "head": "69638b36c691d3e1b8463526fd68c849e8d1aef9", + "credit": "commdata2338: finite three-swap certificate" + }, + { + "pr": 1333, + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "credit": "Gareth Davidson: scalar normalization and restricted generator question" + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1715", + "optimistic_budget": { + "direct_paid_calls": "3t", + "scalar_mixing_and_workspace": "free lower-bound relaxation", + "required_improvement": "four swaps in fewer than 12 fully restored formal paid calls", + "remaining_after_screen": "ten calls, five of each label, at most six roles using credited compression" + }, + "verified_environment": { + "python": "CPython 3.12.12; optimized secondary replay on CPython 3.14.6", + "platform": "macOS arm64" + }, + "first_steps": { + "research_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; complex remains binding", + "alternative_card_control": "PASS_R439_BSECTION_STARS; existing H2/K replacement already covered" + }, + "scope_frozen_at": "2026-10-14T07:45:00Z", + "context_proof": { + "pr": 1541, + "head": "194724d87505ec2517fdca1c1884da12398f4c33", + "path": "research/three-swap-compression-seed6/PROOF.md", + "sha256": "b60b9abd328ae0c45fcb86af19bb5d339d531d329e5f9886ad7b0c0f8d8b3a1e", + "git_blob": "9a1e4dfc6dcb0632efa24aacc2313ac17b10e5bf", + "usage": "context; credited reductions restated, no implementation imported" + }, + "overlap_entry": { + "searched_at": "2026-10-14T07:33:30.794947+00:00", + "terms": [ + "label saturation", + "saturated label", + "coordinate-CNOT", + "four-swap" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T07:30:41.945043+00:00", + "complete_pagination": true, + "records": 398 + }, + "discussions": { + "fetched_at": "2026-10-14T07:32:04.617492+00:00", + "complete_pagination": true, + "records": 353 + } + }, + "local_records": 871, + "warnings": [], + "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.", + "matches_total": 25 + }, + "overlap_final": { + "searched_at": "2026-10-14T07:51:19.516826+00:00", + "terms": [ + "coordinate-CNOT", + "label saturation", + "saturated label", + "four-swap" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T07:48:08.949436+00:00", + "complete_pagination": true, + "records": 408 + }, + "discussions": { + "fetched_at": "2026-10-14T07:49:30.421503+00:00", + "complete_pagination": true, + "records": 358 + } + }, + "local_records": 873, + "warnings": [], + "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.", + "matches_total": 31, + "assessment": "All 31 returned matches inspected by source/title; exact relevant proof/head reads and full cached concrete-term body scan found no duplicate saturation lemma beyond this claim. The related results retain credit. This is not a literature novelty certificate." + }, + "predecessor_heads_rechecked_at": "2026-10-14T07:50:00Z" +} diff --git a/research/coordinate-cnot-label-saturation/VERIFY.json b/research/coordinate-cnot-label-saturation/VERIFY.json new file mode 100644 index 0000000000..c402278f87 --- /dev/null +++ b/research/coordinate-cnot-label-saturation/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coordinate-cnot-register-bound/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact formal censuses and complete two-swap attainers; saturated proof traces, all positive witnesses, source binding, 15 semantic controls and typed receipt equality." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate faithful regular-operator censuses, full positive endpoints forward/reverse, 235 omission controls and complete attainer digest." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 180, + "checks": "Five actual-file corruption and optimized read-only minimal-export test groups." + } + ] +} diff --git a/research/coordinate-cnot-label-saturation/independent.py b/research/coordinate-cnot-label-saturation/independent.py new file mode 100644 index 0000000000..bbd8e3b973 --- /dev/null +++ b/research/coordinate-cnot-label-saturation/independent.py @@ -0,0 +1,217 @@ +#!/usr/bin/env python3 +"""Code-disjoint faithful regular-operator corroboration; Apache-2.0. + +Written in the same Codex session. Imports no primary or predecessor engine. +Independence means a different implementation, not independent human review. +""" +from collections import defaultdict +import hashlib +import itertools +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read(path): + def pairs(items): + result = {} + for k, v in items: + require(k not in result, 'duplicate key') + result[k] = v + return result + + def constant(_): + raise ValueError('nonfinite value') + + return json.loads(path.read_text(), object_pairs_hook=pairs, parse_constant=constant) + + +def encoded(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False) + + +def same(a, b): + require(encoded(a) == encoded(b), 'independent receipt mismatch') + + +def compose(p, q): + return tuple(p[x-1] for x in q) + + +def rows_from_permutation(p): + # The images of basis vectors 1 and 2 are the two binary matrix columns. + return ((p[0] & 1) | ((p[1] & 1) << 1), + ((p[0] >> 1) & 1) | (p[1] & 2)) + + +PERMS = tuple(sorted(itertools.permutations((1, 2, 3)), key=rows_from_permutation)) +INDEX = {p: i for i, p in enumerate(PERMS)} +ONE = INDEX[(1, 2, 3)] +# a(x,y)=(x+y,y), b(x,y)=(x,x+y), s(x,y)=(y,x). +ADDRESS = {'a': (1, 3, 2), 'b': (3, 2, 1), 's': (2, 1, 3)} +REGULAR = {label: tuple(INDEX[compose(p, h)] for h in PERMS) + for label, p in ADDRESS.items()} + + +def unit(n): + return tuple(1 << i for i in range(n)) + + +def endpoint(r, t): + rows = list(unit(6*r)) + for register in range(t): + for h in range(6): + rows[6*register+h] = 1 << (6*register+REGULAR['s'][h]) + return tuple(rows) + + +def generators(r): + # Enumerate binary scalar matrices and filter rank one/idempotence, + # separately from the primary u,v enumeration. + out = [] + for rows in itertools.product(range(1 << r), repeat=r): + nonzero = set(rows)-{0} + if len(nonzero) != 1: + continue + v = next(iter(nonzero)) + u = sum((row != 0) << i for i, row in enumerate(rows)) + if sum(((u >> i) & 1)*((v >> i) & 1) for i in range(r)) % 2 != 1: + continue + out.extend([(label, u, v) for label in ('a', 'b')]) + return sorted(out) + + +def apply(state, gate, r): + label, u, v = gate + require(label in ('a', 'b'), 'address alphabet') + require(type(u) is int and type(v) is int and 0 < u < 2**r and 0 < v < 2**r, + 'projector domain') + require(sum(((u >> i) & 1)*((v >> i) & 1) for i in range(r)) % 2 == 1, + 'projector idempotence') + mixed = [0]*6 + for j in range(r): + if v >> j & 1: + for h in range(6): + mixed[h] ^= state[6*j+h] + delta = [mixed[h] ^ mixed[REGULAR[label][h]] for h in range(6)] + result = list(state) + for i in range(r): + if u >> i & 1: + for h in range(6): + result[6*i+h] ^= delta[h] + return tuple(result) + + +def run(word, r): + state = unit(6*r) + for gate in word: + state = apply(state, gate, r) + return state + + +def coefficients(state, r): + # The identity-basis column of a left-regular block is its full formal + # coefficient vector. This extraction is injective on constructed blocks. + return tuple(sum(((state[6*i+h] >> (6*j+ONE)) & 1) << (6*j+h) + for j in range(r) for h in range(6)) for i in range(r)) + + +def census(r, depth): + alphabet = generators(r) + layer = {0: {unit(6*r)}} + receipt = [] + for q in range(depth+1): + digest = hashlib.sha256() + hits = [] + total = 0 + for na, states in sorted(layer.items()): + total += len(states) + formal_rows = sorted(coefficients(state, r) for state in states) + require(len(set(formal_rows)) == len(states), 'faithful extraction collision') + for rows in formal_rows: + digest.update(bytes([na])) + for row in rows: + digest.update(row.to_bytes(r, 'little')) + for t in range(1, r+1): + if endpoint(r, t) in states: + hits.append({'targets': t, 'counts': [na, q-na]}) + receipt.append({'length': q, 'states_with_label_count': total, + 'sha256': digest.hexdigest(), 'target_hits': hits}) + if q == depth: + break + following = {} + for na, states in layer.items(): + for state in states: + for gate in alphabet: + following.setdefault(na+(gate[0] == 'a'), set()).add(apply(state, gate, r)) + layer = following + return {'registers': r, 'depth': depth, 'layers': receipt} + + +def attainers(): + alphabet = generators(2) + first = defaultdict(list) + for word in itertools.product(alphabet, repeat=3): + first[run(word, 2)].append(word) + words = [] + counts = {2: 0, 3: 0, 4: 0} + for backwards in itertools.product(alphabet, repeat=3): + state = endpoint(2, 2) + for gate in backwards: + state = apply(state, gate, 2) + for prefix in first.get(state, []): + word = prefix+tuple(reversed(backwards)) + a_count = sum(g[0] == 'a' for g in word) + require(a_count in counts, 'attainer label count') + counts[a_count] += 1 + words.append(word) + return {'half_words_each': len(alphabet)**3, 'total': len(words), 'by_a_count': counts, + 'saturated_proof_traces': counts[2]+counts[4], + 'words_sha256': hashlib.sha256(encoded(sorted(words)).encode()).hexdigest()} + + +def main(): + result = read(HERE/'RESULT.json') + expected_domains = sorted( + [(t, t+extra, label, 3*t) for t in range(1, 6) + for extra in (0, 1) for label in ('a', 'b')] + + [(t, t+1, 'a', 3*t+2) for t in range(1, 6)]) + actual_domains = sorted((w['targets'], w['registers'], w['saturated_label'], len(w['word'])) + for w in result['witnesses']) + same(actual_domains, expected_domains) + columns = mutations = 0 + for w in result['witnesses']: + r, t, word = w['registers'], w['targets'], w['word'] + require(type(r) is int and type(t) is int and 1 <= t <= r <= 6, 'witness domain') + require(sum(gate[0] == w['saturated_label'] for gate in word) == t, + 'saturated label count') + same(run(word, r), endpoint(r, t)) + same(run(list(reversed(word)), r), endpoint(r, t)) + columns += 12*r # All faithful columns, forward and reverse. + for i in range(len(word)): + require(run(word[:i]+word[i+1:], r) != endpoint(r, t), 'omitted call accepted') + mutations += 1 + same([census(1, 5), census(2, 6)], result['censuses']) + same(attainers(), result['two_swap_attainers']) + # Explicit literal rank-one/trace near misses, computed without primary code. + rows = [[int((u >> i) & 1) for i in range(3)] for u in (1, 2, 4, 7)] + require(all(sum(row) % 2 == 1 for row in rows), 'zero-sum near-miss legality') + require(all(sum(row[i] for row in rows) % 2 == 0 for i in range(3)), 'zero sum') + require(len(set(tuple(row) for row in rows)) == 4, 'near-miss rows') + print(f'PASS_INDEPENDENT_LABEL_SATURATION faithful_columns={columns} ' + f'omission_controls={mutations} complete_censuses=2 attainers=1296 no_new_kappa') + + +if __name__ == '__main__': + try: + main() + except (ValueError, OSError, KeyError, TypeError) as exc: + print('REJECT_INDEPENDENT_LABEL_SATURATION:', exc, file=sys.stderr) + raise SystemExit(1) diff --git a/research/coordinate-cnot-label-saturation/test_package.py b/research/coordinate-cnot-label-saturation/test_package.py new file mode 100644 index 0000000000..9fbadac49a --- /dev/null +++ b/research/coordinate-cnot-label-saturation/test_package.py @@ -0,0 +1,124 @@ +#!/usr/bin/env python3 +"""Actual-file corruptions and optimized read-only relocation; Apache-2.0.""" +import contextlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +INPUT = Path('research/coordinate-cnot-register-bound/PROOF.md') + + +@contextlib.contextmanager +def exported(): + with tempfile.TemporaryDirectory(prefix='cnot-label-saturation-') as directory: + root = Path(directory) + package = root/'research'/PACKAGE.name + shutil.copytree(PACKAGE, package, ignore=shutil.ignore_patterns('__pycache__')) + (root/INPUT).parent.mkdir(parents=True) + shutil.copy2(ROOT/INPUT, root/INPUT) + yield root, package + + +def run(package, script, optimized=True): + argv = [sys.executable, '-I', '-B'] + if optimized: + argv.append('-O') + return subprocess.run(argv+[str(package/script)], cwd=package.parents[1], + text=True, capture_output=True, timeout=90) + + +class PackageTests(unittest.TestCase): + def test_readonly_minimal_export(self): + with exported() as (root, package): + files = [p for p in root.rglob('*') if p.is_file()] + before = {p.relative_to(root): p.read_bytes() for p in files} + try: + for p in files: + p.chmod(0o444) + for script in ('verify.py', 'independent.py'): + result = run(package, script) + self.assertEqual(result.returncode, 0, result.stdout+result.stderr) + self.assertEqual(before, {p.relative_to(root): p.read_bytes() for p in files}) + finally: + for p in files: + p.chmod(0o644) + + def test_source_bytes_and_missing_input(self): + for missing in (False, True): + with self.subTest(missing=missing), exported() as (root, package): + if missing: + (root/INPUT).unlink() + else: + (root/INPUT).write_bytes((root/INPUT).read_bytes()+b'\ncorruption\n') + result = run(package, 'verify.py') + self.assertNotEqual(result.returncode, 0) + self.assertIn('REJECT_LABEL_SATURATION', result.stderr) + + def test_typed_receipt_corruptions(self): + def changed_minimum(d): + d['four_swap_minimum_interval'] = [12, 12] + + def bool_count(d): + d['schema_version'] = True + + def float_count(d): + d['three_swap_minimum'] = 9.0 + + def proof_cut(d): + d['witnesses'][0]['trace']['covector_rank'] = 0 + + for mutate in (changed_minimum, bool_count, float_count, proof_cut): + with self.subTest(mutation=mutate.__name__), exported() as (_, package): + path = package/'RESULT.json' + data = json.loads(path.read_text()) + mutate(data) + path.write_text(json.dumps(data)) + result = run(package, 'verify.py') + self.assertNotEqual(result.returncode, 0) + self.assertIn('receipt mismatch', result.stderr) + + def test_both_engines_reject_word_and_census_corruptions(self): + for mutation in ('word', 'census', 'attainer', 'missing_witness'): + with self.subTest(mutation=mutation), exported() as (_, package): + path = package/'RESULT.json' + data = json.loads(path.read_text()) + if mutation == 'word': + data['witnesses'][0]['word'].pop() + elif mutation == 'census': + data['censuses'][1]['layers'][6]['sha256'] = '0'*64 + elif mutation == 'attainer': + data['two_swap_attainers']['by_a_count']['2'] -= 1 + else: + data['witnesses'].pop() + path.write_text(json.dumps(data)) + for script in ('verify.py', 'independent.py'): + result = run(package, script) + self.assertNotEqual(result.returncode, 0, result.stdout) + self.assertIn('REJECT_', result.stderr) + + def test_duplicate_nonfinite_and_source_inventory(self): + for mutation in ('duplicate', 'nonfinite', 'source'): + with self.subTest(mutation=mutation), exported() as (_, package): + path = package/'RESULT.json' + if mutation == 'duplicate': + path.write_text('{"schema_version":1,'+path.read_text()[1:]) + elif mutation == 'nonfinite': + path.write_text('{"bad":NaN,'+path.read_text()[1:]) + else: + path = package/'SOURCES.json' + data = json.loads(path.read_text()) + data['files'] = [r for r in data['files'] if r['usage'] != 'input'] + path.write_text(json.dumps(data)) + result = run(package, 'verify.py') + self.assertNotEqual(result.returncode, 0, result.stdout) + self.assertIn('REJECT_', result.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/coordinate-cnot-label-saturation/verify.py b/research/coordinate-cnot-label-saturation/verify.py new file mode 100644 index 0000000000..e7109cce0e --- /dev/null +++ b/research/coordinate-cnot-label-saturation/verify.py @@ -0,0 +1,420 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the written label-saturation proof; Apache-2.0. + +Prepared for Ross Richardson with substantial OpenAI Codex assistance. +No predecessor executable is imported. This is not a proof-assistant kernel. +""" +import argparse +from collections import defaultdict +import hashlib +import itertools +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent + + +class Reject(ValueError): + pass + + +def need(condition, message): + if not condition: + raise Reject(message) + + +def load_json(path): + def pairs(items): + out = {} + for key, value in items: + need(key not in out, 'duplicate JSON key') + out[key] = value + return out + + def bad_constant(value): + raise Reject('nonfinite JSON: ' + value) + + return json.loads(Path(path).read_text(), object_pairs_hook=pairs, + parse_constant=bad_constant) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False) + + +def typed_equal(actual, expected): + # JSON booleans/floats must not alias integer receipt fields. + need(canonical(actual) == canonical(expected), 'receipt mismatch') + + +def dot(a, b): + return (a & b).bit_count() & 1 + + +def rank(vectors): + pivots = {} + for value in vectors: + while value: + bit = value.bit_length() - 1 + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return len(pivots) + + +def xor_rows(rows, mask): + out = 0 + for i, row in enumerate(rows): + if mask >> i & 1: + out ^= row + return out + + +def matmul(a, b): + return tuple(xor_rows(b, row) for row in a) + + +def mv(a, vector): + return sum(dot(row, vector) << i for i, row in enumerate(a)) + + +def invert(rows): + n = len(rows) + aug = [row | (1 << (n+i)) for i, row in enumerate(rows)] + for j in range(n): + pivot = next((i for i in range(j, n) if aug[i] >> j & 1), None) + need(pivot is not None, 'singular basis') + aug[j], aug[pivot] = aug[pivot], aug[j] + for i in range(n): + if i != j and aug[i] >> j & 1: + aug[i] ^= aug[j] + return tuple(row >> n for row in aug) + + +G = tuple(sorted(rows for rows in itertools.product(range(4), repeat=2) + if rank(rows) == 2)) +GID = {g: i for i, g in enumerate(G)} +IDENTITY = GID[(1, 2)] +LABELS = {'a': GID[(3, 2)], 'b': GID[(1, 3)]} +SWAP = GID[(2, 1)] +PRODUCT = tuple(tuple(GID[matmul(a, b)] for b in G) for a in G) + + +def identity(r): + return tuple(1 << (6*i+IDENTITY) for i in range(r)) + + +def target(r, t): + return tuple(1 << (6*i+(SWAP if i < t else IDENTITY)) for i in range(r)) + + +def check_gate(gate, r): + need(isinstance(gate, (tuple, list)) and len(gate) == 3, 'gate shape') + label, u, v = gate + need(label in LABELS, 'paid address alphabet') + need(type(u) is int and type(v) is int, 'projector type') + need(0 < u < (1 << r) and 0 < v < (1 << r) and dot(u, v) == 1, + 'rank-one idempotent') + + +def transform(row, label, r): + result = 0 + for j in range(r): + entry = row >> (6*j) & 63 + for h in range(6): + if entry >> h & 1: + result ^= 1 << (6*j+PRODUCT[LABELS[label]][h]) + return result + + +def step(state, gate): + label, u, v = gate + mixed = xor_rows(state, v) + delta = mixed ^ transform(mixed, label, len(state)) + return tuple(row ^ (delta if u >> i & 1 else 0) + for i, row in enumerate(state)) + + +def formal(word, r): + state = identity(r) + for gate in word: + check_gate(gate, r) + state = step(state, gate) + return state + + +def accept(word, r, t): + need(formal(word, r) == target(r, t), 'full formal dirty endpoint') + + +def projectors(r): + return [(u, v) for u in range(1, 1 << r) for v in range(1, 1 << r) + if dot(u, v)] + + +def natural_step(state, gate, r): + label, u, v = gate + source = r if label == 'a' else 0 + destination = 0 if label == 'a' else r + delta = xor_rows(state[source:source+r], v) + rows = list(state) + for i in range(r): + if u >> i & 1: + rows[destination+i] ^= delta + return tuple(rows) + + +def natural_image(state, r): + rows = [0] * (2*r) + for i, row in enumerate(state): + for j in range(r): + entry = row >> (6*j) & 63 + for h, g in enumerate(G): + if entry >> h & 1: + for x in range(2): + for y in range(2): + if g[x] >> y & 1: + rows[x*r+i] ^= 1 << (y*r+j) + return tuple(rows) + + +def sign_sum(word, r): + return tuple(xor_rows([v if u >> i & 1 else 0 for _, u, v in word], + (1 << len(word))-1) for i in range(r)) + + +def trace_saturation(word, r, t, saturated='a'): + accept(word, r, t) + if saturated == 'b': + word = [('b' if label == 'a' else 'a', u, v) for label, u, v in word] + a_images = [u for label, u, _ in word if label == 'a'] + need(len(a_images) == t, 'label is not saturated') + active = (1 << t)-1 + need(rank(a_images) == t and all(u & ~active == 0 for u in a_images), + 'saturated image span') + columns = a_images + [1 << i for i in range(t, r)] + change = tuple(sum(((column >> i) & 1) << j for j, column in enumerate(columns)) + for i in range(r)) + change_inverse = invert(change) + normalized = [(label, mv(change_inverse, u), xor_rows(change, v)) + for label, u, v in word] + accept(normalized, r, t) + need(sign_sum(normalized, r) == tuple(1 << i if i < t else 0 for i in range(r)), + 'full sign matrix') + state = tuple(1 << i for i in range(2*r)) + b_sum = [0]*r + cuts = [] + a_index = 0 + for gate in normalized: + label, u, v = gate + need(all(((row & ((1 << r)-1)) ^ (row >> r)) == 1 << i + for i, row in enumerate(state[:r])), 'top row-sum rigidity') + if label == 'a': + need(u == v == 1 << a_index, 'saturated coordinate projector') + need(state[r+a_index] == (1 << a_index) | (1 << (r+a_index)), + 'chronological bottom row') + need(b_sum[a_index] == 1 << a_index, 'chronological covector span') + a_index += 1 + else: + for i in range(r): + if u >> i & 1: + b_sum[i] ^= v + state = natural_step(state, gate, r) + cuts.append(list(state)) + need(not any(b_sum), 'opposite label sum is not zero') + opposite = [(u, v) for label, u, v in normalized if label == 'b'] + ru, rv = rank([u for u, _ in opposite]), rank([v for _, v in opposite]) + need(ru >= t and rv >= t and ru+rv <= len(opposite), 'zero-sum rank bound') + if len(opposite) == 2*t: + need(all((u | v) & ~active == 0 for _, u, v in normalized), + 'equality workspace rigidity') + return {'opposite_count': len(opposite), 'image_rank': ru, 'covector_rank': rv, + 'cuts_sha256': hashlib.sha256(canonical(cuts).encode()).hexdigest()} + + +def screened_counts(t, q): + if q % 2 != t % 2: + return [] + return [[a, q-a] for a in range(t, q-t+1) + if (a != t or q-a >= 2*t) and (q-a != t or a >= 2*t)] + + +def census(r, depth): + """All exact-length formal states, retaining both paid label counts.""" + generators = [(g, u, v) for g in ('a', 'b') for u, v in projectors(r)] + tables = {g: [transform(row, g, r) for row in range(1 << (6*r))] + for g in ('a', 'b')} + layer = {0: {identity(r)}} + receipt = [] + for q in range(depth+1): + hits = [] + digest = hashlib.sha256() + total = 0 + for na, states in sorted(layer.items()): + total += len(states) + for state in sorted(states): + digest.update(bytes([na])) + for row in state: + digest.update(row.to_bytes(r, 'little')) + for t in range(1, r+1): + if target(r, t) in states: + need([na, q-na] in screened_counts(t, q), 'census contradicts theorem') + hits.append({'targets': t, 'counts': [na, q-na]}) + receipt.append({'length': q, 'states_with_label_count': total, + 'sha256': digest.hexdigest(), 'target_hits': hits}) + if q == depth: + break + following = {} + for na, states in layer.items(): + for state in states: + for g, u, v in generators: + mixed = xor_rows(state, v) + delta = mixed ^ tables[g][mixed] + nxt = tuple(row ^ (delta if u >> i & 1 else 0) + for i, row in enumerate(state)) + following.setdefault(na+(g == 'a'), set()).add(nxt) + layer = following + return {'registers': r, 'depth': depth, 'layers': receipt} + + +def controls(): + results = [] + + def rejects(name, action): + try: + action() + except Reject: + results.append(name) + return + raise Reject('negative control accepted: ' + name) + + w = [('b', 1, 1), ('a', 1, 1), ('b', 1, 1), + ('b', 2, 2), ('a', 2, 2), ('b', 2, 2)] + accept(w, 3, 2) + for i in range(len(w)): + rejects('omitted_paid_call_' + str(i), lambda i=i: accept(w[:i]+w[i+1:], 3, 2)) + rejects('unrestored_dirty_extra', lambda: accept(w+[('b', 5, 4)], 3, 2)) + rejects('missing_target', lambda: accept(w, 3, 3)) + rejects('expanded_paid_alphabet', lambda: accept([('s', 1, 1)], 1, 1)) + rejects('nilpotent_scalar_factor', lambda: formal([('a', 1, 2)], 2)) + rejects('boolean_projector', lambda: formal([('a', True, 1)], 1)) + changed = list(w) + changed[1] = ('b', 1, 1) + rejects('wrong_address_label', lambda: accept(changed, 3, 2)) + # Four projectors sum to zero with image rank THREE but covector rank ONE. + # A one-span-only variant of the proof is therefore false. + us, vs = [1, 2, 4, 7], [7]*4 + need(all(dot(u, v) for u, v in zip(us, vs)), 'near-miss projector legality') + need(sign_sum([('b', u, v) for u, v in zip(us, vs)], 3) == (0, 0, 0), + 'near-miss zero sum') + need(rank(us) == 3 and rank(vs) == 1, 'near-miss ranks') + rejects('one_span_does_not_suffice', lambda: need(rank(vs) >= 3, 'missing covector span')) + fake = [('a', 1, 7), ('a', 2, 7), ('a', 4, 7)] + need(sum(dot(u, v) for _, u, v in fake) % 2 == 3 % 2, 'parity near-miss') + rejects('trace_parity_is_not_matrix_sign', + lambda: need(sign_sum(fake, 3) == (1, 2, 4), 'full sign matrix')) + # The sum of all six formal elements has zero natural image/augmentation. + alias = list(target(2, 1)) + alias[0] ^= 63 << 6 + need(tuple(alias) != target(2, 1), 'formal alias must differ') + need(natural_image(alias, 2) == natural_image(target(2, 1), 2), 'natural alias fixture') + rejects('natural_alias', lambda: need(tuple(alias) == target(2, 1), 'formal equality')) + return results + + +def all_two_swap_attainers(): + """Complete literal six-call census via a 3+3 join, no pruning.""" + generators = [(g, u, v) for g in ('a', 'b') for u, v in projectors(2)] + front = defaultdict(list) + for word in itertools.product(generators, repeat=3): + front[formal(word, 2)].append(word) + counts = {2: 0, 3: 0, 4: 0} + words = [] + for backwards in itertools.product(generators, repeat=3): + state = target(2, 2) + for gate in backwards: + state = step(state, gate) + for prefix in front.get(state, []): + word = prefix + tuple(reversed(backwards)) + a_count = sum(gate[0] == 'a' for gate in word) + need(a_count in counts, 'unexpected two-swap label count') + counts[a_count] += 1 + if a_count != 3: + trace_saturation(word, 2, 2, 'a' if a_count == 2 else 'b') + words.append(word) + return {'half_words_each': len(generators)**3, + 'total': len(words), 'by_a_count': counts, + 'saturated_proof_traces': counts[2]+counts[4], + 'words_sha256': hashlib.sha256(canonical(sorted(words)).encode()).hexdigest()} + + +def source_binding(root=HERE.parents[1]): + manifest = load_json(HERE/'SOURCES.json') + rows = [row for row in manifest['files'] if row['usage'] == 'input'] + need(len(rows) == 1, 'source inventory') + for row in rows: + data = (root/row['path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == row['sha256'], 'source hash') + return [row['sha256'] for row in rows] + + +def build(): + source_hashes = source_binding() + need(len(G) == 6 and PRODUCT[LABELS['a']][PRODUCT[LABELS['b']][LABELS['a']]] == SWAP, + 'address group') + witnesses = [] + for t in range(1, 6): + for extra in (0, 1): + r = t+extra + w = [(label, 1 << i, 1 << i) for i in range(t) for label in ('b', 'a', 'b')] + # Nontrivial active bases exercise the saturation normalization. + change = tuple((1 << i) ^ ((1 << (i+1)) if i+1 < t else 0) for i in range(r)) + inv = invert(change) + w = [(label, mv(change, u), xor_rows(inv, v)) for label, u, v in w] + for opposite in (False, True): + word = [('b' if label == 'a' else 'a', u, v) for label, u, v in w] if opposite else w + saturated = 'b' if opposite else 'a' + trace = trace_saturation(word, r, t, saturated) + witnesses.append({'targets': t, 'registers': r, 'saturated_label': saturated, + 'word': word, 'trace': trace}) + if extra: + # Touch dirty workspace with a fully charged cancelling pair. + gate = ('b', (1 << t) | 1, 1 << t) + dirty_word = [gate, gate]+w + trace = trace_saturation(dirty_word, r, t) + witnesses.append({'targets': t, 'registers': r, 'saturated_label': 'a', + 'word': dirty_word, 'trace': trace}) + return {'schema_version': 1, 'scope': 'written saturation theorem; finite corroboration only; no_new_kappa', + 'sources': source_hashes, + 'screen': {str(t): {str(q): screened_counts(t, q) for q in range(3*t+1)} + for t in range(1, 7)}, + 'witnesses': witnesses, 'controls': controls(), + 'censuses': [census(1, 5), census(2, 6)], + 'two_swap_attainers': all_two_swap_attainers(), + 'three_swap_minimum': 9, 'four_swap_remaining_counts_below_twelve': [[5, 5]], + 'four_swap_minimum_interval': [10, 12], 'four_swap_ten_call_workspace_cap': 6} + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--write', action='store_true', help='regenerate deterministic receipt') + args = ap.parse_args() + result = build() + if args.write: + (HERE/'RESULT.json').write_text(json.dumps(result, indent=2)+'\n') + else: + typed_equal(result, load_json(HERE/'RESULT.json')) + print('PASS_COORDINATE_CNOT_LABEL_SATURATION three_swap_minimum=9 ' + 'four_swap_minimum=10_or_12 ten_call_counts=5+5 ' + f'witnesses={len(result["witnesses"])} controls={len(result["controls"])} no_new_kappa') + + +if __name__ == '__main__': + try: + main() + except (Reject, OSError, KeyError, TypeError, json.JSONDecodeError) as exc: + print('REJECT_LABEL_SATURATION:', exc, file=sys.stderr) + raise SystemExit(1)