diff --git a/research/bit-address-twist-register-floor/PROOF.md b/research/bit-address-twist-register-floor/PROOF.md
new file mode 100644
index 0000000000..26cbb34d5a
--- /dev/null
+++ b/research/bit-address-twist-register-floor/PROOF.md
@@ -0,0 +1,190 @@
+# Address twists: one-sided floor and a two-sided relaxation witness
+
+## 1. Model with free address twists
+
+Fix an address dimension $m$ and $R$ binary roles. Each role holds an element
+of $\mathbb F_2[M_m(\mathbb Q)]$, with $[A][B]=[A+B]$. A **paid call** is
+
+$$
+D_N([A])=I_R+([A]-1)N,\qquad \operatorname{rank}_{\mathbb Q}A=1,\qquad
+N=xy^T,\ x,y\in\mathbb F_2^R,\ y^Tx=1 .
+$$
+
+Free operations are binary $GL_R(\mathbb F_2)$ mixing and, new here, a
+**twist** of one role $r$ by an additive automorphism
+
+$$
+\varphi_{P,Q}(B)=PBQ,\qquad P,Q\in GL_m(\mathbb Z_{(2)}),
+$$
+
+acting on that role's content by $[B]\mapsto[\varphi(B)]$ and leaving the other
+roles unchanged. Twists may be applied to any role, at any time, any number
+of times. Conjugating an XOR by a twist gives a twisted XOR
+$f_r\mathrel{+}=\varphi(f_s)$, so the operators form matrices over the skew
+group ring $\mathbb F_2[M_m(\mathbb Q)]\rtimes G$. This ring is not
+commutative. The predecessors listed in the README exclude exactly these free
+address maps.
+
+Roles $0,\ldots,W-1$ are data roles; any further roles are dirty helpers. The
+endpoint is
+
+$$
+\operatorname{diag}([C_0],\ldots,[C_{W-1}],1,\ldots,1)
+$$
+
+as an operator, with every helper restored. The **odd-denominator
+hypothesis** is $A_j\in\Gamma:=M_m(\mathbb Z_{(2)})$ for every paid frame.
+Because twists preserve $\Gamma$, the submodule $\mathbb F_2[\Gamma]^R$ is
+invariant under every operation. The endpoint restricted to it sends
+$[0]e_s$ to $[C_s]e_s$, so each $C_s\in\Gamma$. Write $\bar X$ for reduction
+modulo two and $\bar\varphi(X)=\bar P X\bar Q$.
+
+## 2. Square-zero image
+
+Let $\Lambda=\mathbb F_2\oplus M_m(\mathbb F_2)$ with $(a,X)(b,Y)=(ab,aY+bX)$.
+The map $\pi([A])=(1,\bar A)$ is a ring homomorphism
+$\mathbb F_2[\Gamma]\to\Lambda$, because $\overline{A+B}=\bar A+\bar B$. Let
+$K=\ker\pi$.
+
+Each operation preserves $K^R$. Paid calls are $\mathbb F_2[\Gamma]$-linear
+and mixing is scalar. For a twist, $\pi\circ\varphi=\bar\varphi_\Lambda\circ\pi$,
+where $\bar\varphi_\Lambda(c,X)=(c,\bar P X\bar Q)$ is a ring automorphism of
+$\Lambda$. Hence $\varphi(K)=K$. Every operation therefore descends to
+$\Lambda^R$, and the descended word equals the descended endpoint.
+
+Write a state as $(c,w)$ with $c\in\mathbb F_2^R$ and
+$w\in M_m(\mathbb F_2)^R$. The descended operations are:
+
+- mixing $E$: $(c,w)\mapsto(Ec,(E\otimes 1)w)$;
+- twist of role $r$: $c$ is unchanged and $w_r\mapsto\bar P w_r\bar Q$;
+- paid call: $(c,w)\mapsto(c,\ w+(y^Tc)\,x\otimes\bar A)$, since
+  $([A]-1)\mapsto(0,\bar A)$ and $(0,\bar A)(0,X)=0$.
+
+Twists never change $c$, and paid calls do not change how $w$ is transported.
+Let $E_{<j}$ be the product of mixings before call $j$, and $\Psi_j$ the
+composite of free operations after it, acting on $M_m(\mathbb F_2)^R$. For
+$w=0$, the final $w$-part is
+
+$$
+w_{\rm fin}=\sum_{j=1}^k(\hat y_j^Tc)\,\Psi_j(x_j\otimes\bar A_j),
+\qquad \hat y_j=E_{<j}^Ty_j. \tag{1}
+$$
+
+The endpoint requires $w_{{\rm fin},r}=\delta_{rs}\bar C_s$ when $c=e_s$ for
+a data role $s$. Let $L$ be the linear map $c\mapsto w_{\rm fin}$, with
+coefficients $L[(r,i),(s,l)]$ giving entry $(i,l)$ of block $r$ from $c_s$.
+
+## 3. Theorem A: one-sided twists keep the floor
+
+**Theorem A.** Assume the odd-denominator hypothesis. Suppose also that every
+twist used reduces modulo two to a left multiplication
+$X\mapsto\bar PX$ (condition L), or every twist reduces to a right
+multiplication $X\mapsto X\bar Q$ (condition R). Then every exact word has
+
+$$
+k\ \ge\ \sum_{s<W}\operatorname{rank}_{\mathbb F_2}\bar C_s .
+$$
+
+This holds for any finite number of dirty helpers and any binary mixing.
+
+*Proof.* Write $A_j=a_jb_j^T$ with $a_j$ primitive in $\mathbb Z_{(2)}^m$.
+Some coordinate of $a_j$ is a unit, so $b_j\in\mathbb Z_{(2)}^m$ and
+$\bar A_j=\bar a_j\bar b_j^T$.
+
+Under condition L, every map making up $\Psi_j$ commutes with blockwise right
+multiplication by a fixed matrix. Mixing acts across roles, and twists act by
+left multiplication. Put $B_j=e_1\bar b_j^T$. Then
+$x_j\otimes\bar A_j=(x_j\otimes\bar a_je_1^T)B_j$, so
+
+$$
+\Psi_j(x_j\otimes\bar A_j)=\Psi_j(x_j\otimes\bar a_je_1^T)\,B_j .
+$$
+
+Let $u_j\in(\mathbb F_2^m)^R$ be the first column of
+$\Psi_j(x_j\otimes\bar a_je_1^T)$. By (1),
+
+$$
+L[(r,i),(s,l)]=\sum_{j=1}^k u_j(r,i)\,\bar b_j(l)\,\hat y_j(s).
+$$
+
+This matrix, with rows $(r,i)$ and columns $(s,l)$, is a sum of $k$ matrices
+of rank at most one. Its data-to-data block must equal
+$\operatorname{diag}(\bar C_0,\ldots,\bar C_{W-1})$, whose rank is
+$\sum_s\operatorname{rank}\bar C_s$. A submatrix has rank at most that of the
+whole matrix.
+
+Under condition R, every map commutes with blockwise left multiplication.
+Write $x_j\otimes\bar A_j=(\bar a_je_1^T)(x_j\otimes e_1\bar b_j^T)$. Let
+$v_j(r,l)$ be the first row of the transported block. Then
+$L[(r,l),(s,i)]=\sum_j v_j(r,l)\,\bar a_j(i)\,\hat y_j(s)$. With rows $(r,l)$
+and columns $(s,i)$, the target block is
+$\operatorname{diag}(\bar C_s^T)$, with the same rank. $\square$
+
+The proof uses only the data-to-data block, so the bound also holds when
+helper outputs are discarded. With no twists, this is the square-zero bound
+of #2110, extended from one lattice $q^{-1}M_m(\mathbb Z)$ to
+$M_m(\mathbb Z_{(2)})$. Because $q$ is odd, $\overline{qC}$ and $\bar C$
+have the same rank.
+
+**Corollary.** Let the three targets of the three-register model have odd
+denominators, with each $\bar C_s$ invertible. Then one-sided twists and any
+number of dirty helpers still need nine calls. The untwisted direct column
+word uses nine, so nine is the exact minimum in this scoped model.
+
+*Why one-sidedness is needed.* For a two-sided twist,
+$\Psi_j(x_j\otimes\bar a\bar b^T)$ can place $\bar P_r\bar a(\bar Q_r\bar b)^T$
+in role $r$ with $\bar Q_r$ depending on $r$. Then neither flattening
+factors. The witness below shows this matters.
+
+## 4. Proposition B: two-sided twists defeat the square-zero relaxation
+
+Let $m=3$, $W=R=3$, and $C_0=C_1=C_2=I$. Let $\sigma(B)=SBS^T$, where $S$
+swaps address axes 0 and 1. This is a simultaneous relabelling: $P=S$ and
+$Q=S^T$, so condition L and condition R both fail. Use seven calls:
+
+- **J:** $x=y=(1,1,1)$ with frame $E_{00}$ and no twist.
+- **P$_s$** for $s=0,1,2$: twist every role $r\ne s$ by $\sigma$. Then call
+  with $x=(1,1,1)$, $y=e_s$ and frame $E_{11}$, and undo the twist.
+- **D$_s$** for $s=0,1,2$: call with $x=y=e_s$ and frame $E_{22}$.
+
+**Proposition B.** In every one of the $7!=5040$ call orders, the
+square-zero image of the word in $M_3(\Lambda\rtimes G)$ equals that of
+$\operatorname{diag}([I],[I],[I])$. No order realizes the endpoint exactly.
+
+For the $L$ part, column $s$ receives three kinds of contribution:
+
+- **J** adds $E_{00}$ to every block.
+- **P$_s$** adds $E_{11}$ to block $s$. It adds $\sigma(E_{11})=E_{00}$ to
+  every other block.
+- **D$_s$** adds $E_{22}$ to block $s$.
+
+Block $s$ therefore receives $E_{00}+E_{11}+E_{22}=I$, and each other block
+receives $E_{00}+E_{00}=0$. The constant and twist components agree as well.
+`verify.py` checks the full image entry by entry for all 5040 orders. It also
+computes each exact skew-ring product and finds no exact order.
+
+Hence no argument that factors through $\pi$ can prove nine calls once
+two-sided twists are free; this includes Theorem A and the argument of #2110.
+Seven calls pass that relaxation. This is a barrier to the
+**method**. It is neither a seven-call word nor a lower bound below nine:
+whether two-sided twists can beat nine remains open.
+
+## 5. Checked finite evidence and limits
+
+`verify.py` checks the following with exact finite sets in the skew group
+ring:
+
+1. The direct nine-call word is exact, with zero and one dirty helpers.
+2. A deleted call and a mutated frame are rejected.
+3. In 120 seeded random words per side, with 1–4 calls, 3–4 roles, random
+   twists, mixing and odd-denominator integer frames, the correct flattening
+   has rank at most $k$. The opposite flattening exceeds $k$ in many of
+   these words.
+4. Proposition B holds for all 5040 orders, with no exact order.
+5. Controls reject the witness against altered targets, untwisted private
+   calls and left-only private twists.
+
+The random words corroborate Theorem A; the written proof establishes it.
+Proposition B is a finite exact statement about one explicit word family.
+Neither result covers clean ancillas, twists not of the form $PBQ$,
+even-denominator frames, or any native implementation or price of a twist.
diff --git a/research/bit-address-twist-register-floor/README.md b/research/bit-address-twist-register-floor/README.md
new file mode 100644
index 0000000000..e6caa7a011
--- /dev/null
+++ b/research/bit-address-twist-register-floor/README.md
@@ -0,0 +1,130 @@
+# Free address twists: one-sided twists keep the nine-call floor
+
+**Scoped written proof with exact finite corroboration, plus a relaxation
+barrier. No new κ, no supplier and no native implementation.**
+
+## Changed hypothesis
+
+[The three-register bound](../bit-three-register-lower-bound/README.md)
+(Ali Romman, #468) excludes free address maps between paid calls. So do its
+dirty-workspace, clean-ancilla and odd-denominator successors. This package
+allows them.
+
+Between calls, any role may be relabelled by an additive automorphism
+$B\mapsto PBQ$ of the address group, with $P,Q\in GL_m(\mathbb Z_{(2)})$.
+These relabellings are free. Binary XOR mixing and any number of restored dirty
+roles are also free. Paid calls are unchanged: $D_N([A])$ with rational
+rank-one $A$ and binary rank-one idempotent $N$. Conjugating an XOR by a twist
+gives the twisted XOR $f_r\mathrel{+}=\varphi(f_s)$. Operators therefore lie
+in matrices over the skew group ring
+$\mathbb F_2[M_m(\mathbb Q)]\rtimes G$, a nonabelian operation family.
+
+Counted roles: $W$ data roles with diagonal targets $[C_s]$ and any number of
+dirty helpers restored to $1$. Every paid call counts, including any call that
+acts only on a helper. Twists and XORs cost nothing in this formal model.
+
+## Result
+
+**Theorem A (uniform, [PROOF.md](PROOF.md) §3).** Assume every paid frame
+lies in $M_m(\mathbb Z_{(2)})$. Assume also that every twist reduces modulo
+two to a one-sided map: $X\mapsto\bar PX$ for all twists, or
+$X\mapsto X\bar Q$ for all twists. Then every exact word needs at least
+$\sum_s\operatorname{rank}_{\mathbb F_2}(C_s\bmod 2)$ paid calls. This holds
+for any number of dirty helpers. For three targets invertible modulo two,
+such as $I$, $I+E_{10}$ and $I+E_{21}$, the bound is nine. The direct word
+attains it, so nine is exact.
+
+The proof uses the square-zero homomorphism $[A]\mapsto(1,A\bmod 2)$ of
+#2110 (1337isnot1337 / Cinna Davis). The twists are equivariant for this map.
+One-sidedness then keeps every call's contribution rank one in a suitable
+flattening.
+
+**Proposition B (finite exact, PROOF.md §4).** Two-sided twists break this
+argument. Let $\sigma$ simultaneously swap address axes $0$ and $1$, so that
+$B\mapsto SBS^T$. An explicit seven-call word for
+$\operatorname{diag}([I],[I],[I])$ then agrees with the target in the
+complete square-zero image $M_3(\Lambda\rtimes G)$, in all $5040$ call
+orders. The word has:
+
+- one all-role call on $E_{00}$;
+- three private calls on $E_{11}$, with $\sigma$ applied to the other two roles;
+- three diagonal calls on $E_{22}$.
+
+Exact products show that no order is a real identity. Therefore no square-zero
+argument, including Theorem A and #2110, can prove nine once two-sided twists
+are free. Whether two-sided twists can beat nine **remains open**. This
+package claims neither a seven-call word nor a lower bound for that model.
+
+Answer to the card: one explicitly specified nonabelian register model, with
+one-sided address twists, does **not** escape the scoped obstruction in the
+odd-denominator domain. For two-sided twists, the inexpensive obstruction
+method fails. That leaves a precise open target.
+
+## Scope limits
+
+The result concerns formal group-algebra identities. It does not cover:
+
+- clean ancillas;
+- twists not of the form $PBQ$, such as transposition;
+- even-denominator frames;
+- mixtures of left-only and right-only twists.
+
+A finite address identity is not a supplier. The physical meaning and price of
+a free relabelling are not established. The random-word checks corroborate
+Theorem A but do not prove it.
+
+## Reproduce
+
+From the repository root, with Python 3.12 and the standard library:
+
+```sh
+python3.12 -B research/bit-address-twist-register-floor/verify.py
+python3 scripts/research_package.py --package research/bit-address-twist-register-floor --check-only
+python3.12 -B scripts/research_package.py --package research/bit-address-twist-register-floor
+```
+
+The verifier runs in about six seconds. It checks:
+
+- the exact direct nine-call word, with zero and one dirty helpers;
+- controls rejecting a deleted call and a mutated frame;
+- 120 seeded random words for each of the left-only and right-only twist
+  models, with mixing and helpers, where the correct flattening has rank at
+  most the number of calls;
+- that the opposite flattening exceeds the call count, so the side condition
+  is necessary for the argument;
+- all 5040 witness orders exactly, with relaxation agreement and no exact
+  identity;
+- controls rejecting an altered target, untwisted private calls and left-only
+  private twists.
+
+## Open next questions
+
+1. **Can two-sided twists beat nine exactly?** If they can, the free-relabelling
+   premise changes the bit primitive's paid count. Otherwise the floor extends
+   to all $PBQ$ twists. A first step is to compute the order-two term, modulo
+   the cube of the augmentation ideal, for the seven-call frame multiset over
+   all $S_3\times S_3$ twist assignments. That gives a second-order cut or a
+   candidate. A complete search is blocked by the size of the twist alphabet.
+   An exact identity also needs a rank-type invariant that survives
+   $\mathbb F_2[G]$ zero divisors.
+2. **Is a free address relabelling legal and free in the native bit
+   supplier?** Any formal saving matters only if a native layout implements a
+   per-register $PBQ$ change for less than the call it saves. The first step
+   is to identify which address maps the selected bit word's physical layout
+   applies without paid work. That needs a native model, which this package
+   does not provide.
+3. **Do mixed left-only and right-only twists help?** Neither flattening
+   applies directly when both kinds occur. The first step is a small exact
+   relaxation search over left and right axis swaps with at most eight calls.
+
+## Credit
+
+The three-register model and nine-call theorem are by Ali Romman (#468), using
+eumemic's model (#288 §1.2) and huxint's flag method (#203). The square-zero
+method and the odd-denominator floor are by 1337isnot1337 / Cinna Davis
+(#2110, `research/bit-odd-denominator-register-floor-seed16c946`). Theorem A
+extends that method to address twists. The twist model, Theorem A,
+Proposition B and the verifier are new here and were prepared by JoyboyBrian,
+with substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).
+No independent human review or proof-assistant formalization is claimed.
+New work is Apache-2.0.
diff --git a/research/bit-address-twist-register-floor/SOURCES.json b/research/bit-address-twist-register-floor/SOURCES.json
new file mode 100644
index 0000000000..652795f221
--- /dev/null
+++ b/research/bit-address-twist-register-floor/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "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/bit-odd-denominator-register-floor-seed16c946/PROOF.md",
+      "usage": "input",
+      "git_blob": "5130a50440880fcfe8cbee4ef63626afaf2f8769",
+      "sha256": "b61807b41b4a55c37fb01e6d73e7816b7381a629f0dfc3beeaf4f567180ffb00"
+    },
+    {
+      "path": "research/bit-three-register-lower-bound/README.md",
+      "usage": "input",
+      "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
+      "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
+    }
+  ]
+}
diff --git a/research/bit-address-twist-register-floor/TASK.json b/research/bit-address-twist-register-floor/TASK.json
new file mode 100644
index 0000000000..d6f0b87f11
--- /dev/null
+++ b/research/bit-address-twist-register-floor/TASK.json
@@ -0,0 +1,76 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "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": "refined",
+  "actual_scope": "Changed hypothesis: free per-register address twists B -> P B Q (P, Q in GL_m(Z_(2))) between paid calls, which the three-register bound and its successors exclude; with binary mixing and any number of restored dirty roles. Question: can such twists beat sum_s rank(C_s mod 2) (nine for three targets invertible mod 2)? Domain: odd-denominator frames, formal group-algebra identities.",
+  "scope_change_reason": "The card allows a specified nonabelian operation family. Twisted XORs make the operator ring a skew group ring F2[H] x| G with an abelian address group, unlike the nonabelian address groups (Q8, D16, GL_n(F2), A5, ...) already studied. Free address maps are the hypothesis every predecessor names as excluded.",
+  "bottleneck_link": "Side result for the bit primitive: it decides whether free relabellings can reduce the paid call count of the bit interchange. One-sided relabellings cannot in the odd-denominator domain. For two-sided relabellings, the square-zero obstruction is shown to be powerless, which isolates what an exact saving or a stronger cut must handle.",
+  "budget_minutes": 150,
+  "stop_rule": "Stop after a uniform proof for one explicit twist model plus an exact finite witness or obstruction for the complementary model. Do not run open-ended searches over the S3 x S3 twist alphabet in this session.",
+  "outcome": "partial",
+  "evidence": "Written proof of Theorem A (PROOF.md section 3). Exact skew-ring verifier: the direct nine-call word; 240 seeded random one-sided-twist words satisfying the flattening bound, with the opposite flattening exceeding it; and all 5040 orders of the seven-call two-sided witness agreeing with the target in the square-zero image, none exact. Mutation controls are rejected.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5)",
+  "open_questions": [
+    {
+      "question": "Can two-sided address twists (for example B -> S B S^T) realize three invertible targets with fewer than nine paid calls exactly?",
+      "why_it_matters": "A yes would change the paid count of the bit primitive under a free-relabelling premise. A no would extend the floor to all PBQ twists.",
+      "first_step": "Compute the order-two term (modulo the cube of the augmentation ideal) of the seven-call frame multiset over all S3 x S3 twist assignments, to obtain a second-order cut or a candidate.",
+      "blocked_by": "Size of the twist alphabet, and the lack of a rank invariant robust to F2[G] zero divisors."
+    },
+    {
+      "question": "Does the native bit supplier implement a per-register PBQ address relabelling without paid work?",
+      "why_it_matters": "A formal saving matters only if the relabelling is legal and cheaper than the call it saves.",
+      "first_step": "Identify which address maps the selected bit word's physical layout applies for free.",
+      "blocked_by": "No native model of address relabelling in this package."
+    },
+    {
+      "question": "Do words mixing left-only and right-only twists evade the floor?",
+      "why_it_matters": "Neither flattening applies directly, so this is the smallest gap between Theorem A and the open two-sided case.",
+      "first_step": "Run an exact square-zero relaxation search with left and right axis swaps and at most eight calls.",
+      "blocked_by": "Nothing beyond search budget."
+    }
+  ]
+}
diff --git a/research/bit-address-twist-register-floor/VERIFY.json b/research/bit-address-twist-register-floor/VERIFY.json
new file mode 100644
index 0000000000..0d92b0e496
--- /dev/null
+++ b/research/bit-address-twist-register-floor/VERIFY.json
@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/bit-odd-denominator-register-floor-seed16c946/PROOF.md",
+    "research/bit-three-register-lower-bound/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact direct nine-call word with deletion/frame mutation controls; one-sided flattening bound on 240 seeded random twisted words with opposite-flattening control; all 5040 orders of the two-sided seven-call witness match the target in the square-zero image and none is exact; altered-target, untwisted and left-only witness controls."
+    }
+  ]
+}
diff --git a/research/bit-address-twist-register-floor/verify.py b/research/bit-address-twist-register-floor/verify.py
new file mode 100644
index 0000000000..5fa63f7c2d
--- /dev/null
+++ b/research/bit-address-twist-register-floor/verify.py
@@ -0,0 +1,351 @@
+"""Exact checks for free per-register address twists in the formal bit model.
+
+Model: R binary roles holding elements of F2[M_3(Q)].  A paid call is
+D_N([A]) = I + ([A]-1) x y^T with A rank one and y^T x = 1 over F2.  Free
+operations are binary XOR mixing and a per-register twist [B] -> [P B Q^T]
+for axis permutations P, Q.  Operators are matrices over the skew group ring
+F2[M_3(Q)] x| G, represented exactly as finite sets of (frame, twist) pairs.
+
+The verifier checks the finite statements recorded in README.md and PROOF.md:
+the one-sided flattening lemma on seeded random words, the exact direct
+nine-call word, and the two-sided seven-call relaxation witness (all 5040
+orders agree with the target in the square-zero quotient, none exactly).
+Python 3.12 standard library only.  Apache-2.0.  JoyboyBrian, with
+substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).
+"""
+
+import itertools
+import random
+import sys
+
+M = 3
+P_ID = (0, 1, 2)
+TW_ID = (P_ID, P_ID)
+Z9 = (0,) * 9
+
+EXPECTED = {
+    "direct_word_calls": 9,
+    "floor_three_targets": 9,
+    "witness_calls": 7,
+    "witness_orders": 5040,
+    "witness_exact_orders": 0,
+    "random_words_per_side": 120,
+}
+
+
+def fail(msg):
+    print("FAIL:", msg)
+    sys.exit(1)
+
+
+def check(cond, msg):
+    if not cond:
+        fail(msg)
+
+
+def unit(i, j):
+    a = [0] * 9
+    a[M * i + j] = 1
+    return tuple(a)
+
+
+def mat_add(*frames):
+    return tuple(sum(col) for col in zip(*frames))
+
+
+def act(tw, a):
+    """Twist (pl, pr): (P_l A P_r^T)[pl[i], pr[j]] = A[i, j]."""
+    pl, pr = tw
+    out = [0] * 9
+    for i in range(M):
+        for j in range(M):
+            out[M * pl[i] + pr[j]] = a[M * i + j]
+    return tuple(out)
+
+
+def tw_comp(s, t):
+    return (tuple(s[0][t[0][i]] for i in range(M)), tuple(s[1][t[1][i]] for i in range(M)))
+
+
+def tw_inv(t):
+    def inv(p):
+        q = [0] * M
+        for i, v in enumerate(p):
+            q[v] = i
+        return tuple(q)
+    return (inv(t[0]), inv(t[1]))
+
+
+ONE = frozenset({(Z9, TW_ID)})
+ZERO = frozenset()
+
+
+def mul(x, y):
+    out = set()
+    for a, g in x:
+        for b, h in y:
+            out ^= {(tuple(u + v for u, v in zip(a, act(g, b))), tw_comp(g, h))}
+    return frozenset(out)
+
+
+def xsum(items):
+    out = set()
+    for v in items:
+        out ^= v
+    return frozenset(out)
+
+
+def mat_mul(x, y):
+    n = len(x)
+    return [[xsum(mul(x[i][k], y[k][j]) for k in range(n)) for j in range(n)] for i in range(n)]
+
+
+def ident(n):
+    return [[ONE if i == j else ZERO for j in range(n)] for i in range(n)]
+
+
+def paid(n, x, y, a):
+    check(sum(u & v for u, v in zip(x, y)) % 2 == 1, "paid projector is not idempotent")
+    check(rank_q_one(a), "paid frame is not rank one")
+    d = frozenset({(a, TW_ID), (Z9, TW_ID)})
+    return [[xsum([ONE if i == j else ZERO, d if x[i] and y[j] else ZERO]) for j in range(n)] for i in range(n)]
+
+
+def twist(n, tws):
+    return [[frozenset({(Z9, tws[i])}) if i == j else ZERO for j in range(n)] for i in range(n)]
+
+
+def xor_into(n, dst, src):
+    m = ident(n)
+    m[dst][src] = ONE
+    return m
+
+
+def product(n, ops):
+    t = ident(n)
+    for op in ops:
+        t = mat_mul(op, t)
+    return t
+
+
+def rank_q_one(a):
+    rows = [a[M * i:M * i + M] for i in range(M)]
+    nz = [r for r in rows if any(r)]
+    if not nz:
+        return False
+    r0 = nz[0]
+    return all(r0[i] * r[j] == r0[j] * r[i] for r in nz for i in range(M) for j in range(M))
+
+
+def square_zero(entry):
+    """Image in Lambda x| G with Lambda = F2 + M_3(F2) eps, eps^2 = 0."""
+    c = 0
+    lin = [0] * 9
+    tw = set()
+    for a, g in entry:
+        c ^= 1
+        lin = [(u + v) % 2 for u, v in zip(lin, a)]
+        tw ^= {g}
+    return c, tuple(lin), frozenset(tw)
+
+
+def sz_matrix(t):
+    return [[square_zero(e) for e in row] for row in t]
+
+
+def target(cs, n):
+    return [[frozenset({(cs[i], TW_ID)}) if i == j and i < len(cs) else (ONE if i == j else ZERO)
+             for j in range(n)] for i in range(n)]
+
+
+def rank_f2(rows):
+    rank = 0
+    rows = [r for r in rows if r]
+    while rows:
+        pivot = rows.pop()
+        if not pivot:
+            continue
+        rank += 1
+        low = pivot & -pivot
+        rows = [r ^ pivot if r & low else r for r in rows]
+        rows = [r for r in rows if r]
+    return rank
+
+
+def flattened_rank(sz, side):
+    """Rank of L: c -> w.  'left' rows (r,i) cols (s,l); 'right' rows (r,l) cols (s,i)."""
+    n = len(sz)
+    rows = []
+    for r in range(n):
+        for p in range(M):
+            bits = 0
+            for s in range(n):
+                lin = sz[r][s][1]
+                for q in range(M):
+                    val = lin[M * p + q] if side == "left" else lin[M * q + p]
+                    if val:
+                        bits |= 1 << (M * s + q)
+            rows.append(bits)
+    return rank_f2(rows)
+
+
+# Targets: invertible lower-triangular integer frames, invertible mod 2.
+C1 = mat_add(unit(0, 0), unit(1, 1), unit(2, 2))
+C2 = mat_add(C1, unit(1, 0))
+C3 = mat_add(C1, unit(2, 1))
+TARGETS = [C1, C2, C3]
+
+
+def columns(c):
+    out = []
+    for j in range(M):
+        col = [0] * 9
+        for i in range(M):
+            col[M * i + j] = c[M * i + j]
+        out.append(tuple(col))
+    return out
+
+
+def direct_word(n):
+    ops = []
+    for r, c in enumerate(TARGETS):
+        e = tuple(int(k == r) for k in range(n))
+        ops += [paid(n, e, e, col) for col in columns(c)]
+    return ops
+
+
+def check_direct():
+    for n in (3, 4):
+        ops = direct_word(n)
+        check(len(ops) == EXPECTED["direct_word_calls"], "direct word length")
+        check(product(n, ops) == target(TARGETS, n), "direct word is not exact")
+        check(product(n, ops[1:]) != target(TARGETS, n), "deleted-call control passed")
+    bad = direct_word(3)
+    bad[4] = paid(3, (0, 1, 0), (0, 1, 0), mat_add(unit(1, 1), unit(2, 1)))
+    check(product(3, bad) != target(TARGETS, 3), "mutated-frame control passed")
+    floor = flattened_rank(sz_matrix(target(TARGETS, 3)), "left")
+    check(floor == EXPECTED["floor_three_targets"], "target flattened rank")
+    check(flattened_rank(sz_matrix(target(TARGETS, 3)), "right") == floor, "right flattening of target")
+    print("direct word: exact with 0/1 dirty helper; deletion and frame mutation rejected; floor", floor)
+
+
+def random_frame(rng):
+    while True:
+        a = [rng.choice((-2, -1, 0, 1, 1, 2, 3)) for _ in range(M)]
+        b = [rng.choice((-1, 0, 1, 1, 2)) for _ in range(M)]
+        f = tuple(a[i] * b[j] for i in range(M) for j in range(M))
+        if any(f):
+            return f
+
+
+def random_projector(rng, n):
+    while True:
+        x = tuple(rng.randint(0, 1) for _ in range(n))
+        y = tuple(rng.randint(0, 1) for _ in range(n))
+        if sum(u & v for u, v in zip(x, y)) % 2 == 1:
+            return x, y
+
+
+def random_perm(rng):
+    p = list(P_ID)
+    rng.shuffle(p)
+    return tuple(p)
+
+
+def random_word(rng, n, side, calls):
+    ops = []
+    for _ in range(calls):
+        tws = []
+        for _ in range(n):
+            p = random_perm(rng)
+            q = random_perm(rng)
+            tws.append((p, P_ID) if side == "left" else (P_ID, q))
+        pre = []
+        for _ in range(rng.randint(0, 2)):
+            d, s = rng.sample(range(n), 2)
+            pre.append(xor_into(n, d, s))
+        x, y = random_projector(rng, n)
+        ops += pre + [twist(n, tws), paid(n, x, y, random_frame(rng)),
+                      twist(n, [tw_inv(t) for t in tws])] + pre[::-1]
+        if rng.random() < 0.5:
+            d, s = rng.sample(range(n), 2)
+            ops.append(xor_into(n, d, s))
+    return ops
+
+
+def check_one_sided():
+    rng = random.Random(20261023)
+    worst = {"left": 0, "right": 0}
+    violations = {"left": 0, "right": 0, "cross": 0}
+    for side in ("left", "right"):
+        for _ in range(EXPECTED["random_words_per_side"]):
+            n = rng.choice((3, 4))
+            k = rng.randint(1, 4)
+            sz = sz_matrix(product(n, random_word(rng, n, side, k)))
+            rk = flattened_rank(sz, side)
+            worst[side] = max(worst[side], rk - k)
+            if rk > k:
+                violations[side] += 1
+            other = "right" if side == "left" else "left"
+            if flattened_rank(sz, other) > k:
+                violations["cross"] += 1
+    check(violations["left"] == 0 and violations["right"] == 0, "one-sided flattening exceeded call count")
+    check(violations["cross"] > 0, "wrong-side flattening control never exceeded call count")
+    print("one-sided lemma: %d random words per side, flattened rank <= calls; wrong flattening exceeds on %d words"
+          % (EXPECTED["random_words_per_side"], violations["cross"]))
+
+
+SW = ((1, 0, 2), (1, 0, 2))  # simultaneous swap of address axes 0 and 1
+
+
+def witness_calls(private_twist=SW):
+    calls = [("J", None)] + [(kind, s) for s in range(3) for kind in ("P", "D")]
+
+    def ops_for(call):
+        kind, s = call
+        if kind == "J":
+            return [paid(3, (1, 1, 1), (1, 1, 1), unit(0, 0))]
+        e = tuple(int(r == s) for r in range(3))
+        if kind == "D":
+            return [paid(3, e, e, unit(2, 2))]
+        tws = [TW_ID if r == s else private_twist for r in range(3)]
+        return [twist(3, tws), paid(3, (1, 1, 1), e, unit(1, 1)), twist(3, [tw_inv(t) for t in tws])]
+    return calls, ops_for
+
+
+def check_witness():
+    ident_target = target([C1, C1, C1], 3)
+    want = sz_matrix(ident_target)
+    calls, ops_for = witness_calls()
+    check(len(calls) == EXPECTED["witness_calls"], "witness length")
+    orders = exact = 0
+    for order in itertools.permutations(range(len(calls))):
+        ops = [op for idx in order for op in ops_for(calls[idx])]
+        t = product(3, ops)
+        orders += 1
+        check(sz_matrix(t) == want, "witness order disagrees with target in square-zero quotient")
+        if t == ident_target:
+            exact += 1
+    check(orders == EXPECTED["witness_orders"], "witness order count")
+    check(exact == EXPECTED["witness_exact_orders"], "witness exact-order count")
+    check(flattened_rank(want, "left") == 9 and flattened_rank(want, "right") == 9, "witness flattened ranks")
+    # Controls: a different target, or untwisted private calls, break the relaxation match.
+    base = [op for c in calls for op in ops_for(c)]
+    check(sz_matrix(product(3, base)) != sz_matrix(target(TARGETS, 3)), "altered-target control passed")
+    calls0, ops0 = witness_calls(private_twist=TW_ID)
+    check(sz_matrix(product(3, [op for c in calls0 for op in ops0(c)])) != want, "untwisted control passed")
+    callsL, opsL = witness_calls(private_twist=((1, 0, 2), P_ID))
+    check(sz_matrix(product(3, [op for c in callsL for op in opsL(c)])) != want, "left-only twist control passed")
+    print("two-sided witness: %d calls, all %d orders match the target mod square-zero, %d exact"
+          % (len(calls), orders, exact))
+
+
+def main():
+    check_direct()
+    check_one_sided()
+    check_witness()
+    print("PASS bit-address-twist-register-floor")
+
+
+if __name__ == "__main__":
+    main()