Prove a single three-cycle costs six with arbitrary address spectators

research/three-cycle-address-floor/PROOF.md

@@ -0,0 +1,143 @@
+# One coordinate three-cycle costs six calls in every finite workspace
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+This is a computer-assisted theorem with a written uniform reduction and an
+explicit finite exclusion. It is not proof-kernel verification.
+
+## Statement
+
+Let n≥3 and R≥1 be finite. In M_R(F2[GL_n(F2)]), a paid call has the form
+
+    D(g,N)=I+([g]+[e])N,   g=I_n+E_ij, i≠j,
+    N=u v^T, v^T u=1.
+
+Free scalar GL_R(F2) matrices may appear anywhere. There are no free address
+maps. Equality is coefficientwise in the full group algebra for arbitrary
+inputs. Let c cyclically permute three address coordinates and fix the others.
+Then diag([c],[e],...,[e]) costs exactly six paid calls. Every additional
+register is arbitrary dirty input and is individually restored. The result is
+uniform in both address spectators and register workspace.
+
+The lower bound also applies to any full formal endpoint having a nonzero
+coefficient of [c] in any matrix entry. This does not make costs additive for
+several target entries. The upper bound here concerns the stated single target.
+
+## 1. Formal support survives arbitrary scalar mixing
+
+For a matrix M over the group algebra, write supp(M) for the group elements
+with a nonzero binary coefficient matrix. Scalar matrices have support contained
+in {e}. A paid factor is
+
+    D(g,N)=[e](I+N)+[g]N.
+
+Expand a word containing m paid calls, keeping all intervening scalar matrices.
+Every term chooses either e or g_i at each paid position. Its group element is
+therefore a subword of the paid address-label sequence, in the same written
+multiplication order. Its coefficient is the corresponding ordered product of
+binary matrices, including the free maps. Cancellation can remove group
+elements; it cannot introduce an element absent from every expanded term.
+Thus if [c] has a nonzero coefficient, some paid-label subword of length at
+most m multiplies to c. Reversing written order gives its chronological CNOT
+execution; CNOT labels are involutions but no commutation is assumed.
+
+This argument does not use a nonfaithful natural representation. It uses the
+basis of the full group algebra. It does not require an augmentation
+normalization or any bound on R. Rank-one idempotence is part of the paid model
+but is not needed for this support implication.
+
+It remains to exclude an ordinary address CNOT word for c with at most five
+calls, uniformly in n. Such a word is an invertible n×n binary matrix word.
+
+## 2. A short address word writes at most one spectator
+
+Use chronological row operations starting at I_n: (i,j) replaces row i by
+row i plus row j. Every intermediate matrix is invertible.
+
+Each of the three cycled rows must be written at least once, since its final
+row differs from its original unit row. If a spectator row is written exactly
+once, before that write it is its original unit row e_i. Its sole write adds a
+nonzero donor row: invertibility implies every row is nonzero. It is never
+written again, so its final row cannot equal e_i, contradicting restoration.
+Consequently every written spectator receives at least two writes.
+
+At a total budget of five, the three active rows use at least three writes,
+leaving at most two. Hence at most one spectator is ever written. Let S contain
+the three cycled coordinates and every written spectator. Then |S|≤4.
+
+## 3. Deleting never-written donors is a valid restriction
+
+Let U be the complementary set of never-written coordinates. Every generator
+of the short word writes a row in S; it may read a donor in S or U. The
+coordinate subspace V_S={x:x_U=0} is invariant under every generator: no U
+coordinate is written. Restriction to V_S sends a CNOT with donor in S to the
+same coordinate CNOT on S, and a CNOT with donor in U to the identity. Deleting
+the latter calls gives a word of no greater length on |S| coordinates.
+
+Restriction respects the entire ordered product because V_S is invariant at
+every step. Equivalently these generators lie in the block-upper-triangular
+subgroup with lower blocks (0,I_U), and taking the S×S block is a homomorphism
+on that subgroup. No projection from arbitrary GL_n matrices is asserted.
+The final c restricts to the same three-cycle, fixing the possible fourth role.
+
+Setting x_U=0 here is a mathematical restriction of an identity required on
+all inputs. It does not authorize clean ancillas in the original paid model.
+The surviving fourth coordinate remains arbitrary and must be restored.
+
+Relabel the three active coordinates 0,1,2 and the possible spectator 3. If
+|S|=3, pad with an untouched fourth coordinate. It is enough to exclude
+
+    C=(e_1,e_2,e_0,e_3)
+
+as a product of at most five among all 12 row CNOTs on four coordinates.
+The inverse cycle has the same minimum by reversing a word.
+
+## 4. Complete four-coordinate exclusion
+
+The package recomputes, without pruning or symmetry reduction, the full balls
+B_2 and B_3 around I_4 for the 12 CNOT generators. Exact distance layers are
+
+    1, 12, 96, 542;   |B_2|=109, |B_3|=651.
+
+Every word of length at most five splits into factors X and Y with X∈B_3 and
+Y∈B_2. Therefore C would require X^(-1)C∈B_2 for some X∈B_3. The primary
+checker tests all 651 possibilities and finds zero. It also reconstructs and
+checks every stored word, so the list is tied to the actual generators.
+
+A separate implementation uses the literal action on all 16 Boolean address
+vectors, rather than row-bitset matrices or primary multiplication/inversion.
+It independently forms its radius-two ball, the target radius-two ball, and
+all 12 outgoing edges at each of 109 radius-two states. No middle edge reaches
+the target ball; the two radius-two balls do not intersect either. This covers
+all five-or-fewer words, including lengths below five. Its independently formed
+radius-three ball agrees with the primary ball after exact conversion.
+
+The finite exclusion is a premise supplied by these complete executable
+checks, not by stored counts alone. Sections 1–3 show why it suffices for all
+n and R. The proof does not inherit PR4968's n=3,R=2 search or its all-pairs
+census, and no large finite search is run.
+
+## 5. Six-call upper bound
+
+Chronologically execute
+
+    (0,1),(1,0),(0,1), (1,2),(2,1),(1,2).
+
+The first three calls swap coordinates 0 and 1, the last three swap 1 and 2.
+The endpoint is C as displayed. On target register 0 use N=E_00 for each paid
+factor. The formal product is diag([c],[e],...,[e]); every other register and
+address spectator is fixed. This proves attainment for every n≥3,R≥1.
+
+The checker expands the group-algebra word and also tests dense scalar
+conjugates and inverse cycles. Omitting a call, using an incorrect label,
+accepting only a natural image, or dropping restoration are separate controls.
+
+## 6. Scope and remaining question
+
+The result closes the single-three-cycle all-dimension boundary in PR4968.
+Support gives only the largest individual target word-length floor, not a sum
+across target registers. Multiple three-cycles, mixed cycle/permutation targets,
+and the optimum of the regular-representation cut relaxation remain open here.
+Different paid labels, free address maps, unreturned address spectators and
+clean-only endpoint contracts are outside the statement. This is a formal cost
+screen; native realization, physical tariffs, compiler/stock/precision and a
+new multiplication exponent are not supplied.

research/three-cycle-address-floor/README.md

@@ -0,0 +1,133 @@
+# A single coordinate three-cycle costs six in every finite workspace
+
+**Computer-assisted formal-model theorem; no new κ.** In
+`M_R(F2[GL_n(F2)])`, one coordinate three-cycle on one target register costs
+exactly **six coordinate-CNOT calls**, for every finite `n≥3` and `R≥1`.
+Every other address coordinate and arbitrary dirty register is restored.
+Free scalar `GL_R(F2)` mixing is allowed; free address maps are not.
+
+This closes the single-cycle all-dimension boundary left by James Reed's
+[PR4968](https://github.com/CrocSwap/integer-mult-bounds/pull/4968), exact live
+head `99a0f53c640bfa97c84f83b6e4644602e41d2dfd`. Its three-cycle calculation
+covers `n=3,R≤2`. Its separate mixed-transposition theorem and all-pairs census,
+and [PR4950](https://github.com/CrocSwap/integer-mult-bounds/pull/4950)'s `3t`
+identical-swap theorem, are credited context and are not replayed here.
+
+## Uniform reduction and finite premise
+
+Each paid factor is `I+([I_n+E_ij]+[e])uv^T`, with `i≠j` and `v^Tu=1`.
+The endpoint is `diag([c],[e],...,[e])` for a three-cycle c, with full formal
+coefficient equality. [PROOF.md](PROOF.md) establishes:
+
+1. Expanding the word with all free scalar maps shows that every group element
+   in its support is a subword of its paid address labels. A nonzero `[c]`
+   coefficient therefore gives an address CNOT word for c of no greater length.
+2. Three changed address rows each need a write. A written spectator that
+   finishes restored needs at least two writes: with only one, its nonzero
+   donor row could not leave its original unit row unchanged.
+3. At most five calls can write at most one spectator. All other address rows
+   are never written. Restriction to their zero-coordinate invariant subspace
+   deletes their donor calls and leaves the same endpoint on at most four
+   coordinates. This is a subgroup restriction, not a projection of general GL_n.
+4. A complete four-coordinate calculation excludes every word of length at
+   most five. Two swaps attain the three-cycle in six.
+
+The first three statements are written quantified arguments. The last exclusion
+is the explicit finite premise independently recomputed by both implementations.
+The checks do not themselves formalize the unbounded-dimensional proof.
+Setting discarded coordinates to zero in the proof is a restriction of an
+identity required on **all** inputs; it does not supply clean ancillas.
+
+## Exact evidence
+
+| Check | Complete coverage |
+|---|---:|
+| Address alphabet | All 12 coordinate CNOTs on four coordinates |
+| Exact distance layers 0,1,2,3 | 1, 12, 96, 542 |
+| Radius-two / radius-three balls | 109 / 651 |
+| Primary `B3` versus target-translate of `B2` | 651 joins, zero hits |
+| Separate truth-table middle-edge check | 1,308 bridges, zero hits |
+| Truth-table conversion | All 16 inputs of each of 651 states: 10,416 checks |
+| Optimized CLI corruption controls | Six rejected source/receipt mutations |
+
+`verify.py` uses row-bitset matrices, Gaussian inversion and explicit split
+products. `independent.py` imports no primary code: it uses permutations of
+all 16 Boolean address inputs and a middle-edge intersection. Their entire
+radius-three state sets agree after conversion, not just their counts. Both
+have positive short-target reachability controls. No pruning, symmetry
+quotient, heuristic solver or stored frontier is used.
+
+The primary also verifies the six-call word coefficientwise in the full group
+algebra at `(n,R)=(3,1),(4,3),(8,5)`, including dense scalar conjugations with
+free frame restoration. It checks inverse-cycle orientation, arbitrary scalar
+mixing against subword support, every omitted upper-bound call, an incorrect
+label, an unreturned spectator and illegal gates. A six-term nonzero formal
+element with zero natural image demonstrates why natural equality is not
+accepted as a formal certificate. These finite controls corroborate the proof
+and upper construction; they are not a finite-only extrapolation to all n,R.
+
+## Reproduce
+
+Python 3.12, standard library only. From the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/three-cycle-address-floor
+python3.12 -I -O -B research/three-cycle-address-floor/verify.py
+python3.12 -I -O -B research/three-cycle-address-floor/independent.py
+python3.12 -I -O -B research/three-cycle-address-floor/test_controls.py
+```
+
+The core replay takes well under a second locally. `RESULT.json` is a compact
+receipt compared only after full recomputation. The package has no live external
+runtime input; provenance pins are separate. All scripts are read-only by
+default and run directly from a Git-free export. The selected-baseline binding
+check passed; it is not a selected-construction cold replay.
+
+## Scope and family decision
+
+This result covers **one** three-cycle target. The support argument supplies
+the largest individual target word-length floor; it does not add those floors
+across registers. In particular no `6t` multi-cycle tariff, general mixed-target
+additivity, or optimum for regular-representation cuts is claimed. The finite
+exclusion concerns ordinary address matrices only after the full formal support
+reduction; natural-image acceptance is not used.
+
+Stop after this uniform single-cycle screen. There is no native realization,
+paid scalar/physical frame bill, compiler/stock/precision admission, supplier,
+new multiplication theorem or new κ. The selected conditional value remains
+`60403/20000000`. No predecessor census, C++, Lean, Docker or hosted-CI replay
+is claimed. Both implementations are same-session Codex-assisted work, not
+independent human or formal-kernel verification. A separate coordinating Codex
+review read the complete uniform reduction and both exact engines, finding no
+mathematical or coverage blocker.
+
+## Open next questions
+
+- Do multiple three-cycle targets admit sharing? Begin with two targets at
+  fixed address dimension and a genuinely new all-register invariant. The
+  support floor is only six and does not prove twelve; a larger repetition
+  of this single-target census would not resolve the problem.
+- What is the exact optimum of the all-permutation-cut relaxation in PR4968?
+  Its time-limited 3.51 scratch run is not an optimum certificate. Supply a
+  rigorous upper bound and a matching feasible cut certificate before claiming
+  the method's exact limit. This package does not run that LP.
+
+## Sources, overlap and credit
+
+Base `b91956876e5b4122fd89179f1b57557ff8378f15`, priority revision 7.
+[Canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19138311).
+Entry card and exact-term searches covered 317 open PRs, 4,064 Discussion records
+and all 6,636 local notes, with complete pagination/inventory. Live PR4968 and
+canonical #1317 were checked. Nearby cycle findings concern other alphabets or
+fixed dimensions. Cached snapshots, arbitrary diffs and unpublished work remain
+coverage limits; this is not a novelty guarantee.
+
+Credit James Reed #4968/#4950 for the immediate questions and cut results;
+Mihir Srivastava #4939 for the arbitrary-address spectator model, write budget
+and subgroup-projection lineage; commdata2338 #1414/#1495; Ross Richardson
+#1989; Gareth Davidson #1333; PR1541; and their retained predecessor credits.
+Their sources are unchanged. The new contribution combines formal subword
+support with a one-written-spectator reduction and a fresh four-coordinate
+exclusion to settle the single three-cycle for all finite n and R.
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0.

research/three-cycle-address-floor/RESULT.json

@@ -0,0 +1,60 @@
+{
+  "address_dimension_checked": 4,
+  "ball_three": 651,
+  "ball_three_sha256": "f5557230aac39f464eee192e8e68bc2e9a792c78035e3ae14802867712790104",
+  "ball_two": 109,
+  "controls": {
+    "fixtures": [
+      {
+        "R": 1,
+        "coefficient_terms": 1,
+        "dense_projector": [
+          1,
+          1
+        ],
+        "endpoint_sha256": "0f5af9ad37b28bb894fd9a6822bd0cc928d47a9b9b7c5387b6941a37138fa085",
+        "n": 3
+      },
+      {
+        "R": 3,
+        "coefficient_terms": 2,
+        "dense_projector": [
+          6,
+          5
+        ],
+        "endpoint_sha256": "962ce82483b6749e5ac8cc539e914d03550851b4c9668c469ae87831280104e1",
+        "n": 4
+      },
+      {
+        "R": 5,
+        "coefficient_terms": 2,
+        "dense_projector": [
+          30,
+          17
+        ],
+        "endpoint_sha256": "5f5ca2d0a93fa14847b8a6e4f26f031a447dda755058757340ffe8f3d4320e67",
+        "n": 8
+      }
+    ],
+    "natural_alias_terms": 6,
+    "omission_controls": 6,
+    "other_semantic_controls": 6,
+    "subword_elements": 16,
+    "support_terms": 15,
+    "support_word_calls": 4
+  },
+  "generators": 12,
+  "joins_through_five": 651,
+  "layers": [
+    1,
+    12,
+    96,
+    542
+  ],
+  "minimum": 6,
+  "short_target_positive_joins": 7,
+  "six_call_joins": 27,
+  "status": "PASS_THREE_CYCLE_ADDRESS_FLOOR",
+  "target_hits_through_five": 0,
+  "uniform_scope": "one coordinate three-cycle; all finite n>=3 and R>=1 by PROOF.md"
+}

research/three-cycle-address-floor/SOURCES.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/swap-row-order-cut/README.md",
+      "usage": "provenance",
+      "git_blob": "941c1eb4f2301023757c45bbe1bb767962065cd1",
+      "sha256": "a5e9661f5ffa504cafee1c9481f0a1072b98341f98a031a2b4d18bb8c4a9ef7c"
+    },
+    {
+      "path": "research/two-swap-address-spectators/README.md",
+      "usage": "provenance",
+      "git_blob": "a10600771f9f3bd04172087671c2360097d4f6d9",
+      "sha256": "8a390f05ab4f31c46de8e529a6fa31b1fa21819cbaf30855e77664585da68c75"
+    }
+  ],
+  "read_predecessor_context": {
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4968",
+    "head": "99a0f53c640bfa97c84f83b6e4644602e41d2dfd",
+    "path": "research/swap-component-cut/README.md",
+    "sha256": "70d4e1119a253c03f05442a42594363024b685e71a79e1a404fdd56674a8c7bb",
+    "usage": "bibliographic context only; not a proof premise or runtime input"
+  }
+}