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())