Prove two 3-cycles need ten calls in every address dimension (no new κ)

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 / <e_k>` 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 `<e_k>`
+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.

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}