diff --git a/research/three-cycle-address-floor/PROOF.md b/research/three-cycle-address-floor/PROOF.md
new file mode 100644
index 0000000000..1061c6dabe
--- /dev/null
+++ b/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.
diff --git a/research/three-cycle-address-floor/README.md b/research/three-cycle-address-floor/README.md
new file mode 100644
index 0000000000..6a65c91f29
--- /dev/null
+++ b/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.
diff --git a/research/three-cycle-address-floor/RESULT.json b/research/three-cycle-address-floor/RESULT.json
new file mode 100644
index 0000000000..52d6b89849
--- /dev/null
+++ b/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"
+}
diff --git a/research/three-cycle-address-floor/SOURCES.json b/research/three-cycle-address-floor/SOURCES.json
new file mode 100644
index 0000000000..538df46ec5
--- /dev/null
+++ b/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"
+  }
+}
diff --git a/research/three-cycle-address-floor/TASK.json b/research/three-cycle-address-floor/TASK.json
new file mode 100644
index 0000000000..b549025dbd
--- /dev/null
+++ b/research/three-cycle-address-floor/TASK.json
@@ -0,0 +1,77 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15",
+  "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "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": "Exact six-call floor for one coordinate three-cycle in formal M_R(F2[GL_n(F2)]) for every finite n>=3 and R>=1, with all dirty spectators restored.",
+  "scope_change_reason": "PR4968 supplies a three-cycle minimum only at n=3,R<=2. The new formal-support and written-spectator reduction removes both bounds; it does not revisit its transposition theorem.",
+  "bottleneck_link": "This rules out paid savings for a single nonabelian permutation target even with arbitrary dirty/address workspace. It does not admit a native supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the full support/restriction proof, two complete small address exclusions, formal attainment and discriminating controls. No multi-target or LP search.",
+  "outcome": "completed",
+  "evidence": "Written all-n/all-R reduction; disjoint exact GL4 row and truth-table engines, 651 full states with zero five-call joins, full-formal upper witnesses and six optimized-CLI mutations.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation and verification. Separate implementations are not independent human or formal-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Can multiple three-cycle targets share paid calls?",
+      "why_it_matters": "A single-target support floor is only the maximum individual word length.",
+      "first_step": "Choose two target cycles and seek a new all-register invariant before running a search.",
+      "blocked_by": "No additive lower bound is proved here."
+    },
+    {
+      "question": "What is the exact all-permutation-cut optimum for the PR4968 three-cycle?",
+      "why_it_matters": "Its time-limited scratch run is not a rigorous method ceiling.",
+      "first_step": "Construct a rigorous upper certificate and matching feasible cut certificate.",
+      "blocked_by": "No LP certificate or all-cut separation proof is supplied here."
+    }
+  ],
+  "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19138311",
+  "predecessor_heads": {
+    "4968": "99a0f53c640bfa97c84f83b6e4644602e41d2dfd",
+    "4950": "78dc9c12f46967df0d85594875a32a62b5639670",
+    "4939": "743ddd6275cfd560d9c3e7825c42545152d14e4c"
+  },
+  "family_decision": "Scoped negative formal-model screen. Stop after the single-target theorem; multiple targets require a new additive invariant, and physical admission remains unknown."
+}
diff --git a/research/three-cycle-address-floor/VERIFY.json b/research/three-cycle-address-floor/VERIFY.json
new file mode 100644
index 0000000000..08e5fc4bf8
--- /dev/null
+++ b/research/three-cycle-address-floor/VERIFY.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Complete GL4 five-call exclusion and full group-algebra upper/support controls; PROOF.md supplies the uniform reduction."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Disjoint full-address truth-table exclusion, complete-ball agreement and positive joins."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_controls.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Six isolated optimized-CLI source and receipt corruptions must be rejected."
+    }
+  ]
+}
diff --git a/research/three-cycle-address-floor/independent.py b/research/three-cycle-address-floor/independent.py
new file mode 100644
index 0000000000..3a391e70da
--- /dev/null
+++ b/research/three-cycle-address-floor/independent.py
@@ -0,0 +1,58 @@
+#!/usr/bin/env python3
+"""Disjoint truth-table engine: complete 16-input address action, no primary import.
+JoyboyBrian, substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import hashlib
+import json
+from pathlib import Path
+HERE=Path(__file__).resolve().parent
+
+def require(ok,message):
+    if not ok:raise ValueError(message)
+
+GATES=[(i,j) for i in range(4) for j in range(4) if i!=j]
+IDENTITY=tuple(range(16))
+TARGET=tuple(((x>>1)&1)|(((x>>2)&1)<<1)|((x&1)<<2)|(x&8) for x in range(16))
+
+def step(table,gate):
+    target,donor=gate
+    return tuple(y ^ (((y>>donor)&1)<<target) for y in table)
+
+def grow(seed,depth):
+    seen={seed};front={seed};layers=[1]
+    for _ in range(depth):
+        new={step(t,g) for t in front for g in GATES}-seen
+        layers.append(len(new));seen|=new;front=new
+    return seen,layers
+
+def run():
+    left,layers=grow(IDENTITY,2);right,_=grow(TARGET,2)
+    require(not left&right,'target reachable within four')
+    bridge_hits=sum(step(t,g) in right for t in left for g in GATES)
+    require(bridge_hits==0,'target reachable within five')
+    third,layers3=grow(IDENTITY,3)
+    # Convert each whole truth table to rows; verify all 16 inputs, not only basis.
+    matrices=[]
+    for table in third:
+        rows=tuple(sum(((table[1<<j]>>i)&1)<<j for j in range(4)) for i in range(4))
+        for x in range(16):
+            image=sum(((row&x).bit_count()%2)<<i for i,row in enumerate(rows))
+            require(image==table[x],'linear truth-table conversion')
+        matrices.append(rows)
+    digest=hashlib.sha256(json.dumps(sorted(matrices),separators=(',',':')).encode()).hexdigest()
+    receipt=json.loads((HERE/'RESULT.json').read_text())
+    require(receipt['layers']==layers3 and receipt['ball_two']==len(left) and receipt['ball_three']==len(third),'independent ball inventory')
+    require(receipt['ball_three_sha256']==digest,'complete converted ball agreement')
+    require(receipt['target_hits_through_five']==bridge_hits and receipt['minimum']==6,'independent exclusion receipt')
+    word=[(0,1),(1,0),(0,1),(1,2),(2,1),(1,2)];table=IDENTITY
+    for gate in word:table=step(table,gate)
+    require(table==TARGET,'six-call full-address witness')
+    # Reachability positives exercise both overlap and middle-edge paths.
+    small=step(IDENTITY,(0,1));small_right,_=grow(small,2)
+    require(left&small_right,'short positive overlap')
+    five=IDENTITY
+    for gate in word[:5]:five=step(five,gate)
+    five_right,_=grow(five,2)
+    require(any(step(t,g) in five_right for t in left for g in GATES),'short positive bridge')
+    print('PASS_THREE_CYCLE_INDEPENDENT tables=651 full_input_checks=10416 bridges=1308 hits=0')
+if __name__=='__main__':run()
diff --git a/research/three-cycle-address-floor/test_controls.py b/research/three-cycle-address-floor/test_controls.py
new file mode 100644
index 0000000000..b0b3ca2934
--- /dev/null
+++ b/research/three-cycle-address-floor/test_controls.py
@@ -0,0 +1,40 @@
+#!/usr/bin/env python3
+"""Real isolated optimized-CLI corruptions; no new scientific search.
+JoyboyBrian, substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+HERE=Path(__file__).resolve().parent
+
+def need(ok,message):
+    if not ok:raise ValueError(message)
+
+def run():
+    cases=('missing_generator','wrong_target','wrong_upper_word','receipt_count','receipt_minimum','receipt_hash')
+    for case in cases:
+        with tempfile.TemporaryDirectory(prefix='three-cycle-control-') as directory:
+            copied=Path(directory)/'package';shutil.copytree(HERE,copied)
+            script='verify.py'
+            if case=='missing_generator':
+                p=copied/script;s=p.read_text();old='if i!=j]\n    words=';new='if i!=j and (i,j)!=(0,1)]\n    words='
+                need(s.count(old)==1,'exact alphabet mutation site');p.write_text(s.replace(old,new))
+            elif case=='wrong_target':
+                p=copied/script;s=p.read_text();old='target=(2,4,1,8)';need(s.count(old)==1,'exact target mutation site');p.write_text(s.replace(old,'target=identity(4)'))
+            elif case=='wrong_upper_word':
+                script='independent.py';p=copied/script;s=p.read_text();old='(1,2),(2,1),(1,2)];table=IDENTITY';new='(1,2),(2,1),(0,2)];table=IDENTITY'
+                need(s.count(old)==1,'exact witness mutation site');p.write_text(s.replace(old,new))
+            else:
+                p=copied/'RESULT.json';receipt=json.loads(p.read_text())
+                if case=='receipt_count':receipt['ball_three']+=1
+                elif case=='receipt_minimum':receipt['minimum']=5
+                else:receipt['ball_three_sha256']='0'*64
+                p.write_text(json.dumps(receipt));script='independent.py'
+            result=subprocess.run([sys.executable,'-I','-O','-B',str(copied/script)],cwd=copied,
+                                  capture_output=True,text=True,timeout=30)
+            need(result.returncode!=0 and 'ValueError:' in result.stderr,'mutation accepted or unrelated failure: '+case)
+    print('PASS_THREE_CYCLE_CONTROLS optimized_cli_mutations=6')
+if __name__=='__main__':run()
diff --git a/research/three-cycle-address-floor/verify.py b/research/three-cycle-address-floor/verify.py
new file mode 100644
index 0000000000..0cea0e5b5b
--- /dev/null
+++ b/research/three-cycle-address-floor/verify.py
@@ -0,0 +1,155 @@
+#!/usr/bin/env python3
+"""Exact address exclusion and formal controls; uniform reduction is PROOF.md.
+JoyboyBrian, substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import argparse
+import hashlib
+import itertools
+import json
+from pathlib import Path
+
+HERE=Path(__file__).resolve().parent
+
+def need(ok,message):
+    if not ok: raise ValueError(message)
+
+def identity(n): return tuple(1<<i for i in range(n))
+def add(matrix,gate):
+    i,j=gate;n=len(matrix)
+    need(0<=i<n and 0<=j<n and i!=j,'illegal coordinate CNOT')
+    rows=list(matrix);rows[i]^=rows[j];return tuple(rows)
+def product(a,b):
+    need(len(a)==len(b),'matrix dimensions')
+    out=[]
+    for row in a:
+        value=0
+        for j in range(len(a)):
+            if row>>j&1:value^=b[j]
+        out.append(value)
+    return tuple(out)
+def inverse(matrix):
+    n=len(matrix);rows=[x|(1<<(n+i)) for i,x in enumerate(matrix)]
+    for j in range(n):
+        candidates=[k for k in range(j,n) if rows[k]>>j&1]
+        need(candidates,'singular matrix')
+        k=candidates[0];rows[j],rows[k]=rows[k],rows[j]
+        for k in range(n):
+            if k!=j and rows[k]>>j&1:rows[k]^=rows[j]
+    return tuple(x>>n for x in rows)
+def apply_word(n,word):
+    result=identity(n)
+    for g in word:result=add(result,g)
+    return result
+
+def ball(n,radius):
+    gates=[(i,j) for i in range(n) for j in range(n) if i!=j]
+    words={identity(n):()};front={identity(n)};layers=[1]
+    for _ in range(radius):
+        following=set()
+        for matrix in sorted(front):
+            for gate in gates:
+                target=add(matrix,gate)
+                if target not in words:
+                    words[target]=words[matrix]+(gate,);following.add(target)
+        layers.append(len(following));front=following
+    need(all(apply_word(n,w)==m for m,w in words.items()),'stored address words')
+    return words,layers
+
+def encode(value):return json.dumps(value,sort_keys=True,separators=(',',':'))
+def digest(value):return hashlib.sha256(encode(value).encode()).hexdigest()
+
+def matrix_xor(a,b):return tuple(x^y for x,y in zip(a,b))
+def formal_product(a,b):
+    out={}
+    for g,x in a.items():
+        for h,y in b.items():
+            label=product(g,h);coefficient=product(x,y)
+            out[label]=matrix_xor(out.get(label,(0,)*len(x)),coefficient)
+    return {g:m for g,m in out.items() if any(m)}
+def scalar(n,matrix):return {identity(n):matrix}
+def paid(n,r,gate,u,v):
+    need(0<u<1<<r and 0<v<1<<r and (u&v).bit_count()%2==1,'rank-one idempotent')
+    N=tuple(v if u>>i&1 else 0 for i in range(r))
+    label=add(identity(n),gate)
+    result={identity(n):matrix_xor(identity(r),N),label:N}
+    return {g:m for g,m in result.items() if any(m)}
+
+def formal_controls():
+    word=((0,1),(1,0),(0,1),(1,2),(2,1),(1,2))
+    fixtures=[]
+    for n,r in ((3,1),(4,3),(8,5)):
+        cycle=apply_word(n,word)
+        need(cycle==tuple([2,4,1]+[1<<i for i in range(3,n)]),'cycle orientation')
+        E=tuple(1 if i==0 else 0 for i in range(r))
+        expected={identity(n):matrix_xor(identity(r),E),cycle:E}
+        expected={g:m for g,m in expected.items() if any(m)}
+        current=scalar(n,identity(r))
+        for gate in word:current=formal_product(paid(n,r,gate,1,1),current)
+        need(current==expected,'six-call full formal endpoint')
+        # Scalar conjugation produces dense projectors; scalar frames then undo it.
+        B=identity(r)
+        for i in range(1,r):B=add(B,(i,0))
+        if r>1:B=add(B,(0,r-1))
+        Bi=inverse(B);u=sum(((B[i]&1)!=0)<<i for i in range(r));v=Bi[0]
+        dense=scalar(n,B)
+        for gate in word:dense=formal_product(paid(n,r,gate,u,v),dense)
+        dense=formal_product(scalar(n,Bi),dense)
+        need(dense==expected,'free scalar frames and dirty restoration')
+        inv_word=tuple(reversed(word));inv_target=apply_word(n,inv_word)
+        need(product(cycle,inv_target)==identity(n) and cycle!=inv_target,'inverse cycle distinction')
+        fixtures.append({'n':n,'R':r,'coefficient_terms':len(current),'dense_projector':[u,v],
+                         'endpoint_sha256':digest(sorted(current.items()))})
+    # Arbitrary mixing cannot create group support outside label subwords.
+    n=r=3;labels=((0,1),(1,2),(2,0),(1,0));current=scalar(n,identity(r));subwords={identity(n)}
+    couplings=((3,1),(6,2),(5,4),(7,1))
+    for i,(label,(u,v)) in enumerate(zip(labels,couplings)):
+        current=formal_product(paid(n,r,label,u,v),current)
+        group=add(identity(n),label)
+        subwords|={product(group,h) for h in subwords}
+        frame=add(identity(r),(i%r,(i+1)%r))
+        current=formal_product(scalar(n,frame),current)
+        need(set(current)<=subwords,'formal subword support')
+    # An actual nonzero formal element can vanish in the natural representation.
+    gl2=[(a,b) for a in range(1,4) for b in range(1,4) if a!=b]
+    total=(0,0)
+    for g in gl2:total=matrix_xor(total,g)
+    need(total==(0,0) and len(gl2)==6,'natural representation alias control')
+    omitted=sum(apply_word(4,word[:i]+word[i+1:])!=(2,4,1,8) for i in range(6))
+    need(omitted==6,'omitted upper-bound call')
+    wrong=word[:-1]+((0,2),)
+    need(apply_word(4,wrong)!=(2,4,1,8),'wrong final label')
+    need(apply_word(4,word+((3,0),))!=(2,4,1,8),'unreturned address spectator')
+    for gate in ((0,0),(4,0),(-1,0)):
+        try:add(identity(4),gate)
+        except ValueError:pass
+        else:raise ValueError('illegal label accepted')
+    return {'fixtures':fixtures,'support_word_calls':len(labels),'support_terms':len(current),
+            'subword_elements':len(subwords),'omission_controls':omitted,
+            'other_semantic_controls':6,'natural_alias_terms':len(gl2)}
+
+def calculate():
+    B,layers=ball(4,3);B2={m for m,w in B.items() if len(w)<=2};target=(2,4,1,8)
+    need(layers==[1,12,96,542],'complete exact address layers')
+    hits=[m for m in B if product(inverse(m),target) in B2]
+    need(not hits,'three-cycle reached within five address calls')
+    # Positive bridge control: a five-call endpoint must be detected.
+    short=apply_word(4,((0,1),(1,0),(0,1),(1,2),(2,1)))
+    short_hits=sum(product(inverse(m),short) in B2 for m in B)
+    need(short_hits>0,'short target positive join')
+    six_hits=sum(product(inverse(m),target) in B for m in B)
+    need(six_hits>0,'six-call target reachability')
+    return {'status':'PASS_THREE_CYCLE_ADDRESS_FLOOR','address_dimension_checked':4,
+            'generators':12,'layers':layers,'ball_two':len(B2),'ball_three':len(B),
+            'ball_three_sha256':digest(sorted(B)),'joins_through_five':len(B),
+            'target_hits_through_five':len(hits),'six_call_joins':six_hits,
+            'short_target_positive_joins':short_hits,'minimum':6,
+            'uniform_scope':'one coordinate three-cycle; all finite n>=3 and R>=1 by PROOF.md',
+            'controls':formal_controls()}
+
+def main():
+    parser=argparse.ArgumentParser();parser.add_argument('--emit',action='store_true');args=parser.parse_args()
+    actual=calculate()
+    if args.emit:print(json.dumps(actual,indent=2,sort_keys=True));return
+    need(encode(actual)==encode(json.loads((HERE/'RESULT.json').read_text())),'receipt mismatch')
+    print('PASS_THREE_CYCLE_ADDRESS_FLOOR minimum=6 GL4_ball3=651 five_call_hits=0')
+if __name__=='__main__':main()