diff --git a/research/restored-helper-compression/PROOF.md b/research/restored-helper-compression/PROOF.md
new file mode 100644
index 0000000000..2f2a51dbca
--- /dev/null
+++ b/research/restored-helper-compression/PROOF.md
@@ -0,0 +1,180 @@
+# Compress restored helpers by their paired scalar rank
+
+Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0.
+This is a scoped written proof, not proof-kernel verification.
+
+## 1. Exact statement
+
+Use the scalar-idempotent model of #468 and #288. Address exponents belong
+to a torsion-free abelian group; the coefficient field remains F_2. There
+are k factors
+
+\[
+ D_j=I+a_jx_jy_j^T,\qquad a_j=[A_j]-1\ne0,\qquad
+ x_j,y_j\in\mathbb F_2^{t+r},\quad y_j^Tx_j=1.
+\]
+
+The exact whole-matrix endpoint is
+
+\[
+ P=\prod_jD_j=\operatorname{diag}(d_1,\ldots,d_t,I_r),
+ \qquad d_i-1\ne0.                                             \tag{1}
+\]
+
+In the multiplication model, d_i=[C_i] for nonzero C_i; invertibility of
+the address targets is sufficient but unnecessary for this result. Every
+helper returns to identity on arbitrary inputs. Correctness only on
+zero-initialized ancillas is a different hypothesis.
+
+Write X=(x_1 ... x_k)=[B;U] and Y=(y_1 ... y_k)=[C;V], where B,C
+have t data rows and U,V have r helper rows. Put
+
+\[
+ u=\operatorname{rank}_{\mathbb F_2}U,\quad
+ v=\operatorname{rank}_{\mathbb F_2}V,\quad
+ w=\operatorname{rank}_{\mathbb F_2}(V^TU).
+\]
+
+**Theorem.** Another exact word has the same k frames in the same order,
+the same data components B,C of every scalar projector, and endpoint
+diag(d_1,...,d_t,I_w), with
+
+\[
+ u+v\le k-t,\qquad
+ w\le\min(u,v)\le\left\lfloor\frac{k-t}{2}\right\rfloor.          \tag{2}
+\]
+
+It preserves every scalar pairing y_i^T x_j. Among realizations preserving
+B,C and all these pairings, w is the least helper dimension. This is not
+the least helper count among every possible word for the endpoint.
+There is no restriction on address dimension, frame span, target flags,
+or target commutativity. Original rank-one address frames stay unchanged.
+
+## 2. Call surplus bounds the helper spans
+
+The finitely generated exponent subgroup is free abelian, so its binary
+group algebra is a Laurent polynomial domain. Work over its fraction
+field K. The inherited ordered-product factorization is
+
+\[
+ P-I=XHY^T,                                                     \tag{3}
+\]
+
+where H is upper triangular with nonzero diagonal a_1,...,a_k. Its i,j
+entry sums the increasing call paths from i to j. Each path coefficient
+depends only on the a_l and scalar contractions y_p^T x_q. Thus H is
+invertible over K. This is the rank factorization of #468 and the retained
+arbitrary-register treatment in `research/bit-dirty-auxiliary-registers`.
+
+By (1), P-I has rank t and its column and transposed row spaces equal the
+data-coordinate subspace E. Therefore E lies in the column spaces of X
+and Y. The inclusions hold over F_2 as well as K: adjoining the binary
+basis of E does not increase rank, and binary matrix ranks do not change
+under field extension. Projecting these spaces to helper coordinates gives
+
+\[
+ \operatorname{rank}X=t+u,\qquad\operatorname{rank}Y=t+v.
+\]
+
+Sylvester's rank inequality applied to XH and Y^T now gives
+t>=t+u+t+v-k, proving u+v<=k-t. The remaining inequalities in (2)
+are matrix-rank bounds. Nonidentity helper endpoints would raise rank(P-I)
+and invalidate this particular surplus calculation.
+
+## 3. The construction preserves the entire endpoint
+
+Let W=im U and W_0=W intersect ker(V^T). Choose an r-by-w binary matrix S
+whose columns form a complement of W_0 in W. Choose Q:F_2^r -> F_2^w
+vanishing on W_0 with QS=I_w, first on W and then by extending a basis.
+For each column of U, U-SQU belongs to W_0. Therefore
+
+\[
+ V^TSQU=V^TU.                                                   \tag{4}
+\]
+
+Set U_hat=QU, V_hat=S^TV, X_hat=[B;U_hat], Y_hat=[C;V_hat]. Then
+
+\[
+ Y_{\rm hat}^TX_{\rm hat}=C^TB+V^TSQU=Y^TX.                    \tag{5}
+\]
+
+In particular each new self-pairing is one, so all new scalar projectors
+remain rank one and idempotent. All ordered path coefficients agree and
+the same H gives P_hat-I=X_hat H Y_hat^T.
+
+The original endpoint has BHV^T=0, UHC^T=0 and UHV^T=0. The new upper
+cross block is BHV^TS, the lower cross block is QUHC^T, and the helper
+block minus identity is QUHV^TS. They all vanish; the data block BHC^T
+is unchanged. This proves exact identity on arbitrary new helper inputs,
+not only equality of a data block. When w=0 the same calculation removes
+all helpers. Nonzero U,V may have V^TU=0, so their separate dimensions
+alone do not determine how many helpers survive.
+
+## 4. Executable factorization, cost and precise optimality
+
+Form the k-by-k binary matrix G=V^TU and select w independent columns,
+with indices j_1,...,j_w. Take S to be those columns of U. For each j,
+express G[:,j] uniquely in the selected column basis; use these coordinates
+as column j of U_hat. Row l of V_hat is the transpose of G[:,j_l].
+This is precisely the quotient construction above, without constructing
+an arbitrary ambient extension of Q.
+
+Direct binary inner products cost O(r k^2); elimination and all coordinate
+solves cost O(k^3). Input and temporary storage use O(rk+k^2) bits. These
+are finite preprocessing costs, not recursive-query savings. The generated
+word executes k calls with unchanged frames and order. Its scalar vectors
+are specified directly in the retained formal alphabet; no physical
+register-basis change is granted for free. Separately charged scalar
+mixings, routing, allocation, native operations and cleanup need their own
+implementation bill.
+
+Any h-helper realization preserving B,C and all pairings factors the same
+G as V_new^T U_new, so h>=rank G=w. This proves the stated optimality.
+The invariant bound (2) can be attained: t coordinate data calls and p
+independent helper-only cancelling pairs give k=t+2p and w=p. Reassigning
+or deleting those pairs can use a different number of helpers, but changes
+the preservation contract; no universal need for p helpers is claimed.
+
+## 5. The outstanding five-call block becomes a one-helper question
+
+The merged `research/bit-span4-auxiliary-structure` (#4118) leaves a
+five-call, three-data-target, two-dimensional address block with auxiliary
+registers. Its arbitrary nonidentity-helper-endpoint question remains
+broader than this theorem. For the **exactly restored** helper subcase,
+k=5,t=3 give w<=1. Thus a counterexample with any number of restored
+helpers exists if and only if one exists with at most one restored helper;
+untouched extra coordinates give the converse.
+
+The predecessor `research/three-register-no-target-flag` (#720) excludes
+zero helpers. Citing that result, the remaining restored-helper case has
+four scalar registers. Its alphabet has 120 binary rank-one idempotents,
+versus 28 on three registers. The naive five-call domain has
+120^5=24,883,200,000 ordered words. No such census is performed here, and
+rational address realizability and relation-lattice obligations remain.
+For eight calls and three nonidentity data targets, at most two restored
+helpers suffice, independently of address span.
+
+This reduces an unbounded register-count question to bounded dimension.
+It supplies no five-call construction and no new paid-call lower bound.
+
+## 6. Evidence and limits
+
+The verifier checks every pair of two-by-three binary helper matrices
+(4,096 cases), formal words with nested inverses, paired-rank sharpness,
+and a zero-pairing case with both helper spans nonzero. Controls challenge
+corrupted pairings, invalid projectors, missing restoration and incorrectly
+counted identity targets. These finite checks corroborate the universal
+proof; they do not infer it by extrapolation.
+
+Credit Ali Romman's #468 and eumemic's #288 model/factorization, waynenilsen's
+arbitrary-register domain/rank treatment, David Govea's #720 zero-helper
+result, and unpaidmoon's #4118 open block question. Classical rank inequalities
+and bilinear-space quotients are not claimed as new. The contribution is
+this complete-endpoint compression and the explicit call-surplus bound.
+SOURCES.json pins the exact canonical source notes and original task card.
+
+**No new κ.** Zero-initialized-only ancillas, nonidentity helper endpoints,
+approximate identities, other scalar alphabets, interposed free address
+maps, physical/native tariffs and complete multiplication admission are
+outside scope. All five selected assumptions remain; no human or formal
+proof-kernel acceptance is claimed.
diff --git a/research/restored-helper-compression/README.md b/research/restored-helper-compression/README.md
new file mode 100644
index 0000000000..d24a16ee5b
--- /dev/null
+++ b/research/restored-helper-compression/README.md
@@ -0,0 +1,181 @@
+# Compress restored helpers without changing the paid word
+
+**Result:** an exact `k`-call scalar-idempotent word with `t` nonidentity
+data targets and any number of exactly restored helpers can be realized
+with
+
+\[
+ w=\operatorname{rank}_{\mathbb F_2}(V^TU)
+ \le\left\lfloor\frac{k-t}{2}\right\rfloor
+\]
+
+helpers, while preserving every paid frame, call order, data component of
+every scalar vector, and scalar pairing. Here `U,V` are the helper parts
+of the call vectors `x_j,y_j`. The data endpoint is unchanged, and all
+new helper registers return to identity on arbitrary inputs.
+
+For three nonidentity data targets and five calls, **at most one restored
+helper suffices**. Thus arbitrary restored-helper populations do not add
+another width parameter to that five-call question. Citing David Govea's
+[PR #720](https://github.com/CrocSwap/integer-mult-bounds/pull/720), which
+excludes the zero-helper case for three invertible `2x2` targets, the
+remaining restored-helper case uses four scalar registers. This is a
+width reduction, not a new five-call construction or paid-call lower
+bound. It changes no kappa, selected supplier, or retained assumption.
+
+## Model and proof
+
+A paid call is `I+([A_j]-1)x_j y_j^T`, over the binary group algebra of a
+torsion-free additive exponent group. The coefficient `[A_j]-1` is
+nonzero; `x_j,y_j` are binary vectors with `y_j^T x_j=1`. The endpoint is
+an equality of whole matrices:
+
+```
+product = diag(d_1,...,d_t,I_r),    d_i != 1.
+```
+
+Correctness only on zero-initialized ancillas is insufficient. Arbitrary
+nonidentity helper endpoints are also outside this surplus bound.
+Original rational rank-one address frames remain unchanged. No target
+flag, frame-span restriction, target commutativity or fixed address
+dimension is needed.
+
+[PROOF.md](PROOF.md) gives the complete argument. The ordered product has
+`P-I=X H Y^T`, with invertible triangular `H` over the Laurent fraction
+field. Because the endpoint update has precisely the data-coordinate
+column and row spaces, `rank X=t+rank U` and `rank Y=t+rank V`.
+Sylvester's inequality gives `rank U+rank V<=k-t`.
+
+The compression quotients the span of the helper `x` components by the
+directions invisible to all helper `y` components. It changes both sides
+of the pairing together. This preserves all scalar contractions and
+therefore the same ordered-product matrix `H`. Fixed left and right
+projections then carry each zero data/helper cross block and the zero
+helper update block to zero. Consequently the proof establishes the
+whole new endpoint, not just its data block.
+
+An arbitrary nonminimal replacement that preserves pairings can introduce
+new helper output terms. The proof uses its particular quotient projections;
+[REVIEW.md](REVIEW.md) gives an exact counterexample to omitting that step.
+
+The number `w` is **minimal under the stated preservation contract**:
+any smaller realization of all the same pairings would factor the same
+matrix `V^TU` through fewer than its rank dimensions. It need not be the
+minimum helper count among every possible word for the endpoint.
+
+## Constructor and its preconditions
+
+[compress.py](compress.py) exposes
+
+```python
+smaller_calls, helper_count = compress_calls(calls, data, registers)
+```
+
+Pass a finite list or tuple of calls. Each call is `(frame, x_mask, y_mask)`. The masks encode binary vectors;
+the frame is retained unchanged. The constructor validates scalar
+idempotence and dimensions, and computes a rank factorization of the
+helper pairing matrix. It accepts opaque frames and does **not** certify
+the old endpoint, nonzero address coefficients, or the count of
+nonidentity data targets. Those hypotheses must be established before
+applying the call-surplus bound. In particular, a zero-address call can
+have a nonzero scalar pairing while its formal operation is identity.
+
+The reference bit-operation cost is `O(r k^2+k^3)` and storage is
+`O(rk+k^2)`. This is preprocessing for a word in the formal alphabet;
+it is not a physical register-allocation or native-mixing invoice.
+
+A nontrivial zero-helper example is
+
+```
+t=1, r=2:
+(E11, 1, 1), (E22, 3, 5), (-E22, 3, 5).
+```
+
+Both original helper spans have dimension one, but they pair to zero.
+The constructor removes both helpers, preserves the three frames and
+data components, and keeps the endpoint `diag([E11],I_2)` on the original
+roles and `[E11]` on the compressed data role. The verifier also supplies
+examples with both helper spans of dimension two but paired rank one,
+and examples attaining the `floor((k-t)/2)` bound.
+
+## Reproduction and exact evidence
+
+From the repository root:
+
+```sh
+python3 -I -W error -B research/restored-helper-compression/verify.py
+python3 -I -O -W error -B research/restored-helper-compression/verify.py
+python3 -B scripts/research_package.py --package research/restored-helper-compression --check-only
+python3 -B scripts/research_package.py --package research/restored-helper-compression
+```
+
+[verify.py](verify.py) uses only the standard library. Its rank oracle
+explicitly enumerates binary spans, independently of the kernel's
+elimination. Its endpoint oracle multiplies matrices in the exact formal
+binary group algebra, without using the proof's `X H Y^T` factorization.
+
+| Check | Executed scope |
+| --- | --- |
+| Binary helper factorization | All 4,096 pairs of `2x3` binary helper matrices |
+| Paired-rank distribution | Rank zero: 274; rank one: 2,058; rank two: 1,764 |
+| General data-block identity | 64 predetermined legal three-call words, without assuming restored endpoints |
+| Structured restored words | 16 cases, including sharpness, zero paired rank, two-sided invisible directions, a mixed nonadjacent commutator and a no-data cancellation |
+| Nested inverse words | 64 bounded words with random rank-one `2x2` integer frames, seed `2026110617` |
+| Rejection controls | Corrupted pairing, invalid idempotence, nonidentity helper output, counted identity data target, mutated cleanup frame, zero address update, and preservation of self-pairings alone |
+| Separate review implementation | 448 factorizations through 65 helper bits; 181 complete Laurent-matrix words; 121 strict reductions; six counterexamples to broader claims |
+
+The unrestored control is particularly direct: with `t=1,r=1`, calls
+`(E11,1,1),(E22,2,2)` have paired helper rank one, whereas
+`floor((k-t)/2)=0`. Their helper endpoint is `[E22]`, so they do not
+satisfy the theorem. A zero-address helper call and an incorrectly
+counted identity data target provide separate failures of other premises.
+
+The primary normal and optimized modes print
+`PASS_RESTORED_HELPER_COMPRESSION`. The separately implemented
+[independent.py](independent.py) prints
+`PASS_C_INDEPENDENT_COMPRESSION_REVIEW` in both modes and reports the
+reviewed proof and constructor hashes. It uses its own rectangular binary
+elimination and one-variable Laurent matrix oracle. The review was not
+blind; the mathematical argument and code were supplied to the reviewer. These are finite corroborating
+controls. The universal statement rests on the written proof. No
+`120^5` word census or predecessor search engine is run.
+
+[VERIFY.json](VERIFY.json) declares a self-contained replay.
+[SOURCES.json](SOURCES.json) pins the cited sources as provenance; none
+is a live scientific input to the verifier. The shared selected-baseline
+attempt was blocked by a missing checkpoint certificate in the sparse
+lead checkout. No selected-baseline PASS or full selected replay is
+claimed here.
+
+## Open next questions
+
+1. Decide the four-register, five-call case for three invertible `2x2`
+   targets, span three, and one restored helper. Begin with exact scalar
+   symmetries and the two-relation/address-realizability conditions. The
+   raw `120^5 = 24,883,200,000` ordered words are not a finished search
+   plan. The broader arbitrary-nonidentity-helper question in
+   [PR #4118](https://github.com/CrocSwap/integer-mult-bounds/pull/4118)
+   remains outside this application.
+2. Determine whether retaining only the contractions needed by increasing
+   call paths permits a smaller realization than the rank of the full
+   pairing matrix. Any proposed reduction still has to preserve legal
+   scalar idempotence and every endpoint block; matching self-pairings
+   alone fails an explicit control.
+
+The complete original seed-68 card and scope refinement are retained in
+[TASK.json](TASK.json). This package supplies no native implementation,
+physical cleanup tariff, supplier admission, complete multiplication
+result, human acceptance, or proof-kernel verification.
+
+## Credit and license
+
+Prepared for **@CubeJerry** with substantial OpenAI Codex assistance,
+including separate proof/kernel and independent verifier work. New work
+is **Apache-2.0**. Credit eumemic's #288 model; Ali Romman's #468 ordered
+rank factorization; waynenilsen's arbitrary-register dirty-auxiliary
+arguments; David Govea's #720 zero-helper result; and unpaidmoon's #4118
+remaining block question. The source metadata confirms the #720 and
+#4118 attributions. Classical rank inequalities and bilinear quotients
+are not claimed as new. The contribution is the preservation of the
+complete restored endpoint together with the explicit call-surplus
+bound and its bounded-width application.
diff --git a/research/restored-helper-compression/REVIEW.md b/research/restored-helper-compression/REVIEW.md
new file mode 100644
index 0000000000..db4586237d
--- /dev/null
+++ b/research/restored-helper-compression/REVIEW.md
@@ -0,0 +1,237 @@
+# Independent review of restored-helper compression
+
+Reviewer: Worker C for @CubeJerry, with substantial OpenAI Codex assistance.
+Apache-2.0. Review completed 2026-11-06, before the 04:35 UTC deadline.
+This is a separate AI-assisted mathematical/code review with finite exact
+checks. The review was not blind: the reviewer received the proposed theorem,
+proof, constructor, and review targets. It is not independent human peer review or proof-kernel verification.
+
+## Conclusion
+
+**No blocking mathematical or constructor defect found in the stated scope.**
+The full-endpoint quotient argument is valid, the descent to binary column
+spaces is justified, and the exact bound is
+
+\[
+u+v\le k-t,\qquad
+w=\operatorname{rank}_{\mathbb F_2}(V^TU)
+\le\min(u,v)\le\left\lfloor\frac{k-t}{2}\right\rfloor.
+\]
+
+The constructor realizes the particular quotient needed by the proof. Its
+output preserves the entire restored-helper endpoint, not only the data
+block. The optimality claim is correctly restricted to fixed data components
+and all scalar pairings. The result applies to the exactly restored helper
+subcase of #4118; it does not settle that predecessor's more general arbitrary
+diagonal helper endpoints or its remaining five-call existence question.
+
+The reviewer did not edit the package. These are the reviewed proof and constructor bytes:
+
+| File | Bytes | SHA256 |
+|---|---:|---|
+| `PROOF.md` | 8,281 | `4d9edf19ed4eec2708cbfcd186e9d6085af43cc0213e14fb2bd54efdeda2a20b` |
+| `compress.py` | 2,685 | `47b702b79f454a3aa86adf13edac807e7f3fddc286f83d737f3c1c8ea745075c` |
+
+Both paths are in this package.
+Later edits require comparison with this reviewed version.
+
+## 1. Fraction field, binary descent and the exact surplus
+
+For the finite set of exponents used by the word, the generated torsion-free
+abelian group is free abelian. Its binary group algebra is a Laurent polynomial
+domain. Passing to its fraction field therefore preserves the nonzero
+diagonal entries `a_j` of the ordered-path matrix `H`; `H` is invertible.
+The fixed ordering supplies an upper triangular `H` with
+`P-I=X H Y^T`. The entries use only the unchanged coefficients `a_j` and the
+scalar contractions `y_i^T x_j`.
+
+The endpoint makes the column and transposed row spaces of `P-I` exactly the
+data-coordinate space `E`, of dimension `t`. Every `d_i-1` must be nonzero;
+the target frames need not share a flag or commute as rational matrices.
+
+The written rank-invariance descent to `F_2` is sound. An independent way to
+see the same step is to take a binary row `z^T` with `z^T X=0`. Then
+`z^T(P-I)=0`, so `z_i(d_i-1)=0` for every data coordinate. Because `z_i` is
+binary and `d_i-1` is nonzero, all data coordinates of `z` vanish. Thus
+`ker(X^T)` is contained in `E^perp` over `F_2`, and `E` is contained in the
+binary image of `X`. Applying the transposed argument gives the same inclusion
+for `Y`. No field-dependent scalar mixing has been silently introduced.
+
+The helper projection of `im X` has image `im U` and kernel exactly `E`,
+giving `rank X=t+u`; similarly `rank Y=t+v`. Sylvester's inequality over the
+fraction field yields
+
+`t = rank(X H Y^T) >= (t+u)+(t+v)-k`.
+
+Therefore `u+v<=k-t`. Combining `w<=min(u,v)` with
+`2 min(u,v)<=u+v` gives the stated floor, without an off-by-one issue. This
+also implies `t<=k`. The proof handles zero helper width and zero paired rank.
+
+## 2. Why the quotient preserves the whole endpoint
+
+On `W=im U`, take the kernel `W_0=W intersect ker(V^T)` and a complement
+with basis matrix `S`. Its dimension is exactly `w=rank(V^TU)`. A map `Q`
+annihilating `W_0` and satisfying `QS=I_w` exists; extending it outside `W`
+is harmless. For every original helper column,
+`U-SQU` lies in `W_0`, so `V^T S Q U=V^T U`.
+
+Consequently the new vectors preserve all scalar pairings, including the
+self-pairings equal to one. Each new projector remains a nonzero binary
+rank-one idempotent, with the same address frame. The ordered-path matrix
+`H` is therefore unchanged.
+
+For a compact independent full-endpoint check, set
+
+`R=diag(I_t,Q)` and `T=diag(I_t,S)`.
+
+Then `RT=I`, `X_hat=RX`, `Y_hat^T=Y^T T`, and
+
+`P_hat-I = R(P-I)T`, hence `P_hat=RPT`.
+
+For `P=diag(D,I_r)`, this is exactly `diag(D,I_w)`. This verifies all cross
+blocks and the helper identity at once. It is an algebraic proof of a newly
+specified word, not permission to discard live helpers while executing the
+old word or to implement physical basis changes without a charge.
+
+Preserving pairings alone for an arbitrary replacement realization would
+not justify this conclusion. An explicit counterexample appears below. The
+particular quotient, or an equivalent minimal factorization, is substantive.
+
+## 3. Constructor and minimality
+
+`factor_helpers` forms the Gram columns `G=V^T U`. The selected independent
+columns of `G` correspond to independent original columns of `U`: any relation
+among the latter would also be a relation among their images. The selected
+columns therefore give a valid `S` complement. The returned left coordinates
+define `Q` on `im U`, because every relation among columns of `U` is also a
+relation among their Gram columns. The returned right coordinates are exactly
+`S^T V`. Thus the implementation follows the proof's quotient, rather than
+merely returning an unchecked pairing-preserving replacement.
+
+I checked the bit-mask indexing and the incremental column-basis coordinate
+algorithm. Pivots retain coordinates in the original selected basis; dependent
+columns do not advance the basis index. Empty and all-zero Gram matrices give
+width zero. `compress_calls` retains frames and both data components in call
+order, and checks the binary self-pairings before construction.
+
+Any realization with `h` helpers preserving the data components and all
+pairings must factor the same `G` as `V_new^T U_new`, so `h>=rank G=w`.
+The quotient attains this bound with the required endpoint. This is precisely
+the claimed restricted optimum. It is not an unrestricted lower bound on
+helpers for all words implementing the endpoint.
+
+The constructor is not an endpoint or theorem-precondition validator. In
+particular it does not test nonzero address frames, the full restored endpoint,
+or which data targets are nonidentity. This is consistent with its stated
+separate-check contract. Those conditions must be established before its
+returned width is compared with the surplus bound. The zero-frame control
+below makes that boundary explicit.
+
+## 4. Exact counterexamples to stronger claims
+
+Let `D(a,x,y)=I+(z^a-1)xy^T` in `F_2[z,z^{-1}]`; coordinate indices start
+at zero. All vectors below have self-pairing one. These examples were checked
+by direct Laurent matrix multiplication, independently of `H`.
+
+1. **Allowing nonidentity helper endpoints invalidates the width bound.**
+   Take one data register and one helper, with calls
+   `D(1,e0,e0), D(1,e1,e1)`. The endpoint is `diag(z,z)`;
+   `k=2,t=1,u=v=w=1`. Thus `w=1>floor((k-t)/2)=0`.
+   The same word is correct on zero helper input and returns that input to
+   zero, so zero-initialized-only correctness does not rescue the bound.
+
+2. **Zero-input correctness can violate the stronger span inequality even
+   with an identity helper diagonal.** One call with `x=e0`, `y=e0+e1`
+   gives `[[z,z-1],[0,1]]`. Its action on `(data,0)` is `(z data,0)`, but
+   `u+v=1>k-t=0`. The missing hypothesis is the zero upper cross block on
+   arbitrary dirty input.
+
+3. **Identity targets cannot be counted in `t`.** The helper-only inverse
+   pair `D(1,e1,e1),D(-1,e1,e1)` has endpoint `I_2`, but if the identity
+   data coordinate were counted as `t=1`, it would give `w=1>0` again.
+
+4. **Zero frames cannot be retained when applying the surplus inequality.**
+   The calls `D(2,e0,e0),D(0,e1,e1)` have endpoint `diag(z^2,1)` and paired
+   helper rank one, violating the putative `k=2,t=1` bound. The second call
+   has `a_j=0` and is explicitly outside the theorem. This illustrates why
+   constructor output alone is not a certificate of the width bound.
+
+5. **Arbitrary nonminimal pairing-preserving replacements can change the
+   full endpoint.** Start from
+   `D(3,e0,e0),D(1,e1,e1),D(-1,e1,e1)`, whose endpoint is `diag(z^3,1)`.
+   In a three-register realization replace only the last `x` by `e1+e2`.
+   Every data component and every scalar pairing is unchanged. The new
+   endpoint has helper block `[[1,0],[z^-1-1,1]]`, not `I_2`. The quotient
+   construction avoids this unpaired direction.
+
+6. **Paired rank is not an unrestricted helper lower bound.** The original
+   word in the preceding example has `w=1`. Moving both adjacent cancelling
+   calls onto `e0` gives the same endpoint `z^3` with no helper, the same
+   frames and order, but different data components and pairings. This is
+   excluded by the stated optimality contract.
+
+An additional positive edge case uses the word
+`D(3,e0,e0),D(1,e0+e1,e0+e2),D(-1,e0+e1,e0+e2)`.
+Both original helper spans have rank one, while `V^T U=0`; the constructor
+removes both helpers and preserves the exact endpoint. This rules out
+substituting separate span ranks for the paired rank.
+
+## 5. Scope against the retained predecessors
+
+I read the retained READMEs for `bit-dirty-auxiliary-registers`,
+`bit-span4-auxiliary-structure` (#4118), and
+`three-register-no-target-flag` (#720), and checked all three SHA256 and Git
+blob hashes against the current package's `SOURCES.json`. This checks context
+bytes, not the complete predecessor proofs or finite engines.
+
+The dirty-auxiliary model explicitly permits arbitrary diagonal monomial
+helper endpoints; #4118 inherits that broader setting. Its five-call,
+three-data-target, two-dimensional address block is therefore not generally
+reduced to one helper by the new theorem. For **exact restoration**, however,
+`k=5,t=3` gives `w<=1`. The frames, their span and their rational realizability
+are unchanged. #720's six-call result for exactly three scalar registers
+excludes zero helpers under its cited hypotheses, leaving the four-register
+case. The 120-projector count and `120^5=24,883,200,000` ordered-word count
+are correct. No such census was run in this review.
+
+For `k=8,t=3`, the restored-helper reduction to at most two helpers also
+follows. Neither consequence proves a new paid-call lower bound, solves the
+remaining address relation obligations, establishes a physical implementation,
+or changes the selected result or its five assumptions.
+
+## 6. Independent executed evidence
+
+The separate checker is [independent.py](independent.py). Its packaged copy
+changes only the package locator from the original review workspace to its own
+directory; no mathematical or test logic was changed.
+It uses the Python standard library, a separately written rectangular binary
+elimination, and direct sparse Laurent matrix multiplication. It does not
+import the package's verifier or use the ordered-path identity as its endpoint
+oracle. The constructor is loaded from source bytes without bytecode writes.
+
+Under CPython 3.12.14, both commands passed with byte-identical JSON output:
+
+```sh
+python3 -I -W error -B research/restored-helper-compression/independent.py
+python3 -I -O -W error -B research/restored-helper-compression/independent.py
+```
+
+Marker: `PASS_C_INDEPENDENT_COMPRESSION_REVIEW`; seed `2026110655`.
+
+| Independent check | Count |
+|---|---:|
+| Arbitrary helper factorizations, through 65 helper bits and 13 calls | 448 |
+| Exact full-endpoint words | 181 |
+| Strict reductions in helper dimension among those words | 121 |
+| Explicit counterexamples to stronger claims | 6 |
+
+The restored words include products in arbitrary binary scalar bases,
+coordinate helper inverses, additional idle helper coordinates mixed by an
+independent helper basis, and the zero-paired-rank example. The generated
+original and compressed whole matrices, all scalar pairings, frames, data
+parts, paired ranks and applicable surplus inequalities were checked.
+
+The original normal and optimized receipts were compared during review.
+Their executed counts and reviewed source hashes are retained above. The packaged
+checker emits a fresh receipt containing the proof and constructor hashes. The universal conclusion rests on the written argument
+audited above; these finite cases corroborate it without extending its scope.
diff --git a/research/restored-helper-compression/SOURCES.json b/research/restored-helper-compression/SOURCES.json
new file mode 100644
index 0000000000..5fd7c3aeed
--- /dev/null
+++ b/research/restored-helper-compression/SOURCES.json
@@ -0,0 +1,61 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bit-dirty-auxiliary-registers/README.md",
+      "usage": "provenance",
+      "git_blob": "273bb963ee40869145cf8309db4f8dddebcfe43d",
+      "sha256": "da984fddaa09bfa7b1a3e11505e737283cee36e7972b2081f9de28ec420607cd"
+    },
+    {
+      "path": "research/bit-span4-auxiliary-structure/README.md",
+      "usage": "provenance",
+      "git_blob": "b22887c72ff33e6c9b0d2f809a9f23c60a933581",
+      "sha256": "18209bc77ce7583947f117600fd84ced45f7777d94465155c3ac385eab22a26a"
+    },
+    {
+      "path": "research/three-register-no-target-flag/README.md",
+      "usage": "provenance",
+      "git_blob": "290bfb79db5f4177b8b03bc2027c3848671fac9e",
+      "sha256": "95d4483da9b19df051c7d13fe290eefb82da019ab4be8e66ad9216199ddda4eb"
+    },
+    {
+      "path": "research/bit-three-register-lower-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
+      "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
+    },
+    {
+      "path": "research/bit-span4-auxiliary-structure/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "84833a7ef6711c2db9a7af8150e690fb03f9ac4c",
+      "sha256": "58f95c1fbe14cfec8b5d772fec7cc6a1ac6d603f3e1cec2d2ec6178b79444f7f"
+    },
+    {
+      "path": "research/community-efficient1800-audit/DISPOSITIONS.json",
+      "usage": "provenance",
+      "git_blob": "acf1582c979eb1d21d8605015d816bf3f8a68877",
+      "sha256": "b5654865e30ea1bc9e2c9e20b97e168d5e7f2172e9a50b3e6a6352579e6a054b"
+    },
+    {
+      "path": "docs/research/pr-intake-decisions.json",
+      "usage": "provenance",
+      "git_blob": "c39161eba92dfba20d053f820d2f87889dc3d4b3",
+      "sha256": "c3e06bb20616abb639e7a459f7da797a025549a8f3ec1f4919aa16d3c190132c"
+    }
+  ],
+  "source_note": "All external sources are provenance only. The proof is written self-contained, and the exact verifier reads only package-local code. No predecessor census is replayed or used as executable input. Canonical metadata confirms that the three-register no-target-flag source is David Govea #720, incorporated at head a942c0ae1b463710ca535c1fba1b07b6431b5a86, and that the span-four auxiliary source is unpaidmoon #4118. The zero-helper exclusion in the application is cited to the pinned #720 source, not claimed as a new replay."
+}
diff --git a/research/restored-helper-compression/TASK.json b/research/restored-helper-compression/TASK.json
new file mode 100644
index 0000000000..ea517007b6
--- /dev/null
+++ b/research/restored-helper-compression/TASK.json
@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Compress arbitrary exactly restored helper registers in the scalar-idempotent model to rank_F2(V^T U), at most floor((k-t)/2), while preserving paid frames, order, data components and all scalar pairings.",
+  "scope_change_reason": "The seed-68 register-model card is refined to a proved normalization for larger restored-helper populations. It changes the number of scalar roles allowed in the input word but retains the formal alphabet. This bounds the register dimension needed to study the restored-helper subcase of #4118; it does not repeat the covered GL3 census or produce a new native supplier.",
+  "bottleneck_link": "The result turns an unbounded restored-helper count into a finite-dimensional word question: any five-call three-data counterexample needs at most one restored helper. It supplies no paid-call saving, native implementation, supplier admission or change to kappa.",
+  "budget_minutes": 45,
+  "stop_rule": "Finish the written compression proof, exact binary factorization census, bounded formal endpoint controls and source-bound package. Do not run the full 120^5 word census, claim a five-call construction, or extend the surplus bound to nonidentity helper outputs.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves full-endpoint compression and the call-surplus bound. verify.py independently enumerates binary spans for all 4096 r=2,k=3 helper matrix pairs, checks 64 arbitrary data-block identities, 16 structured restored words, 64 seeded nested-inverse words and seven substantive rejection controls. A separate Worker C checker adds 448 factorizations through 65 helper bits, 181 exact Laurent endpoint words, 121 strict reductions and six explicit overbroad-claim counterexamples; REVIEW.md retains the reviewed proof/kernel hashes.",
+  "author": "@CubeJerry",
+  "ai_assistance": "Substantial OpenAI Codex assistance: lead derivation/proof and compression kernel, Worker A independent mathematical challenge, span-enumeration/formal-group-algebra verifier and package metadata; separate AI cross-review. No independent human or proof-kernel acceptance claimed.",
+  "open_questions": [
+    {
+      "question": "Does a five-call, three-target, rank-one 2x2 address word exist with exactly one restored helper and frame span three?",
+      "why_it_matters": "The new theorem makes this a complete restored-helper width reduction for the remaining #4118 block; the cited #720 result excludes zero helpers.",
+      "first_step": "Work with the 120 four-register idempotents and exact two-relation/address-realizability constraints; derive symmetry or algebraic reductions before a word census.",
+      "blocked_by": "The naive 120^5 domain has 24,883,200,000 ordered words, and this package supplies no construction or exclusion. Nonidentity auxiliary outputs remain outside the restored-helper application."
+    },
+    {
+      "question": "Can a smaller helper dimension suffice when preserving only the scalar contractions needed by ordered paths rather than every pairing?",
+      "why_it_matters": "The paired rank is optimal under the stated preservation contract, but need not minimize helper count across all possible words for an endpoint.",
+      "first_step": "Identify the increasing-path contractions in H for one small fixed word and compare exact alternative realizations while checking all endpoint blocks.",
+      "blocked_by": "Preserving self-pairings or the data block alone is insufficient. A weaker invariant must still prove helper restoration and legal idempotence."
+    }
+  ],
+  "original_selection_seed": 68,
+  "assignment_date": "2026-11-06",
+  "baseline_orientation": {
+    "selected_pr": 6030,
+    "selected_kappa": "781451/250000000",
+    "admitted_BIT": "0.0034",
+    "binding_track": "complex",
+    "retained_assumptions": 5,
+    "baseline_command_status": "Shared lead baseline attempt blocked by missing certificates/checkpoints/frontier4359.json in the sparse checkout. No PASS claimed. Selected record and full application review inspected manually by lead; no full selected cold replay was needed or run for this independent formal-model result."
+  },
+  "overlap_coverage": {
+    "checked_sources": [
+      "#468 rank factorization",
+      "arbitrary-register dirty-auxiliary note",
+      "#4118 span-four auxiliary PROOF and open question",
+      "#720 three-register no-target-flag result"
+    ],
+    "new_step": "Quotient by invisible helper directions while preserving every scalar contraction and all clean endpoint blocks; combine with rank(P-I)=t to bound paired helper rank by call surplus.",
+    "coverage_limits": "Targeted source review, not an exhaustive novelty survey. The underlying rank inequality and bilinear quotient are classical. No claimed extension to arbitrary nonidentity dirty-helper endpoints."
+  }
+}
diff --git a/research/restored-helper-compression/VERIFY.json b/research/restored-helper-compression/VERIFY.json
new file mode 100644
index 0000000000..31ba22bde7
--- /dev/null
+++ b/research/restored-helper-compression/VERIFY.json
@@ -0,0 +1,59 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "All 4096 r=2,k=3 binary factorizations with independent span ranks; exact formal whole-matrix endpoints; sharp surplus and zero-pairing controls; 64 seeded nested inverse words; rejection of nonrestoration, identity-data counting, zero updates, pairing and frame mutations, and invalid idempotence."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "The same exact controls with Python assertions disabled; every condition uses explicit exceptions."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Separate Worker C implementation: 448 factorizations through 65 helper bits, 181 complete Laurent-matrix endpoint words, 121 strict dimension reductions, and six counterexamples to overbroad premises or optimality claims."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "The same separate review checker in optimized Python, retaining proof/constructor hash receipts."
+    }
+  ]
+}
diff --git a/research/restored-helper-compression/compress.py b/research/restored-helper-compression/compress.py
new file mode 100644
index 0000000000..5b4560500e
--- /dev/null
+++ b/research/restored-helper-compression/compress.py
@@ -0,0 +1,67 @@
+"""Exact binary paired-rank compression, @CubeJerry/AI, Apache-2.0."""
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def parity(x):
+    return x.bit_count() & 1
+
+
+def column_basis(columns):
+    """Return original basis indices and coordinates of every input column."""
+    pivots, selected = {}, []
+    for index, original in enumerate(columns):
+        value, coefficients = original, 1 << len(selected)
+        while value:
+            top = value.bit_length()-1
+            if top not in pivots:
+                pivots[top] = value, coefficients
+                selected.append(index)
+                break
+            vector, coords = pivots[top]
+            value ^= vector
+            coefficients ^= coords
+    coordinates = []
+    for original in columns:
+        value, coefficients = original, 0
+        while value:
+            top = value.bit_length()-1
+            need(top in pivots, 'Column belongs to selected span')
+            vector, coords = pivots[top]
+            value ^= vector
+            coefficients ^= coords
+        coordinates.append(coefficients)
+    return selected, coordinates
+
+
+def factor_helpers(left, right):
+    """U/V columns are nonnegative bit masks; return compressed columns."""
+    need(len(left) == len(right), 'Matching helper column counts')
+    need(all(type(v) is int and v >= 0 for v in left+right), 'Binary helper vectors')
+    gram = [sum(parity(y & x) << i for i, y in enumerate(right)) for x in left]
+    selected, compressed_left = column_basis(gram)
+    compressed_right = [sum(((gram[j] >> i) & 1) << p for p, j in enumerate(selected))
+                        for i in range(len(right))]
+    return compressed_left, compressed_right, len(selected)
+
+
+def compress_calls(calls, data, registers):
+    """Preserve frames and data parts; endpoint validity is a separate check.
+
+    Calls are (exponent, x_mask, y_mask). The surplus bound applies only
+    when the theorem's full endpoint hypothesis has been established.
+    """
+    need(type(data) is int and type(registers) is int and 0 <= data <= registers,
+         'Data and register dimensions')
+    need(all(type(x) is int and type(y) is int and 0 <= x < 1 << registers
+             and 0 <= y < 1 << registers and parity(x & y) == 1
+             for _, x, y in calls), 'Binary rank-one idempotent projector')
+    left, right = [x >> data for _, x, _ in calls], [y >> data for _, _, y in calls]
+    new_left, new_right, width = factor_helpers(left, right)
+    mask = (1 << data)-1
+    result = [(a, (x & mask) | (u << data), (y & mask) | (v << data))
+              for (a, x, y), u, v in zip(calls, new_left, new_right)]
+    return result, width
diff --git a/research/restored-helper-compression/independent.py b/research/restored-helper-compression/independent.py
new file mode 100644
index 0000000000..7edb1828ad
--- /dev/null
+++ b/research/restored-helper-compression/independent.py
@@ -0,0 +1,249 @@
+"""Independent finite review; no edits to the package under review.
+
+@CubeJerry, with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import hashlib
+import json
+import random
+import types
+from pathlib import Path
+
+PACKAGE = Path(__file__).resolve().parent
+kernel_bytes = (PACKAGE / 'compress.py').read_bytes()
+kernel = types.ModuleType('independent_review_kernel')
+exec(compile(kernel_bytes, str(PACKAGE / 'compress.py'), 'exec'), kernel.__dict__)
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def dot(a, b, width):
+    return sum(((a >> i) & 1) * ((b >> i) & 1) for i in range(width)) % 2
+
+
+def rank(columns, rows):
+    table = [[(c >> i) & 1 for c in columns] for i in range(rows)]
+    pivot = 0
+    for j in range(len(columns)):
+        found = next((i for i in range(pivot, rows) if table[i][j]), None)
+        if found is None:
+            continue
+        table[pivot], table[found] = table[found], table[pivot]
+        for i in range(rows):
+            if i != pivot and table[i][j]:
+                table[i] = [a ^ b for a, b in zip(table[i], table[pivot])]
+        pivot += 1
+    return pivot
+
+
+ZERO, ONE = frozenset(), frozenset({0})
+
+
+def pmul(a, b):
+    result = set()
+    for x in a:
+        for y in b:
+            if x + y in result:
+                result.remove(x + y)
+            else:
+                result.add(x + y)
+    return frozenset(result)
+
+
+def identity(n):
+    return tuple(tuple(ONE if i == j else ZERO for j in range(n)) for i in range(n))
+
+
+def product(a, b):
+    n = len(a)
+    output = [[ZERO for _ in range(n)] for _ in range(n)]
+    for i in range(n):
+        for j in range(n):
+            for k in range(n):
+                output[i][j] ^= pmul(a[i][k], b[k][j])
+    return tuple(tuple(row) for row in output)
+
+
+def endpoint(calls, n):
+    answer = identity(n)
+    for exponent, x, y in calls:
+        factor = [list(row) for row in identity(n)]
+        scalar = frozenset({exponent}) ^ ONE
+        for i in range(n):
+            for j in range(n):
+                if (x >> i) & (y >> j) & 1:
+                    factor[i][j] ^= scalar
+        answer = product(answer, factor)
+    return answer
+
+
+def desired(t, r, exponent):
+    answer = [list(row) for row in identity(t + r)]
+    for i in range(t):
+        answer[i][i] = frozenset({exponent})
+    return tuple(tuple(row) for row in answer)
+
+
+def binary_inverse(rows):
+    n = len(rows)
+    left = rows[:]
+    right = [1 << i for i in range(n)]
+    for j in range(n):
+        i = next(i for i in range(j, n) if (left[i] >> j) & 1)
+        left[i], left[j] = left[j], left[i]
+        right[i], right[j] = right[j], right[i]
+        for i in range(n):
+            if i != j and (left[i] >> j) & 1:
+                left[i] ^= left[j]
+                right[i] ^= right[j]
+    need(left == [1 << i for i in range(n)], 'binary inverse')
+    return right
+
+
+def random_basis(n, rng):
+    rows = [1 << i for i in range(n)]
+    if n > 1:
+        for _ in range(5 * n):
+            i, j = rng.sample(range(n), 2)
+            rows[i] ^= rows[j]
+    return rows, binary_inverse(rows)
+
+
+def all_pairings(calls, n):
+    return [[dot(y, x, n) for _, x, _ in calls] for _, _, y in calls]
+
+
+def check_word(calls, t, r, target):
+    compressed, w = kernel.compress_calls(calls, t, t + r)
+    need(endpoint(calls, t + r) == target, 'original full endpoint')
+    need(endpoint(compressed, t + w) == tuple(tuple(target[i][j]
+         if i < t and j < t else (ONE if i == j else ZERO)
+         for j in range(t + w)) for i in range(t + w)), 'compressed full endpoint')
+    need(all_pairings(calls, t + r) == all_pairings(compressed, t + w), 'all call pairings')
+    mask = (1 << t) - 1
+    need([(a, x & mask, y & mask) for a, x, y in calls] ==
+         [(a, x & mask, y & mask) for a, x, y in compressed], 'frames and data components')
+    left, right = [x >> t for _, x, _ in calls], [y >> t for _, _, y in calls]
+    u, v = rank(left, r), rank(right, r)
+    gram = [sum(dot(x, y, r) << i for i, y in enumerate(right)) for x in left]
+    need(w == rank(gram, len(calls)), 'paired rank width')
+    need(u + v <= len(calls) - t, 'helper surplus rank')
+    need(w <= (len(calls) - t) // 2, 'surplus width')
+    return w
+
+
+def main():
+    rng = random.Random(2026110655)
+    count = {'arbitrary_helper_factorizations': 0, 'full_endpoint_words': 0,
+             'strict_dimension_reductions': 0, 'overbroad_claim_counterexamples': 0}
+    for r in (0, 1, 2, 3, 5, 9, 17, 65):
+        for k in (0, 1, 2, 3, 5, 8, 13):
+            for _ in range(8):
+                left = [rng.getrandbits(r) for _ in range(k)]
+                right = [rng.getrandbits(r) for _ in range(k)]
+                ul, vl, w = kernel.factor_helpers(left, right)
+                need(len(ul) == len(vl) == k, 'column counts')
+                need(all(0 <= z < 1 << w for z in ul + vl), 'compressed bit widths')
+                for i in range(k):
+                    for j in range(k):
+                        need(dot(right[i], left[j], r) == dot(vl[i], ul[j], w), 'pairing factor')
+                gram = [sum(dot(y, x, r) << i for i, y in enumerate(right)) for x in left]
+                need(w == rank(gram, k), 'independent Gram rank')
+                count['arbitrary_helper_factorizations'] += 1
+
+    # A mixed scalar basis resolves z I into rank-one calls. Coordinate
+    # helper inverses restore the helpers. Idle dimensions are then mixed
+    # by an independently generated helper-only basis change.
+    for t in (1, 2, 3):
+        for r in range(5):
+            for core in range(r + 1):
+                for _ in range(4):
+                    n = t + core
+                    basis, inverse = random_basis(n, rng)
+                    exponent = rng.choice((-3, -2, -1, 1, 2, 3))
+                    calls = [(exponent, sum(((basis[i] >> j) & 1) << i for i in range(n)), inverse[j])
+                             for j in range(n)]
+                    calls += [(-exponent, 1 << i, 1 << i) for i in range(t, n)]
+                    change, reverse = random_basis(r, rng)
+                    changed = []
+                    mask = (1 << t) - 1
+                    for a, x, y in calls:
+                        hx, hy = x >> t, y >> t
+                        ux = sum(dot(row, hx, r) << i for i, row in enumerate(change))
+                        vy = sum(dot(sum(((reverse[j] >> i) & 1) << j for j in range(r)), hy, r) << i
+                                 for i in range(r))
+                        changed.append((a, (x & mask) | (ux << t), (y & mask) | (vy << t)))
+                    w = check_word(changed, t, r, desired(t, r, exponent))
+                    need(w == core, 'sharp mixed-basis paired width')
+                    count['full_endpoint_words'] += 1
+                    count['strict_dimension_reductions'] += w < r
+
+    # Both individual helper spans are nonzero, yet the paired width is zero.
+    calls = [(3, 1, 1), (1, 3, 5), (-1, 3, 5)]
+    need(check_word(calls, 1, 2, desired(1, 2, 3)) == 0, 'zero paired rank')
+    count['full_endpoint_words'] += 1
+    count['strict_dimension_reductions'] += 1
+
+    # Nonidentity helpers: exact diagonal endpoint, but the surplus bound fails.
+    calls = [(1, 1, 1), (1, 2, 2)]
+    _, w = kernel.compress_calls(calls, 1, 2)
+    need(endpoint(calls, 2) == desired(2, 0, 1) and w == 1 and w > (len(calls)-1)//2,
+         'nonidentity-helper counterexample')
+    count['overbroad_claim_counterexamples'] += 1
+
+    # Correct on zero helper input, including its return to zero; full
+    # matrix restoration is absent. Even the u+v surplus statement fails.
+    calls = [(1, 1, 3)]
+    need(endpoint(calls, 2) == ((frozenset({1}), frozenset({0, 1})), (ZERO, ONE)),
+         'zero-input-only endpoint')
+    need(rank([0], 1) + rank([1], 1) > len(calls)-1, 'zero-input-only rank violation')
+    count['overbroad_claim_counterexamples'] += 1
+
+    # Counting an identity target as nonidentity makes the claimed width false.
+    calls = [(1, 2, 2), (-1, 2, 2)]
+    _, w = kernel.compress_calls(calls, 1, 2)
+    need(endpoint(calls, 2) == identity(2) and w == 1 and w > (len(calls)-1)//2,
+         'identity-target counterexample')
+    count['overbroad_claim_counterexamples'] += 1
+
+    # A zero address frame is an identity call but still carries scalar
+    # pairing rank. It is excluded by the theorem, not by the constructor.
+    calls = [(2, 1, 1), (0, 2, 2)]
+    _, w = kernel.compress_calls(calls, 1, 2)
+    need(endpoint(calls, 2) == desired(1, 1, 2) and w == 1 and w > (len(calls)-1)//2,
+         'zero-frame counterexample')
+    count['overbroad_claim_counterexamples'] += 1
+
+    # Pairings and data components alone do not force a new endpoint when
+    # unrestricted, nonminimal helper factorizations are substituted.
+    original = [(3, 1, 1), (1, 2, 2), (-1, 2, 2)]
+    replaced = [(3, 1, 1), (1, 2, 2), (-1, 6, 2)]
+    need(all_pairings(original, 2) == all_pairings(replaced, 3), 'replacement pairings')
+    need(endpoint(original, 2) == desired(1, 1, 3), 'replacement original restored')
+    changed = [list(row) for row in desired(1, 2, 3)]
+    changed[2][1] = frozenset({-1, 0})
+    need(endpoint(replaced, 3) == tuple(tuple(row) for row in changed),
+         'pairings-only endpoint counterexample')
+    count['overbroad_claim_counterexamples'] += 1
+
+    # The paired rank is optimal only under the stated preservation
+    # contract. Moving an adjacent cancelling pair onto the data wire
+    # keeps frames and the endpoint, but changes the scalar components.
+    replacement = [(a, 1, 1) for a, _, _ in original]
+    need(kernel.compress_calls(original, 1, 2)[1] == 1 and
+         endpoint(replacement, 1) == desired(1, 0, 3),
+         'paired rank mistaken for an unrestricted helper lower bound')
+    count['overbroad_claim_counterexamples'] += 1
+
+    source_hashes = {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest()
+                     for name in ('PROOF.md', 'compress.py')}
+    need((PACKAGE / 'compress.py').read_bytes() == kernel_bytes, 'kernel changed during review')
+    return {'marker': 'PASS_C_INDEPENDENT_COMPRESSION_REVIEW', 'seed': 2026110655,
+            'counts': count, 'reviewed_sha256': source_hashes,
+            'scope': 'Independent finite evidence; universal proof separately reviewed.'}
+
+
+if __name__ == '__main__':
+    print(json.dumps(main(), indent=2, sort_keys=True))
diff --git a/research/restored-helper-compression/verify.py b/research/restored-helper-compression/verify.py
new file mode 100644
index 0000000000..52b1eab14e
--- /dev/null
+++ b/research/restored-helper-compression/verify.py
@@ -0,0 +1,282 @@
+#!/usr/bin/env python3
+"""Independent exact controls for the written helper-compression theorem.
+
+Worker A review for @CubeJerry, with substantial OpenAI Codex assistance.
+Apache-2.0. Finite controls do not establish the universal theorem.
+"""
+from collections import Counter
+from itertools import product
+import json
+from pathlib import Path
+from random import Random
+import runpy
+
+core = runpy.run_path(str(Path(__file__).with_name('compress.py')))
+compress_calls = core['compress_calls']
+factor_helpers = core['factor_helpers']
+ZERO = (0, 0, 0, 0)
+E11, E22, ONES = (1, 0, 0, 0), (0, 0, 0, 1), (1, 1, 1, 1)
+SEED = 2026110617
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def dot(x, y):
+    return sum(((x >> j) & 1) * ((y >> j) & 1)
+               for j in range(max(x.bit_length(), y.bit_length()))) % 2
+
+
+def rank_by_span(vectors):
+    """Independent rank oracle: enumerate the entire binary span, no elimination."""
+    span = {0}
+    for v in vectors:
+        span |= {x ^ v for x in tuple(span)}
+    return len(span).bit_length() - 1
+
+
+def gram(left, right):
+    return [sum(dot(y, x) << j for j, y in enumerate(right)) for x in left]
+
+
+def same_pairings(left, right, smaller_left, smaller_right):
+    need(gram(left, right) == gram(smaller_left, smaller_right), 'Every scalar pairing preserved')
+
+
+def add(a, b):
+    return tuple(x + y for x, y in zip(a, b))
+
+
+def negative(a):
+    return tuple(-x for x in a)
+
+
+def rank_one(a):
+    return len(a) == 4 and a != ZERO and a[0] * a[3] == a[1] * a[2]
+
+
+def identity(n):
+    return [[{ZERO} if i == j else set() for j in range(n)] for i in range(n)]
+
+
+def ring_product(a, b):
+    result = set()
+    for x in a:
+        for y in b:
+            z = add(x, y)
+            result.symmetric_difference_update((z,))
+    return result
+
+
+def matrix_product(a, b):
+    n = len(a)
+    result = [[set() for _ in range(n)] for _ in range(n)]
+    for i in range(n):
+        for h in range(n):
+            if not a[i][h]:
+                continue
+            for j in range(n):
+                if b[h][j]:
+                    result[i][j] ^= ring_product(a[i][h], b[h][j])
+    return result
+
+
+def formal_word(calls, registers):
+    """Direct matrix multiplication in F_2[(M_2(Z),+)], without the H formula."""
+    result = identity(registers)
+    for a, x, y in calls:
+        need(rank_one(a), 'Nonzero rank-one address fixture')
+        need(0 <= x < 1 << registers and 0 <= y < 1 << registers and dot(x, y) == 1,
+             'Legal scalar projector')
+        factor = identity(registers)
+        for i in range(registers):
+            if x >> i & 1:
+                for j in range(registers):
+                    if y >> j & 1:
+                        factor[i][j] ^= {ZERO} ^ {a}
+        result = matrix_product(result, factor)
+    return result
+
+
+def target_matrix(targets, helpers):
+    exponents = list(targets) + [ZERO] * helpers
+    return [[{exponents[i]} if i == j else set() for j in range(len(exponents))]
+            for i in range(len(exponents))]
+
+
+def successful_control(name, calls, targets, helpers):
+    data, registers = len(targets), len(targets) + helpers
+    need(all(a != ZERO for a in targets), 'Count only nonidentity data targets')
+    before = tuple(calls)
+    need(formal_word(calls, registers) == target_matrix(targets, helpers), 'Full restored-helper endpoint')
+    smaller, width = compress_calls(calls, data, registers)
+    need(tuple(calls) == before and [a for a, _, _ in smaller] == [a for a, _, _ in calls],
+         'Frames, order and source word unchanged')
+    mask = (1 << data) - 1
+    need(all((x & mask, y & mask) == (xx & mask, yy & mask)
+             for (_, x, y), (_, xx, yy) in zip(calls, smaller)), 'Data components unchanged')
+    same_pairings([x for _, x, _ in calls], [y for _, _, y in calls],
+                  [x for _, x, _ in smaller], [y for _, _, y in smaller])
+    need(formal_word(smaller, data + width) == target_matrix(targets, width), 'Compressed full endpoint')
+    left, right = [x >> data for _, x, _ in calls], [y >> data for _, _, y in calls]
+    u, v = rank_by_span(left), rank_by_span(right)
+    need(width == rank_by_span(gram(left, right)), 'Minimal pairing-preserving dimension')
+    need(rank_by_span([x for _, x, _ in calls]) == data + u and
+         rank_by_span([y for _, _, y in calls]) == data + v, 'Data coordinate spaces included')
+    need(u + v <= len(calls) - data and width <= min(u, v) and
+         width <= (len(calls) - data) // 2, 'Call-surplus helper bound')
+    return {'case': name, 'calls': len(calls), 'data': data, 'original_helpers': helpers,
+            'left_rank': u, 'right_rank': v, 'compressed_helpers': width}
+
+
+def expect_rejection(name, action, controls):
+    try:
+        action()
+    except ValueError:
+        controls.append(name)
+    else:
+        raise ValueError('Control was not rejected: ' + name)
+
+
+def random_frame(rng):
+    while True:
+        u, v = [rng.randint(-2, 2) for _ in range(2)], [rng.randint(-2, 2) for _ in range(2)]
+        if any(u) and any(v):
+            return tuple(a * b for a in u for b in v)
+
+
+def main():
+    widths = Counter()
+    for left in product(range(4), repeat=3):
+        for right in product(range(4), repeat=3):
+            new_left, new_right, width = factor_helpers(left, right)
+            need(width == rank_by_span(gram(left, right)), 'Independent exhaustive rank')
+            need(len(new_left) == len(new_right) == 3 and
+                 all(0 <= x < 1 << width for x in new_left + new_right), 'Compressed dimensions')
+            need(rank_by_span(new_left) == rank_by_span(new_right) == width, 'Full rank factors')
+            same_pairings(left, right, new_left, new_right)
+            widths[width] += 1
+    need(widths == {0: 274, 1: 2058, 2: 1764}, 'Independent rank distribution')
+
+    # These 64 arbitrary legal three-call words need not have restored
+    # endpoints, so this check does not apply the surplus bound to them.
+    selected_words = {(73 * j + 19) % 4096 for j in range(64)}
+    for number, (left, right) in enumerate(product(product(range(4), repeat=3), repeat=2)):
+        if number not in selected_words:
+            continue
+        calls = [(a, 1 | (u << 1), (1 ^ dot(u, v)) | (v << 1))
+                 for a, u, v in zip((E11, E22, ONES), left, right)]
+        smaller, width = compress_calls(calls, 1, 3)
+        need(formal_word(calls, 3)[0][0] == formal_word(smaller, 1 + width)[0][0],
+             'Ordered data block preserved for an arbitrary endpoint')
+
+    cases = [successful_control('no_data_cancelling_pair',
+                                [(E11, 1, 1), (negative(E11), 1, 1)], [], 1)]
+    for data in range(1, 4):
+        for pairs in range(4):
+            calls = [(E11, 1 << j, 1 << j) for j in range(data)]
+            for j in range(pairs):
+                x = 1 << (data + j)
+                calls += [(E22, x, x), (negative(E22), x, x)]
+            record = successful_control('sharp_cancellation_pairs', calls, [E11] * data, pairs)
+            need(record['compressed_helpers'] == pairs == (len(calls) - data) // 2,
+                 'Sharp surplus equality')
+            cases.append(record)
+
+    orthogonal = [(E11, 1, 1), (E22, 3, 5), (negative(E22), 3, 5)]
+    record = successful_control('orthogonal_nonzero_helper_spans', orthogonal, [E11], 2)
+    need((record['left_rank'], record['right_rank'], record['compressed_helpers']) == (1, 1, 0),
+         'Zero paired rank despite two nonzero spans')
+    cases.append(record)
+
+    radical = [(E11, 1, 1), (E22, 2, 2), (negative(E22), 2, 2),
+               (ONES, 6, 10), (negative(ONES), 6, 10)]
+    record = successful_control('two_sided_radicals', radical, [E11], 3)
+    need((record['left_rank'], record['right_rank'], record['compressed_helpers']) == (2, 2, 1),
+         'Both invisible helper directions removed')
+    cases.append(record)
+
+    # These projectors commute by orthogonality despite mixing data and
+    # helpers. The four-call commutator is a nonadjacent cancellation word.
+    commutator = [(E11, 1, 1), (E22, 3, 5), (ONES, 5, 3),
+                  (negative(E22), 3, 5), (negative(ONES), 5, 3)]
+    record = successful_control('nonadjacent_mixed_commutator', commutator, [E11], 2)
+    need(record['compressed_helpers'] == 2, 'Mixed sharp two-helper example')
+    cases.append(record)
+
+    rng = Random(SEED)
+    random_widths = Counter()
+    for trial in range(64):
+        data, helpers, depth = rng.randint(1, 3), rng.randint(0, 5), rng.randint(1, 3)
+        registers = data + helpers
+        calls, targets = [], []
+        for j in range(data):
+            frame = random_frame(rng)
+            calls.append((frame, 1 << j, 1 << j))
+            target = frame
+            if trial % 2:
+                while True:
+                    second = random_frame(rng)
+                    candidate = add(frame, second)
+                    if candidate[0] * candidate[3] != candidate[1] * candidate[2]:
+                        break
+                calls.append((second, 1 << j, 1 << j))
+                target = candidate
+            targets.append(target)
+        nested = []
+        for _ in range(depth):
+            x = rng.randrange(1, 1 << registers)
+            while True:
+                y = rng.randrange(1, 1 << registers)
+                if dot(x, y):
+                    break
+            nested.append((random_frame(rng), x, y))
+        calls += nested + [(negative(a), x, y) for a, x, y in reversed(nested)]
+        record = successful_control('seeded_nested_inverse', calls, targets, helpers)
+        random_widths[record['compressed_helpers']] += 1
+
+    controls = []
+    expect_rejection('corrupted_scalar_pairing', lambda: same_pairings([1], [1], [1], [0]), controls)
+    expect_rejection('wrong_idempotence', lambda: compress_calls([(E11, 1, 2)], 1, 2), controls)
+    unrestored = [(E11, 1, 1), (E22, 2, 2)]
+    _, unrestored_width = compress_calls(unrestored, 1, 2)
+    need(unrestored_width == 1 > (len(unrestored) - 1) // 2, 'Restoration premise counterexample')
+    expect_rejection('nonidentity_helper_endpoint',
+                     lambda: successful_control('bad', unrestored, [E11], 1), controls)
+    wrong_count = [(E22, 2, 2), (negative(E22), 2, 2)]
+    _, wrong_width = compress_calls(wrong_count, 1, 2)
+    need(wrong_width == 1 > (len(wrong_count) - 1) // 2, 'Identity data-count counterexample')
+    expect_rejection('counted_identity_data_target',
+                     lambda: successful_control('bad', wrong_count, [ZERO], 1), controls)
+    mutated = [(E11, 1, 1), (E22, 2, 2), (E22, 2, 2)]
+    expect_rejection('mutated_cleanup_frame',
+                     lambda: successful_control('bad', mutated, [E11], 1), controls)
+    zero_call = [(ZERO, 1, 1)]
+    _, zero_width = compress_calls(zero_call, 0, 1)
+    need(zero_width == 1 > len(zero_call) // 2 and ({ZERO} ^ {ZERO}) == set(),
+         'Zero coefficient gives identity but destroys the surplus bound')
+    expect_rejection('zero_address_update', lambda: formal_word(zero_call, 1), controls)
+
+    # Preserving self-pairings alone is insufficient: the data blocks differ.
+    two = [(E22, 3, 5), (ONES, 5, 3)]
+    truncated = [(a, 1, 1) for a, _, _ in two]
+    need(formal_word(two, 3)[0][0] != formal_word(truncated, 1)[0][0],
+         'Self-pairing-only rejection control')
+    controls.append('preserved_self_pairings_only')
+
+    print(json.dumps({'status': 'PASS_RESTORED_HELPER_COMPRESSION',
+                      'binary_factorizations': sum(widths.values()),
+                      'paired_rank_histogram': dict(sorted(widths.items())),
+                      'arbitrary_endpoint_data_block_checks': 64,
+                      'structured_restored_word_checks': len(cases),
+                      'seeded_nested_inverse_checks': 64,
+                      'seed': SEED, 'random_width_histogram': dict(sorted(random_widths.items())),
+                      'zero_pairing_example': next(c for c in cases if c['case'] == 'orthogonal_nonzero_helper_spans'),
+                      'rejection_controls': controls,
+                      'scope': 'Finite exact controls; the universal theorem is the written proof.'}, indent=2))
+
+
+if __name__ == '__main__':
+    main()