From 3d9d5eb2ae784356497771661960ad0455b137db Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 21:31:52 +0000 Subject: [PATCH] feat(research): bound two 3-cycles by ten calls in every dimension A whole-word projection lemma shows no coordinate the target restores can be written or read exactly once, and each target coordinate is written twice. With restriction and quotient removal of idle spectators, every address dimension reduces to n <= 5, excluding lengths up to 9 everywhere and leaving one five-coordinate case for exact cost 12. --- .../two-three-cycles-every-dimension/PROOF.md | 161 +++++++++ .../README.md | 104 ++++++ .../SOURCES.json | 36 ++ .../TASK.json | 76 ++++ .../VERIFY.json | 34 ++ .../verify.py | 324 ++++++++++++++++++ 6 files changed, 735 insertions(+) create mode 100644 research/two-three-cycles-every-dimension/PROOF.md create mode 100644 research/two-three-cycles-every-dimension/README.md create mode 100644 research/two-three-cycles-every-dimension/SOURCES.json create mode 100644 research/two-three-cycles-every-dimension/TASK.json create mode 100644 research/two-three-cycles-every-dimension/VERIFY.json create mode 100644 research/two-three-cycles-every-dimension/verify.py diff --git a/research/two-three-cycles-every-dimension/PROOF.md b/research/two-three-cycles-every-dimension/PROOF.md new file mode 100644 index 0000000000..ca69281283 --- /dev/null +++ b/research/two-three-cycles-every-dimension/PROOF.md @@ -0,0 +1,161 @@ +# Two coordinate 3-cycles in every address dimension + +This is a written proof with finite corroboration in [verify.py](verify.py). +It extends one step of the n = 3 and n = 4 results to every n. Those two +results are cited premises; they are not re-run here. + +## 1. Model + +Work in `M_R(F2[G])`, `G = GL_n(F2)`, as in Mihir Srivastava's #4939 and the +packages that follow it. Write `E_ij = I + e_i e_j^T` (i ≠ j) for the coordinate +CNOT with `x_i <- x_i + x_j`. Say that `E_ij` **writes** `i` and **reads** `j`. +A paid call is + + D(g, N) = I + ([g] + [e]) N, g a coordinate CNOT, N = u v^T, v^T u = 1, + +with `N` a rank-one idempotent in `M_R(F2)`. Free scalar `GL_R(F2)` maps are +allowed; their entries are multiples of `[e]`. Equality is formal: every group +coefficient must agree. + +Let `c` be a coordinate 3-cycle on coordinates 0, 1, 2. Coordinates +`3, ..., n-1` are **spectators**. The question is the least number of paid calls +in a word whose product is `T = diag([c],[c])` at `R = 2`. The target fixes +every spectator row and column. + +Two facts are used throughout. + +* Each paid call is an involution. `([g]+[e])^2 = [g^2] + [e] = 0` because + `g^2 = e` and the characteristic is two. So `D^2 = I`, and every word product + is invertible. +* The augmentation `eps: F2[G] -> F2`, `[g] -> 1`, is a ring homomorphism. Applied + entrywise it maps `M_R(F2[G])` to `M_R(F2)`. For every rank-one idempotent + `N`, `I + N` has rank `R - 1`, because `(I+N)u = u + u(v^T u) = 0`. + +## 2. A coordinate written exactly once + +For a coordinate `k`, let `S_k = {h in G : e_k^T h = e_k^T}`: the elements that +leave row `k` unchanged. It is a subgroup. Let `pi_k` be the F2-linear +projection that keeps the group elements of `S_k` and deletes the others, +applied entrywise. + +**Lemma 1.** Suppose exactly one call `t` of a word writes `k`. Write the +product as `P = A D_t B`. Then + + pi_k(P) = A (I + N_t) B. + +*Proof.* Every call other than `t` has a label in `S_k`, so `A` and `B` have +support in `S_k`. Expand `D_t = (I + N_t) + [g_t] N_t`. The first part is a +scalar matrix. For `a, b in S_k` and `g_t = E_kj`, + + e_k^T a g_t b = e_k^T g_t b = (e_k^T + e_j^T) b = e_k^T + e_j^T b, + +and `e_j^T b ≠ 0` because `b` is invertible. Hence every element in the support +of `A [g_t] N_t B` lies outside `S_k`. Because `S_k` is a subgroup, multiplying +by `A` and `B` keeps `A (I+N_t) B` inside `S_k`. Projection therefore +deletes exactly the second part. QED + +**Corollary 2 (spectator writes).** In a word with product `T`, no spectator is +written exactly once. + +*Proof.* `T` has support `{c}` and `c` fixes the spectator row, so +`pi_k(T) = T`. Lemma 1 gives `A (I+N_t) B = T`. Apply `eps`. The left side has +rank at most `R - 1 = 1`. The right side is `eps(T) = I`, which has rank two. +QED + +**Corollary 3 (target writes).** In a word with product `T`, each of the +coordinates 0, 1, 2 is written at least twice. + +*Proof.* `c` changes row `k` for `k = 0, 1, 2`, so `pi_k(T) = 0`. If no call +wrote `k`, every label would lie in `S_k`, so `pi_k(P) = P = T ≠ 0`. If exactly +one call wrote `k`, Lemma 1 gives `A (I+N_t) B = 0`. Then `eps(A)` and `eps(B)` +are invertible, so `I + N_t = 0`. That is impossible because `I + N_t` has +rank one. QED + +**Reads.** The map `[h] -> [h^T]` is an anti-automorphism of `F2[G]`. Together +with matrix transposition it is an anti-automorphism of `M_R(F2[G])`. It sends +`D(g,N)` to `D(g^T, N^T)`, a legal paid call, and it reverses the word. +`E_ij^T = E_ji`, so a read becomes a write. The target becomes +`diag([c^{-1}],[c^{-1}])`, another coordinate 3-cycle that fixes every +spectator. Corollaries 2 and 3 therefore hold for reads too. No spectator is +read exactly once, and each target coordinate is read at least twice. + +## 3. Removing idle spectators + +**Lemma 4.** Let `k` be a spectator. + +1. If no call writes `k`, the subspace `U = {x : x_k = 0}` is invariant under + every label and under `c`. Restriction to `U` is a homomorphism. It sends + every call that reads `k` to `D(e, N) = I` and keeps every other call. The + result is a word of no greater length for the same target at dimension + `n - 1`. +2. If no call reads `k`, the line spanned by `e_k` is invariant under every + label and under `c`. The induced action on `F2^n / ` is a homomorphism. + It sends every call that writes `k` to `I` and keeps every other call. The + result is again a shorter-or-equal word at dimension `n - 1`. + +*Proof.* A label `E_ij` maps `e_j` to `e_j + e_i` and fixes every other basis +vector. In case 1, no label has `i = k`, so `U` is invariant and the labels +`E_ik` act as the identity on `U`. In case 2, no label has `j = k`, so `` +is invariant and the labels `E_kj` induce the identity on the quotient. The +3-cycle `c` fixes `e_k` and the coordinate `x_k`. Group homomorphisms extend to +the group algebras and to `M_R`, and `[e] + [e] = 0` turns a mapped call with +identity label into `I`. QED + +Apply Lemma 4 repeatedly until neither case applies. Each step lowers the +dimension, so this stops. The final word realizes `T` at dimension `3 + s` and +has length `L' <= L`. Each of its `s` remaining spectators is written and read. +By Corollary 2 and its read form, each is written at least twice and read at +least twice. + +## 4. The bound + +**Theorem.** For every `n >= 3`, no word of length at most 9 realizes +`diag([c],[c])` in `M_2(F2[GL_n(F2)])`. A word of length 10 or 11 exists for some +`n` only if one exists at `n = 5` in which both spectators are written at +least twice and read at least twice, the three target coordinates are each +written and read at least twice, and the write counts (target, spectator) are +`(6,4)`, `(6,5)` or `(7,4)`. + +*Proof.* Each call writes exactly one coordinate. In the final word of +Section 3, the writes to target coordinates number at least 6 by Corollary 3. +The writes to spectators number at least `2s`. So `L >= L' >= 6 + 2s`. + +If `L <= 9`, then `s <= 1`, so the final word lives at dimension 3 or 4 and has +length at most 9. James Reed's #5005 (n = 3) and #5379 (n = 4) exclude every +length up to 11 there. If `L <= 11`, then `s <= 2`. The cases `s <= 1` are +excluded in the same way, so `s = 2`, dimension 5 and `L' in {10, 11}`. The +three listed write profiles are the solutions of `w_T + w_S = L'`, +`w_T >= 6` and `w_S >= 4`. QED + +**Remark (one cross call each way).** In the residual case some call writes a +target coordinate while reading a spectator, and some call writes a spectator +while reading a target coordinate. If no call of the first kind existed, the +span of the spectator basis vectors would be invariant. The quotient by it +would delete all `w_S >= 4` spectator writes and leave a word of length at most +7 at `n = 3`, contradicting #5005. The second kind follows by transposition. + +Upper bound: the 12-call word of #5005, which never touches a spectator, +realizes `T` for every `n >= 3`. Hence `10 <= cost <= 12` for every `n >= 5`. +Exact cost 12 for every `n` is equivalent to excluding the residual +five-coordinate case. + +## 5. What the checks cover + +`verify.py` checks the ingredients on concrete words: the involution property +of all 120 paid calls at `n = 5`, `R = 2`; `rank(I+N) = R-1` for every rank-one +idempotent at `R = 2, 3`; the identity of Lemma 1 on 150 random words at +`n = 5`; the restriction and quotient homomorphisms of Lemma 4 on 60 random +words each; the transpose anti-automorphism on 60 random words; an exhaustive +instance of Lemma 1's rank consequence on all 368,136 reduced words of length +at most 3 at `n = 4`, `R = 2` (629,928 single-write cases); the 12-call word at +`n = 5`; and the counting step. Two controls reject a corrupted projection +formula. Random words are checks of the written lemmas, not a proof of them. + +## 6. Limits + +* The residual `n = 5`, length 10 and 11 case is not searched. Exact cost 12 + for `n >= 5` therefore remains open. +* Only `R = 2` is concluded. Lemma 1 and the rank argument work for any `R`, + including dirty registers, but no `R = 3` base case beyond #5292 is known. +* This is a formal-model statement. It supplies no native operation, tariff, + supplier or κ change. diff --git a/research/two-three-cycles-every-dimension/README.md b/research/two-three-cycles-every-dimension/README.md new file mode 100644 index 0000000000..7e3ebad0cf --- /dev/null +++ b/research/two-three-cycles-every-dimension/README.md @@ -0,0 +1,104 @@ +# Two 3-cycles need at least ten calls in every address dimension + +**Written proof with finite corroboration in a formal model. No new κ.** +The selected conditional exponent stays 62009/20000000. + +## Result + +In the formal model `M_2(F2[GL_n(F2)])` of #4939/#4950/#4968, a paid call is +`I + ([g]+[e])N` with `g` a coordinate CNOT and `N` a rank-one binary +idempotent. Free scalar maps are allowed and equality is formal. Let `c` be a +coordinate 3-cycle and let every other address coordinate be a spectator that +the target restores. + +For **every** `n >= 3`, `diag([c],[c])` has no word of length at most 9. A word +of length 10 or 11 at any `n` would give one at `n = 5` with a narrow profile: + +* both spectators written at least twice and read at least twice; +* each target coordinate written and read at least twice; +* (target, spectator) write counts `(6,4)`, `(6,5)` or `(7,4)`; +* at least one call writing a target coordinate from a spectator, and one + writing a spectator from a target coordinate. + +Hence `10 <= cost <= 12` for every `n >= 5`. Before this note, the known lower +bound for `n >= 5` was the single-cycle cost 6 of `research/three-cycle-address-floor`. +Exact cost 12 in every dimension is now equivalent to excluding that one +five-coordinate case. + +## Why it works + +A coordinate written by exactly one call cannot be restored. Project the word +product onto the group elements that leave that row unchanged. The projection +equals `A (I+N) B`, where `A` and `B` are the products before and after the +call. After augmentation, `I+N` has rank one, while the target is invertible. +The same projection forces each target coordinate to be written at least +twice. Transposition turns writes into reads. Spectators that are never written, +or never read, are removed by an exact restriction or quotient homomorphism. +Counting writes then bounds the number of live spectators by two. +[PROOF.md](PROOF.md) gives the complete argument. + +## Evidence + +[verify.py](verify.py) uses only the standard library and checks the lemmas on +concrete words: + +| Check | Coverage | +|---|---| +| Paid calls are involutions | all 120 calls at `n = 5`, `R = 2` | +| `rank(I+N) = R-1` | all 6 idempotents at `R = 2`, all 28 at `R = 3` | +| Single-write projection identity | 150 random words at `n = 5` | +| Restriction and quotient homomorphisms | 60 random words each | +| Transpose anti-automorphism | 60 random words | +| Single-write rank consequence | all 368,136 reduced words of length ≤ 3 at `n = 4` (629,928 cases) | +| Upper bound | the 12-call word at `n = 5`, spectators untouched | +| Counting step | residual profiles `(10,6,4)`, `(11,6,5)`, `(11,7,4)` | +| Controls | a dropped `I+N` factor is rejected | + +The random checks test the written lemmas; they do not replace the proof. The +`n = 3` and `n = 4` exclusions are cited premises, not re-run. + +## Reproduce + +From the repository root, CPython 3.12, standard library only: + +```sh +python3.12 -I -W error -B research/two-three-cycles-every-dimension/verify.py +python3.12 -I -O -W error -B research/two-three-cycles-every-dimension/verify.py +python3.12 -B scripts/research_package.py --package research/two-three-cycles-every-dimension +``` + +Each run prints `PASS_TWO_THREE_CYCLES_EVERY_DIMENSION` in about five seconds. + +## Scope + +Card `bit-new-register-model`, scope **changed** (see [TASK.json](TASK.json)). +This answers the reduction part of Open next question 1 of James Reed's +[#5379](https://github.com/CrocSwap/integer-mult-bounds/pull/5379) +(`research/spectator-three-cycle-additivity`): every `n` now reduces to `n = 5`, +and lengths up to 9 are excluded everywhere. It does not search `n = 5`, does +not treat a dirty third register, and supplies no native operation, tariff or +κ change. + +## Open next questions + +1. **Exclude lengths 10 and 11 at `n = 5`.** This would make the cost 12 in + every dimension. First restrict a meet-in-the-middle search to the three + write profiles above. Each spectator must be both written and read twice, + which removes most of the 120-letter alphabet at each position. The blocker + is the size of the unrestricted ball. +2. **Dirty third register with spectators.** Lemma 1 and the rank argument hold + for any register count, so the same reduction applies to + `diag([c],[c],[e])`. It needs base cases at `R = 3` beyond the `n = 3` bound + of #5292, whose length-11 case is still open. +3. **Sharper write counts.** A two-write analogue of Lemma 1, controlling when + two writes to one row cancel, might show that each live spectator costs three + calls. That would remove the residual case without search. + +## Credit + +The formal model is Mihir Srivastava's #4939. The `n = 3` and `n = 4` exact +costs, and the question, are James Reed / jwr404's #5005 and #5379. The +single-cycle all-dimension reduction of `research/three-cycle-address-floor` +(JoyboyBrian, #4974) suggested the restriction step. Those results are cited, +not re-run or audited. The whole-word projection lemma, the read/write +counting and this reduction were produced by Nick Petalas. diff --git a/research/two-three-cycles-every-dimension/SOURCES.json b/research/two-three-cycles-every-dimension/SOURCES.json new file mode 100644 index 0000000000..79c877bef7 --- /dev/null +++ b/research/two-three-cycles-every-dimension/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/spectator-three-cycle-additivity/README.md", + "usage": "provenance", + "git_blob": "7365c5defa67d16fcb9a12fe4190a290e99c035f", + "sha256": "bf4a2c95f5b6a6f0584aa8a6b4461fc9ad62ec04ca6848abf499d68a4940dd44" + }, + { + "path": "research/two-three-cycle-additivity/README.md", + "usage": "provenance", + "git_blob": "6bbd51f92adebdf1e5ca8141251cc35f5990af7c", + "sha256": "b292e40966b928f26b407ae5c59b4ed9b8d4687d28076efbc759a8afdf62cdfb" + }, + { + "path": "research/three-cycle-address-floor/README.md", + "usage": "provenance", + "git_blob": "6a65c91f29e5b226cebd32d0c1d6963a60a98761", + "sha256": "a63c4ea4c874cac1fb064e1aff07f8ef791391eb795aec22a2154eb44a8fa81e" + } + ] +} diff --git a/research/two-three-cycles-every-dimension/TASK.json b/research/two-three-cycles-every-dimension/TASK.json new file mode 100644 index 0000000000..074a0afe88 --- /dev/null +++ b/research/two-three-cycles-every-dimension/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove, for every address dimension n >= 3, that diag([c],[c]) for a coordinate 3-cycle c in M_2(F2[GL_n(F2)]) has no word of length at most 9, and reduce lengths 10 and 11 in every dimension to one five-coordinate case with explicit write/read profiles (Open next question 1 of PR #5379, research/spectator-three-cycle-additivity).", + "scope_change_reason": "PR #5005 (n = 3) and PR #5379 (n = 4) settle the smallest cases by search; #5379 asks for every n >= 4 and names the missing written two-target argument as the blocker. A whole-word projection lemma supplies that argument for all but one residual case.", + "bottleneck_link": "In this formal register model, extra address spectators cannot bring two 3-cycles below ten calls in any dimension; any further saving needs the residual five-coordinate word or a changed operation/tariff. No native implementation or kappa change follows.", + "budget_minutes": 60, + "stop_rule": "Stop at the written all-dimension reduction with lemma checks. Do not search the residual n = 5 case in this package.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/two-three-cycles-every-dimension", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Do lengths 10 and 11 fail at n = 5 under the residual write profiles (6,4), (6,5), (7,4)?", + "why_it_matters": "Excluding them gives exact cost 12 for two 3-cycles in every address dimension.", + "first_step": "Restrict a meet-in-the-middle search to words whose two spectators are each written and read at least twice.", + "blocked_by": "The unrestricted n = 5 ball over 120 paid letters is large; the profile restriction has not been implemented." + }, + { + "question": "Does the same reduction close a dirty third register with spectators, diag([c],[c],[e])?", + "why_it_matters": "Lemma 1 holds for any register count; combining it with R = 3 base cases would extend #5292 to every n.", + "first_step": "Recompute the write-count bound with the R = 3 rank condition.", + "blocked_by": "The R = 3, n = 3 length-11 case (#5292) is open and no R = 3 spectator base case exists." + }, + { + "question": "Does a two-write analogue of Lemma 1 force three writes per live spectator?", + "why_it_matters": "It would remove the residual case without search.", + "first_step": "Classify when two writes to one row return it to the unit row inside the projected support.", + "blocked_by": "Two writes can cancel on the row, so the single-write projection no longer isolates one factor." + } + ] +} diff --git a/research/two-three-cycles-every-dimension/VERIFY.json b/research/two-three-cycles-every-dimension/VERIFY.json new file mode 100644 index 0000000000..d9c0ccb91e --- /dev/null +++ b/research/two-three-cycles-every-dimension/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Involution of all 120 paid calls at n=5, R=2; rank(I+N)=R-1 at R=2,3; single-write projection identity on 150 random n=5 words; restriction, quotient and transpose maps on 60 random words each; exhaustive single-write rank consequence on all 368,136 reduced n=4 words of length <= 3; 12-call upper word; counting step and residual profiles; corrupted-projection control." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks with assertions disabled; verification uses explicit failures, not assert." + } + ] +} diff --git a/research/two-three-cycles-every-dimension/verify.py b/research/two-three-cycles-every-dimension/verify.py new file mode 100644 index 0000000000..e314cd0323 --- /dev/null +++ b/research/two-three-cycles-every-dimension/verify.py @@ -0,0 +1,324 @@ +"""Finite corroboration for the all-dimension two-3-cycle reduction. + +Model: M_R(F2[GL_n(F2)]). A group element is a tuple of row bitmasks, so the +coordinate CNOT with row i gaining bit j is x_i <- x_i + x_j ("writes i, +reads j"). An algebra element is a frozenset of group elements (F2 +coefficients). A paid call is D(g, N) = I + ([g] + [e]) N with N a rank-one +binary idempotent. The written proof is PROOF.md; these checks exercise its +lemmas on concrete words. They do not search for length-10 or length-11 words. +""" + +from __future__ import annotations + +import itertools +import json +import random +import sys + +MARK = "PASS_TWO_THREE_CYCLES_EVERY_DIMENSION" + + +def need(cond, msg): + if not cond: + raise SystemExit("FAIL: " + msg) + + +def gmul(a, b, n): + out = [] + for i in range(n): + acc = 0 + for k in range(n): + if a[i] >> k & 1: + acc ^= b[k] + out.append(acc) + return tuple(out) + + +def ident(n): + return tuple(1 << i for i in range(n)) + + +def cnot(n, i, j): + g = list(ident(n)) + g[i] ^= 1 << j + return tuple(g) + + +def gtranspose(g, n): + return tuple(sum(((g[r] >> c) & 1) << r for r in range(n)) for c in range(n)) + + +def amul(x, y, n): + acc = set() + for g in x: + for h in y: + acc ^= {gmul(g, h, n)} + return frozenset(acc) + + +def mmul(X, Y, n): + R = len(X) + out = [] + for i in range(R): + row = [] + for j in range(R): + acc = set() + for k in range(R): + acc ^= amul(X[i][k], Y[k][j], n) + row.append(frozenset(acc)) + out.append(tuple(row)) + return tuple(out) + + +def scalar(M, n): + e = frozenset({ident(n)}) + return tuple(tuple(e if M[i][j] else frozenset() for j in range(len(M))) for i in range(len(M))) + + +def idempotents(R): + out = [] + for u in range(1, 1 << R): + for v in range(1, 1 << R): + if bin(u & v).count("1") % 2 == 1: + out.append(tuple(tuple((u >> i & 1) & (v >> j & 1) for j in range(R)) for i in range(R))) + return out + + +def call(g, N, n): + """I + ([g] + [e]) N.""" + R = len(N) + e = ident(n) + x = frozenset({g}) ^ frozenset({e}) if g != e else frozenset() + rows = [] + for i in range(R): + row = [] + for j in range(R): + v = frozenset({e}) if i == j else frozenset() + if N[i][j]: + v = v ^ x + row.append(v) + rows.append(tuple(row)) + return tuple(rows) + + +def product(word, n, R): + P = scalar(tuple(tuple(int(i == j) for j in range(R)) for i in range(R)), n) + for g, N in word: + P = mmul(P, call(g, N, n), n) + return P + + +def mmap(P, f): + return tuple(tuple(frozenset(f(x)) for x in row) for row in P) + + +def proj_row_stab(P, k, n): + want = 1 << k + return mmap(P, lambda x: {g for g in x if g[k] == want}) + + +def augment(P): + return tuple(tuple(len(x) % 2 for x in row) for row in P) + + +def f2rank(M): + rows = [sum(b << j for j, b in enumerate(r)) for r in M] + rank = 0 + for bit in range(len(M[0]) if M else 0): + piv = next((i for i in range(rank, len(rows)) if rows[i] >> bit & 1), None) + if piv is None: + continue + rows[rank], rows[piv] = rows[piv], rows[rank] + for i in range(len(rows)): + if i != rank and rows[i] >> bit & 1: + rows[i] ^= rows[rank] + rank += 1 + return rank + + +def delete_coord(g, k, n): + keep = [r for r in range(n) if r != k] + out = [] + for r in keep: + m = 0 + for pos, c in enumerate(keep): + if g[r] >> c & 1: + m |= 1 << pos + out.append(m) + return tuple(out) + + +def writes(g, n): + e = ident(n) + return next(i for i in range(n) if g[i] != e[i]) + + +def reads(g, n): + e = ident(n) + i = writes(g, n) + return next(j for j in range(n) if (g[i] ^ e[i]) >> j & 1) + + +def three_cycle(n): + # rows 0,1,2 of c are rows 1,2,0 of the identity; all other rows fixed + e = ident(n) + return tuple([e[1], e[2], e[0]] + list(e[3:])) + + +def three_cycle_inverse(n): + e = ident(n) + return tuple([e[2], e[0], e[1]] + list(e[3:])) + + +def main(): + rng = random.Random(20261027) + stats = {} + + # A. every paid call is an involution (n=5, R=2: 20 CNOTs x 6 idempotents) + n, R = 5, 2 + Ns = idempotents(R) + need(len(Ns) == 6, "six rank-one idempotents in M_2(F2)") + gens = [cnot(n, i, j) for i in range(n) for j in range(n) if i != j] + I2 = scalar(((1, 0), (0, 1)), n) + for g in gens: + for N in Ns: + D = call(g, N, n) + need(mmul(D, D, n) == I2, "paid call is an involution") + stats["involution_calls"] = len(gens) * len(Ns) + + # B. I + N has F2-rank R-1 for every rank-one idempotent, R = 2 and 3 + for RR in (2, 3): + for N in idempotents(RR): + M = tuple(tuple((int(i == j) + N[i][j]) % 2 for j in range(RR)) for i in range(RR)) + need(f2rank(M) == RR - 1, "rank(I+N) = R-1") + stats["idempotents_checked"] = {"R2": 6, "R3": len(idempotents(3))} + + # C. projection identity pi_k(P) = A (I+N_t) B when k is written once + trials = 0 + for _ in range(150): + k = rng.randrange(n) + L = rng.randrange(2, 8) + t = rng.randrange(L) + others = [g for g in gens if writes(g, n) != k] + once = [g for g in gens if writes(g, n) == k] + word = [(rng.choice(others), rng.choice(Ns)) for _ in range(L)] + word[t] = (rng.choice(once), rng.choice(Ns)) + P = product(word, n, R) + A = product(word[:t], n, R) + B = product(word[t + 1:], n, R) + Nt = word[t][1] + IN = scalar(tuple(tuple((int(i == j) + Nt[i][j]) % 2 for j in range(R)) for i in range(R)), n) + need(proj_row_stab(P, k, n) == mmul(mmul(A, IN, n), B, n), "projection identity") + rest = mmul(mmul(A, mmap(scalar(Nt, n), lambda x: {word[t][0]} if x else set()), n), B, n) + need(all(g[k] != 1 << k for row in rest for x in row for g in x), "written-once term leaves the stabilizer") + need(f2rank(augment(proj_row_stab(P, k, n))) == R - 1, "projected augmentation has rank R-1") + trials += 1 + stats["projection_trials"] = trials + + # D/E. restriction (k never written) and quotient (k never read) are homomorphisms + for mode in ("restrict", "quotient"): + for _ in range(60): + k = rng.randrange(3, n) + if mode == "restrict": + pool = [g for g in gens if writes(g, n) != k] + else: + pool = [g for g in gens if reads(g, n) != k] + word = [(rng.choice(pool), rng.choice(Ns)) for _ in range(rng.randrange(1, 7))] + P = product(word, n, R) + lhs = mmap(P, lambda x: _reduce_set(x, k, n)) + short = [(delete_coord(g, k, n), N) for g, N in word] + short = [(g, N) for g, N in short if g != ident(n - 1)] + need(lhs == product(short, n - 1, R), mode + " homomorphism") + stats[mode + "_trials"] = 60 + + # F. transpose anti-automorphism reverses words and keeps calls legal + for _ in range(60): + word = [(rng.choice(gens), rng.choice(Ns)) for _ in range(rng.randrange(1, 7))] + P = product(word, n, R) + tP = tuple(tuple(frozenset(gtranspose(g, n) for g in P[j][i]) for j in range(R)) for i in range(R)) + tw = [(gtranspose(g, n), tuple(tuple(N[j][i] for j in range(R)) for i in range(R))) for g, N in reversed(word)] + need(all(writes(a, n) == reads(b, n) for (a, _), (b, _) in zip(tw, reversed(word))), "transpose swaps write and read") + need(tP == product(tw, n, R), "transpose anti-automorphism") + stats["transpose_trials"] = 60 + + # G. exhaustive single-write lemma instance: n=4, R=2, all words of length <= 3 + n4 = 4 + gens4 = [cnot(n4, i, j) for i in range(n4) for j in range(n4) if i != j] + letters = [(g, N) for g in gens4 for N in Ns] + calls4 = {(g, N): call(g, N, n4) for g, N in letters} + I24 = scalar(((1, 0), (0, 1)), n4) + checked = 0 + stack = [((), I24)] + while stack: + word, P = stack.pop() + if word: + counts = [0] * n4 + for g, _ in word: + counts[writes(g, n4)] += 1 + for k in range(n4): + if counts[k] == 1: + proj = proj_row_stab(P, k, n4) + need(f2rank(augment(proj)) == 1, "single-write projection has augmentation rank 1") + checked += 1 + if len(word) < 3: + for lt in letters: + if word and word[-1] == lt: + continue + stack.append((word + (lt,), mmul(P, calls4[lt], n4))) + stats["exhaustive_single_write_cases_n4_len_le3"] = checked + + # H. the 12-call upper bound in every dimension (shown at n=5): spectators untouched + c = three_cycle(n) + swap01 = [cnot(n, 0, 1), cnot(n, 1, 0), cnot(n, 0, 1)] + swap12 = [cnot(n, 1, 2), cnot(n, 2, 1), cnot(n, 1, 2)] + seq = swap01 + swap12 + acc = ident(n) + for g in seq: + acc = gmul(acc, g, n) + need(acc in (c, three_cycle_inverse(n)), "two swaps give a coordinate 3-cycle") + c = acc + E00 = ((1, 0), (0, 0)) + E11 = ((0, 0), (0, 1)) + word12 = [(g, E00) for g in seq] + [(g, E11) for g in seq] + T = product(word12, n, R) + need(T == ((frozenset({c}), frozenset()), (frozenset(), frozenset({c}))), "12-call word realizes diag([c],[c])") + need(all(writes(g, n) < 3 and reads(g, n) < 3 for g, _ in word12), "upper word never touches spectators") + stats["upper_bound_calls"] = len(word12) + + # I. counting: L' = W_T + W_S with W_T >= 6, W_S >= 2s; W_T = a+b, R_T = a+c, etc. + profiles = [] + for L in range(0, 12): + for s in range(0, 6): + for wt in range(6, L + 1): + ws = L - wt + if ws >= 2 * s and (s > 0 or ws == 0): + profiles.append((L, s, wt, ws)) + need(all(s <= 2 for _, s, _, _ in profiles), "length <= 11 forces at most two live spectators") + need(all(s <= 1 for L, s, _, _ in profiles if L <= 9), "length <= 9 forces at most one live spectator") + residual = sorted({(L, wt, ws) for L, s, wt, ws in profiles if s == 2}) + need(residual == [(10, 6, 4), (11, 6, 5), (11, 7, 4)], "residual write profiles") + stats["residual_s2_write_profiles"] = [list(r) for r in residual] + + # J. controls: the identity fails when a corrupted factor is used + k = 0 + word = [(cnot(n, 1, 2), Ns[0]), (cnot(n, 0, 3), Ns[1]), (cnot(n, 2, 4), Ns[2])] + P = product(word, n, R) + A = product(word[:1], n, R) + B = product(word[2:], n, R) + bad = mmul(A, B, n) + need(proj_row_stab(P, k, n) != bad, "control: dropping I+N_t is detected") + need(f2rank(((1, 0), (0, 1))) == 2, "control: identity has full rank, unlike I+N") + stats["controls"] = 2 + + print(MARK, json.dumps(stats, sort_keys=True)) + + +def _reduce_set(x, k, n): + out = set() + for g in x: + out ^= {delete_coord(g, k, n)} + return out + + +if __name__ == "__main__": + sys.exit(main())