diff --git a/research/refined-native-recovery/CHAIN_PROOF.md b/research/refined-native-recovery/CHAIN_PROOF.md
new file mode 100644
index 0000000000..e6af4bbcbb
--- /dev/null
+++ b/research/refined-native-recovery/CHAIN_PROOF.md
@@ -0,0 +1,233 @@
+# Sharp recovery with mode-preserving parity-I native frames
+
+This is a scoped interface theorem for the literal 112-by-8 integer matrix
+in [#5444](https://github.com/CrocSwap/integer-mult-bounds/pull/5444),
+`research/precision-state-frontier/FIXTURE.json`. It does not prove physical
+reversibility, a selected supplier bound, or a new multiplication exponent.
+
+## 1. Exact statement and source facts
+
+Let R be componentwise nearest-integer rounding, with half ties away from
+zero. Let M be the pinned integer matrix and define
+
+    K(z) = z − M R(Mᵀz/52),       z ∈ Z^112.
+
+The following finite identities are inherited from #5444 and rechecked on
+the actual fixture by both implementations in this package:
+
+    MᵀM = 56 I8,
+    C := ker_F2(M mod 2) = row_F2(M mod 2),
+    |C| = 16,     W_C(a,b) = a^8 + 14 a^4 b^4 + b^8.
+
+In particular C is self-dual and contains zero. No claim is made that these
+finite source identities prove a statement about other native matrices.
+
+Fix any integer t ≥ 1. For 1 ≤ j < t, let U_j be fixed, known matrices with
+
+    U_j ∈ GL_112(Z),       MᵀU_j = Mᵀ,       U_j ≡ I (mod 2).       (1)
+
+They may fail to commute with K, its linear approximation, or one another.
+Define the chain
+
+    z_1 = K(2x),     z_(j+1) = K(U_j z_j),     x ∈ Z^112.          (2)
+
+The factor 2 represents exactly one relative precision bit, introduced
+before the first invocation. Every subsequent invocation is on the same
+integer grid. There is no hidden refinement between later invocations.
+Only the final output y=z_t and a retained tag are available for recovery.
+
+**Theorem.** The exact maximum fiber of (2), for every frame sequence
+satisfying (1), is
+
+    A_t = W_C((13^t+1)/2, (13^t−1)/2)
+        = (13^(8t) + 14·13^(4t) + 1)/16.                         (3)
+
+The output y=0 attains this maximum. Thus A_t is the smallest fixed tag
+alphabet for exact recovery in this declared interface. The minimum packed
+binary tag length is ceil(log₂ A_t). These are state-count statements, not
+physical storage or execution tariffs.
+
+At t=2,
+
+    A_2                         = 41,588,538,787,713,121,
+    A_1 · 13^8                  = 41,608,923,949,414,081,
+    A_1 · 13^8 − A_2            =     20,385,161,700,960.
+
+Both counts still require 56 bits. Multiplying isolated maxima is a valid
+upper bound, but it is not sharp here. The one-step and same-grid results
+remain predecessor work; (3) determines their refined composition in (1).
+
+## 2. A scalar interval lemma that retains the tie convention
+
+For an integer s put
+
+    Q(s) = {q ∈ Z : R((s+56q)/52) = q},
+    F_s(v) = v − R((s+56v)/52).
+
+The usual residual inequality gives
+
+    ceil((-26−s)/4) ≤ q ≤ floor((26−s)/4).                     (4)
+
+At the lower residual endpoint −26, the quotient must satisfy q ≥ 1;
+at the upper residual endpoint +26, it must satisfy q ≤ −1. These are the
+literal half-away rules, not an assumption that rounding commutes with
+integer translation at a tie.
+
+The interval in (4) has thirteen integers unless s≡2 mod4, when it has
+fourteen. In the latter case its two extreme integers cannot both satisfy
+the endpoint rules: the smaller would have to be positive and the larger
+negative. Removing the disallowed extremes leaves a nonempty interval
+with at most thirteen integers. Therefore Q(s) is consecutive, nonempty,
+and |Q(s)|≤13 for every integer s.
+
+If real numbers differ by 14/13, their rounded integers differ by one or
+two. Indeed each rounding error has magnitude at most 1/2, so the integer
+difference lies between 1/13 and 27/13. It follows that
+
+    F_s(v+1) − F_s(v) ∈ {0,−1}.                              (5)
+
+Also F_s(v)=−v/13−s/52+O(1), so F_s maps Z onto Z. Its level sets are
+consecutive, and directly from the definitions
+
+    F_s^(-1)({w}) = w + Q(s+56w).                            (6)
+
+Every level set thus has at most thirteen elements. For any finite integer
+interval I, its preimage is again a finite integer interval, of size at
+most 13|I|. Iterating gives
+
+    I_t(s) := {v : F_s composed t times sends v to 0}
+    is a nonempty consecutive interval,   |I_t(s)| ≤ 13^t.   (7)
+
+At s=0, denominator thirteen excludes half ties, and integer translation
+in rounding is legitimate:
+
+    F_0(v) = v − R(14v/13) = −R(v/13).
+
+The preimage of [−h,h] is [−13h−6,13h+6]. Starting from {0} proves
+
+    I_t(0) = [−(13^t−1)/2, (13^t−1)/2] ∩ Z.                (8)
+
+Equations (4)–(8) prove the all-integer statement. The finite scalar
+checks in this package corroborate them; the checks are not the proof.
+
+## 3. Exact fiber parametrization for arbitrary outputs
+
+Fix a proposed final output y and write s=Mᵀy. For a potential input,
+let T_j be the cumulative quotient still to be subtracted after stage j.
+Then T_t=0 and the mode projection at that stage is s+56T_j. This follows
+from MᵀM=56I and the mode-preservation condition in (1), which also holds
+for U_j^(-1).
+
+Each scalar coordinate therefore satisfies
+
+    T_j = F_s(T_(j−1)),      q_j = T_(j−1)−T_j.             (9)
+
+The possible initial total quotients are exactly the vectors T=T_0 with
+
+    T_k ∈ I_t(s_k) for k=1,...,8,
+    y + MT ≡ 0 (mod 2).                                   (10)
+
+Here is a direct proof of sufficiency, including chronology. From a vector
+T satisfying (10), compute all T_j by (9) and the corresponding q_j.
+Starting at z_t=y, reverse the chain by
+
+    z_(j−1) = U_(j−1)^(-1)(z_j + Mq_j)   for j=t,...,2,
+    2x = z_1 + Mq_1.                                      (11)
+
+Every intermediate vector is integral. Since each inverse frame is I mod2,
+the last expression has parity y+M∑q_j=y+MT, so x is integral. Mode
+preservation proves inductively that the reconstructed pre-kernel vector
+has projection s+56T_(j−1). Thus its actual rounded quotient is q_j;
+every forward invocation returns the vector prescribed in (11).
+
+Necessity follows by reversing an actual chain. Distinct T give distinct
+inputs because
+
+    2Mᵀx = s + 56T.                                      (12)
+
+Consequently (10) is a bijection with the full fiber, not just a necessary
+congruence or a volume relaxation. There are no extra quotient-history
+tags in this parametrization.
+
+## 4. Counting and sharpness
+
+Let N=13^t, a=(N+1)/2 and b=(N−1)/2. Each scalar interval in (10) has at
+most N elements, hence at most a of its preferred parity and b of the
+other parity. The possible parity vectors in (10) are either absent or
+one coset of C. After shifting the preferred parity vector, an upper bound
+on the fiber is the largest value of
+
+    sum_(c ∈ C+z) a^(8−weight(c)) b^weight(c).              (13)
+
+For a≥b≥0 the zero coset maximizes (13). To see this without assuming a
+coset classification, expand by binary characters:
+
+    (13) = |C|/256 · sum_(u ∈ C-perp) (−1)^(u·z)
+                          (a+b)^(8−weight(u))(a−b)^weight(u).
+
+All unsigned summands are nonnegative, and zero z gives every sign +1.
+Since C=C-perp, its checked weight enumerator proves the upper bound
+W_C(a,b). This use of code-character duality is classical; it is not
+claimed as new mathematics.
+
+For y=0, (8) gives N elements in every coordinate. Because 13^t≡1 mod4,
+the symmetric interval has exactly a even and b odd integers. The
+congruence in (10) is T mod2∈C. Thus the count is exactly W_C(a,b), and
+(11) reconstructs every attaining input for every allowed frame sequence.
+This proves (3) and its constructive attainment.
+
+## 5. Actual noncommuting source frames
+
+Use zero-based source row indices. The literal source rows satisfy
+
+    Mᵀv=0,   v=e1+e12−e0−e16,
+    Mᵀw=0,   w=e0+e8−e2−e6.
+
+Set U=I+2v e2ᵀ and V=I+2w e3ᵀ. The source coordinates satisfy v_2=w_3=0,
+so U^(-1)=I−2v e2ᵀ and V^(-1)=I−2w e3ᵀ. Both satisfy all of (1).
+They do not commute with each other:
+
+    UV−VU = −4v e3ᵀ ≠ 0.
+
+They are not merely changes commuting with the native inverse. For the
+actual vector h=52e2, direct exact arithmetic gives
+
+    K(Uh)−U K(h) = 8v ≠ 0.
+
+The same witness shows noncommutation with the linear approximation
+L=I−MMᵀ/52, because all quotients on this witness are exact integers.
+The two-step instance uses U; longer checked chains alternate U and V.
+This establishes that the theorem includes genuinely noncommuting frames.
+It does not price their physical delivery at a selected caller.
+
+## 6. Effective codec and scope
+
+The implementation computes I_t(s) by taking the two extreme preimages
+in (6), never by enumerating 13^t points. It enumerates the at most sixteen
+parity blocks in (10), counts each Cartesian product, and uses mixed-radix
+ranking/unranking. Equation (11) reconstructs the input and a literal
+forward replay checks the result. The largest fiber determines the fixed
+alphabet; a specific output may use fewer tags.
+
+The executable supports depths 1 through 8 and the validated integer-shear
+interface. This is an operational limit, while the written theorem covers
+every finite t and every frame satisfying (1). Arbitrary-precision integer
+arithmetic, fixed known source/frame descriptions and full output access
+are assumed. Reversible arithmetic, quotient workspace, finite registers,
+physical routing, cleanup and complete native/caller tariffs are not
+provided. Input-dependent frames, later refinements, mode-changing frames,
+and parity-changing frames are outside the theorem.
+
+Theorem (3) resolves a restricted but source-sized family of #5444's mixed
+refinement question. The companion PROOF.md determines the optimal two-stage count for the full
+mode-preserving class, including parity-changing frames. Mode-changing
+frames and nonuniform refinement remain open. All five selected framework
+assumptions remain; no new κ.
+
+Prepared for @CubeJerry with substantial OpenAI Codex assistance, including
+separate derivation and implementation review. Credit zxv/#5444 for the
+precision-state question, general one-step fiber theorem and changing-frame
+history result; Ali Romman/#5323 for the same-grid source count; Brian/#5035
+for the literal rounded kernel; and the retained native/caller lineage.
+New proof and implementation are Apache-2.0. Independent human and formal
+proof-kernel acceptance are not claimed.
diff --git a/research/refined-native-recovery/COST_SCOPE.md b/research/refined-native-recovery/COST_SCOPE.md
new file mode 100644
index 0000000000..34bff974e6
--- /dev/null
+++ b/research/refined-native-recovery/COST_SCOPE.md
@@ -0,0 +1,119 @@
+# Caller compatibility and cost scope
+
+The 52-bit optimum is an information statement for the changed function
+`H_U(x)=K(U K(2x))`, with the full final 112-owner output available to the
+decoder. It does not by itself price a physical implementation or change the
+selected multiplication bound.
+
+## Exact boundary for a linear consumer
+
+Write the explicit frame as `U=I+VE`, with `EV=0` and `M^T V=0`. For every
+integer z, mode preservation gives exactly
+
+    K(Uz)-K(z)=VEz.
+
+Consequently, for the identity-frame baseline `H_I(x)=K(K(2x))`,
+
+    H_U(x)-H_I(x)=VE K(2x).
+
+A fixed real- or complex-linear observer O therefore sees the same output for every integer
+input if `OV=0`. For this particular frame, the condition is also necessary.
+The four integer inputs `x=26e_a`, for `a in (0,1,2,4)`, give the columns
+of
+
+    E K(2x):  52I_4-G,   G=E M M^T E^T=2I_4+2J_4,
+
+where J_4 is the all-one matrix. Thus `52I-G=50I-2J` has eigenvalues
+42,50,50,50 and determinant 5,250,000. These four columns span all of R^4.
+If `O H_U=O H_I` on every integer input, then `OV(52I-G)=0`, hence `OV=0`.
+This also proves necessity on any finite input range containing those four
+witnesses. It does not assert necessity for every smaller reachable set.
+
+In particular, `O=M^T` is compatible. A consumer whose complete use of the
+output factors through an observer annihilating V has a possible interface
+route to the new function. **The full H_U output must still be retained or
+otherwise supplied to the 52-bit decoder.** If only `O H_U` is retained,
+its fiber count must be analyzed again; for example, M^T alone discards an
+unbounded native-mode kernel: adding n v_0 to x changes H_U by 2n v_0 and leaves M^T H_U unchanged. Thus no finite tag recovers arbitrary inputs from that observation alone.
+No actual selected caller with this observer and retention contract is
+identified here, and physical access to the full output remains charged.
+
+## An inverse endpoint frame does not restore the old output
+
+For `q=R(M^Tz/52)`, the other exact identity is
+
+    U^-1 K(Uz)-K(z)=V E M q.
+
+It is generally nonzero. With `m=row_0(M)^T`, the actual source input
+`x=(52e_0-13Mm)/2` is integral, has sup norm 13, and satisfies
+`K(2x)=52e_0`. It gives
+
+    U^-1 H_U(x)-H_I(x)=4v_0+2v_1+2v_2+2v_3 != 0.
+
+Thus a caller requiring the complete old output needs a further,
+quotient-dependent correction, rather than just U^-1. If this correction
+restores exactly H_I and retains no additional observation, the old A_2
+maximum fiber and 56-bit tag lower bound return. The identity-frame zero
+fiber is already attained inside the coarse sup-norm bound 168. A smaller
+actual input range needs its own analysis. Any retained correction or side
+observation belongs in the combined recovery alphabet and storage bill.
+
+## Optimistic complete invoice and remaining obligations
+
+The four sources are disjoint from all sixteen destinations, and the four
+update columns have disjoint supports. Hence U and U^-1 each have a literal
+schedule of sixteen signed full-word additions per real coordinate, with
+coordinate sup-norm amplification at most two. This algebraic schedule
+requires no extra coordinate, but does not make physical delivery or carry
+scratch free.
+
+A complete forward-and-recovery invoice must include
+
+    source access + relative-grid provision + first K + U + second K
+      + tag encoding + live quotient/tag storage
+      + unranking + output-mode access + two M lifts + U^-1
+      + exact halving + scratch/tag cleanup + downstream consumption.
+
+The declared direct arithmetic has 896 signed additions and eight
+round-by-52 operations per K call; its owned zero-writing is destructive.
+A direct fresh output projection M^Ty requires 448 signed additions and
+the two reconstruction lifts require 896, per real coordinate. Any reuse
+of already available modes needs a chronological retention schedule.
+The current interface codec's forward replay is verification; if retained
+in an operational decoder, it adds two K calls and a forward frame.
+Reversible rank/unrank, finite word widths, source movement, quotient and
+carry lifetimes, and eventual cleanup have no supplied physical tariff.
+Retaining or rereading the original input is a competing interface whose
+access/storage must also be priced.
+
+For a coarse input bound H, one conservative forward range envelope is
+
+    Q(B)=floor((56B+26)/52),   k(B)=B+4Q(B),
+    B0=2H, B1=k(B0), B2=2B1, B3=k(B2).
+
+Kernel mode accumulators can reach 56B; partial reconstruction lifts and
+codec arithmetic need additional prefix bounds. The theorem does not
+establish that a selected caller's existing registers cover these bounds.
+
+The four-bit packed-tag reduction compares interfaces already supplying
+the same one-bit relative refinement. Counting only added fractional
+positions and a separately packed tag gives 112+56=168 positions for the
+parity-I baseline and 112+52=164 for this frame, per real coordinate. A
+same-grid two-call interface needs 60 tag bits; introducing the refinement
+would instead add 104 positions before magnitude, scratch and movement.
+Absolute working precision alone does not establish a relative grid gain.
+For multiple coordinates packed jointly, use the ceiling of the logarithm
+of the complete product alphabet, rather than assuming four saved bits
+per coordinate after arbitrary pooling.
+
+No selected paid rank, productive target, complete caller invoice or
+precision/tape premise changes here. The complex supplier remains binding
+under the selected certificate. All five assumptions remain:
+`native_all_columns`, `owned_erasure`, `compiler`, `precision_tape`, and
+`analytic_recovery`. **No new κ.**
+
+This scope analysis builds on the relative-grid and physical-caller
+limitations of CrocSwap/integer-mult-bounds#5444, the same-grid recovery
+result in #5323, and the source arithmetic in #5035. Prepared for @CubeJerry
+with substantial OpenAI Codex assistance, including separate source-bound
+compatibility and cost review.
diff --git a/research/refined-native-recovery/PROOF.md b/research/refined-native-recovery/PROOF.md
new file mode 100644
index 0000000000..26abf5db19
--- /dev/null
+++ b/research/refined-native-recovery/PROOF.md
@@ -0,0 +1,299 @@
+# Optimal two-stage refined recovery over mode-preserving integer frames
+
+This theorem concerns the literal 112-by-8 integer matrix from
+[#5444](https://github.com/CrocSwap/integer-mult-bounds/pull/5444), pinned
+in SOURCES.json. It gives a minimum abstract recovery alphabet for a
+specified family of changed output functions. It does not give a paid
+physical memory saving, a supplier invoice, or a new multiplication exponent.
+
+## 1. Exact statement
+
+Let R be componentwise nearest-integer rounding with half ties away from
+zero, and let
+
+    K(z)=z−M R(Mᵀz/52),             z∈Z^112.
+
+The actual source satisfies MᵀM=56I8 and
+
+    C=ker_F2(M mod2)=row_F2(M mod2),
+    |C|=16,       W_C(a,b)=a^8+14a^4b^4+b^8.
+
+These finite source identities are inherited from #5444 and independently
+rechecked on its pinned fixture. All indices below are zero-based.
+Let G be the class of all fixed, known matrices
+
+    U∈GL_112(Z) with MᵀU=Mᵀ,
+
+without imposing U≡I modulo two. For U∈G define the output function
+
+    H_U(x)=K(U K(2x)),             x∈Z^112.
+
+The factor 2 is exactly one relative precision bit before the first call;
+there is no additional refinement before the second. Only the declared
+final output H_U(x) and a tag are available for exact recovery. Put
+
+    F=W_C(7,6)=(13^8+14·13^4+1)/16=51,008,161.
+
+**Theorem.** The optimal worst-case fiber over this entire class is
+
+    min_(U∈G) max_y |H_U^−1(y)| = F²
+                                = 2,601,832,488,601,921.       (1)
+
+A frame attains this minimum if and only if
+
+    im_F2(M) ∩ im_F2(U^−1M) = {0}.                            (2)
+
+An explicit integer frame satisfying (2) is constructed in Section 3.
+For it the zero output attains the maximum. Consequently its minimum
+fixed recovery-tag alphabet has F² states and its packed width is 52 bits.
+By contrast, every frame in the parity-I subclass has sharp two-step
+maximum A2=(13^16+14·13^8+1)/16=41,588,538,787,713,121, requiring 56 bits.
+The output map changes with U; this is not a claim that a caller can
+retain its original output contract and save four physical bits.
+
+The separate [CHAIN_PROOF.md](CHAIN_PROOF.md) proves the complementary
+all-finite-depth formula A_t=(13^(8t)+14·13^(4t)+1)/16 for mode-preserving
+parity-I frame sequences, including genuinely noncommuting ones. Its
+scalar lemmas and full chronology are restated where needed below.
+
+## 2. Full two-step fiber parametrization and universal lower bound
+
+For a final output y put s=Mᵀy, coordinatewise, and define
+
+    Q(s)={q∈Z: R((s+56q)/52)=q},
+    F_s(T)=T−R((s+56T)/52),
+    I2(s)={T: F_s(F_s(T))=0}.
+
+The scalar interval proof in CHAIN_PROOF.md, Section 2, shows that Q(s)
+is a nonempty interval of length at most 13, I2(s) is a nonempty interval
+of length at most 169, and
+
+    F_s^−1({w})=w+Q(s+56w).
+
+The half-away convention is retained even at endpoints. At s=0,
+Q(0)=[−6,6] and I2(0)=[−84,84]. For every U∈G the actual fiber is in
+bijection with the eight-coordinate total quotient T satisfying
+
+    T_j∈I2(s_j),       U^−1(y+Mq2)+Mq1 is even,              (3)
+    q2=F_s(T),         q1=T−q2.
+
+Indeed reverse chronology gives
+
+    x=(U^−1(y+Mq2)+Mq1)/2.                                 (4)
+
+Integrality is exactly the second condition in (3). Mode preservation
+shows that the two actual pre-kernel modes are s+56T and s+56q2,
+respectively, so their rounded quotients are precisely q1 and q2.
+Thus forward execution returns y. Conversely any actual preimage gives
+these quantities. Distinct T give distinct inputs because
+
+    2Mᵀx=s+56T.                                           (5)
+
+For the universal lower bound in (1), take q2∈[−6,6]^8 with q2 mod2∈C.
+At y=0 the first quotient lies in
+
+    q1∈Q(56q2)=[−6,6]^8−14q2.
+
+This translation is even and has no half ties. The choices with q1 mod2∈C
+number F for every such q2, and the choices of q2 number F. Both Mq1 and
+Mq2 are even. Since U^−1 is integral, every one of these F² pairs gives
+an actual input by (4) for every U∈G. No two pairs give the same T,
+since q2=F_0(T), and (5) then proves input distinctness. Consequently
+|H_U^−1(0)|≥F² universally. This is constructive attainment, not a
+volume or determinant lower bound.
+
+## 3. Explicit source-sized frame and binary image separation
+
+Let E have rows e0ᵀ,e1ᵀ,e2ᵀ,e4ᵀ, and let V have columns
+
+    v0=e64−e65−e96+e97,
+    v1=e10−e11+e62−e63,
+    v2=e14−e15+e41−e42,
+    v3=e18−e19+e39−e40.
+
+Their disjoint supports exclude 0,1,2,4, so EV=0. Write ρ_i for row i
+of M and f7 for the last standard mode vector. The pinned rows satisfy
+
+    ρ64−ρ65=−2f7=ρ96−ρ97,
+    ρ10−ρ11=−2f7,      ρ62−ρ63= 2f7,
+    ρ14−ρ15= 2f7,      ρ41−ρ42=−2f7,
+    ρ18−ρ19=−2f7,      ρ39−ρ40= 2f7.
+
+Thus MᵀV=0 exactly. Set U=I+VE. Then (VE)²=0,
+U^−1=I−VE is integral, and MᵀU=Mᵀ, proving U∈G.
+
+For the quotient condition let L have rows
+
+    (e4+e64)ᵀ, (e10+e70)ᵀ, (e14+e52)ᵀ, (e18+e54)ᵀ.
+
+The paired source rows have identical binary masks 153,165,170,150,
+respectively, hence LM=0 modulo two; the displayed supports give LV=I4
+over the integers. Therefore the four V columns are independent modulo
+im(M mod2). The rows of EM have binary masks 15,51,85,153 and rank four:
+the first three span {0,15,51,60,85,90,102,105}, excluding 153.
+Their span is C, so ker_F2(EM)=C.
+
+If Mp=(M−VEM)q modulo two, then M(p−q)=−VEMq. Multiplying by L gives
+EMq=0; hence q∈C and the common vector is zero. This proves (2).
+The source identities, exact inverse and full binary ranks are checked
+independently. The frame is four commuting sparse transvections, with
+16 signed coordinate additions algebraically; these are not paid machine
+tariffs. It need not commute with the rounded kernel.
+
+## 4. Scalar joint-parity Fourier bound
+
+
+Define a two-by-two integer table and its binary Fourier coefficients by
+
+    w_s(p,q)=#{T∈I2(s): T mod2=p, F_s(T) mod2=q},
+    ŵ_s(α,β)=Σ_(p,q) (−1)^(αp+βq) w_s(p,q).
+
+At s=0 the interval is [−84,84] and F_0(T)=−R(T/13), giving
+
+    w_0 = [[49,36],[42,42]],
+    (ŵ_0(0,0),ŵ_0(1,0),ŵ_0(0,1),ŵ_0(1,1))=(169,1,13,13).
+
+We prove the componentwise bound
+
+    |ŵ_s(α,β)| ≤ ŵ_0(α,β)  for every integer s.             (W)
+
+Here are the complete cases, retaining signs at ties. The exact quotient
+endpoints obey
+
+    ceil((-26−s)/4) ≤ q ≤ floor((26−s)/4),
+
+where the lower extreme at residual −26 requires q≥1, and the upper
+extreme at residual +26 requires q≤−1. If s is not 2 modulo 4, there are
+no endpoint ties, Q(s) has length 13, and
+
+    Q(s+56q2)=Q(s)−14q2.
+
+The parity counts of both q2 and q1 are therefore 7 and 6, with a fixed
+preferred q1 parity independent of q2. Since p=q1+q2 and q=q2, the table
+is a row/column permutation of w0. Such permutations only change signs
+of Fourier coefficients, proving (W) in this case.
+
+For the tie case write s=4k+2. The exact intervals are
+
+    k≥7:       Q(s)=[−k−6,6−k],
+    −7≤k≤6:   Q(s)=[−k−6,5−k],
+    k≤−8:      Q(s)=[−k−7,5−k].                            (5)
+
+If s≥34, then k≥8 and every q2∈Q(s) satisfies
+s+56q2≤338−52k≤−78. Hence the inner quotient interval is in the last
+case of (5) and is
+
+    Q(s+56q2)=[−k−7,5−k]−14q2.
+
+All outer and inner intervals again have length 13 and a fixed preferred
+q1 parity, so the same Fourier conclusion follows. Oddness of R sends
+(s,T,q2) to (−s,−T,−q2), preserving both parities. Thus w_−s=w_s and the
+case s≤−34 follows too.
+
+Only s=±2,±6,...,±30 remain. Using (5), each table follows from the finite
+identity w_s(p,q)=Σ_(q2∈Q(s),q2≡q) #{q1∈Q(s+56q2):q1+q2≡p}.
+The eight nonnegative representatives are:
+
+|s|w_s (rows p, columns q)|Fourier coefficients (00,10,01,11)|
+|---|---|---|
+|2|[[38,39],[39,39]]|(155,−1,−1,−1)|
+|6|[[39,38],[38,40]]|(155,−1,−1,3)|
+|10|[[37,40],[40,38]]|(155,−1,−1,−5)|
+|14|[[40,37],[37,41]]|(155,−1,−1,7)|
+|18|[[36,41],[41,37]]|(155,−1,−1,−9)|
+|22|[[41,36],[36,42]]|(155,−1,−1,11)|
+|26|[[36,42],[42,36]]|(156,0,0,−12)|
+|30|[[42,42],[36,48]]|(168,0,−12,12)|
+
+These complete (W). Entrywise domination by a permuted w0 is false, for
+example at s=2; the proof specifically uses absolute Fourier domination.
+
+## 5. The sharp all-output upper bound and necessity
+
+Suppose (2) holds. Reducing (4) modulo two gives
+
+    Mq1+U^−1Mq2=U^−1y.
+
+Disjointness implies that this equation either has no solution or uniquely
+fixes each of Mq1 and U^−1Mq2. Their binary kernels are both C. Thus
+(q1 mod2,q2 mod2) ranges over one affine coset of C×C. Under the
+invertible change (p,q)=(q1+q2,q2), the kernel is still C×C.
+
+For any fixed modes s=Mᵀy the full fiber count is therefore the product
+weight of an affine coset b+(C×C) under the eight scalar tables w_sj.
+Since C is self-dual, character orthogonality gives exactly
+
+    1/256 Σ_(h∈C×C) (−1)^(h·b) Π_(j=0)^7 ŵ_(sj)(h_pj,h_qj).
+
+The absolute coefficient bound in Section 4 and the triangle inequality
+bound this by the same sum with all factors replaced by their nonnegative
+w0 coefficients and all signs positive. That sum is the actual zero-output
+fiber, since y=0 gives s=0 and b=0. At zero the q1,q2 parities separate,
+and Section 2 counts precisely F². This proves the all-output upper bound
+and the sufficiency direction of (2), completing (1).
+
+For necessity, suppose the two binary images have a nonzero common vector z.
+Choose binary quotient cosets mapping to z under M and U^−1M. Every binary
+parity vector is represented in each of the nonempty 13-element scalar
+intervals for q2 and q1 at zero, so these cosets give additional actual
+inputs via (4). They lie outside the C×C family because z≠0. Their
+trajectory and total quotient are unique by Section 2. Thus the zero fiber
+is strictly larger than F². This proves the converse, without assuming an
+unproved classification of coset weights.
+
+## 6. Effective full-output codec and exact scope
+
+For the explicit frame, let δ=Ly modulo two. Equation (3) is equivalent to
+
+    Mp=y+Vδ,          (EM)q=δ+Ey,          p=T mod2, q=q2 mod2.
+
+The first syndrome is either impossible or a C-coset; the second is a
+C-coset. For every coordinate, enumerate at most 169 values of I2(s_j)
+and partition them into four joint (p_j,q_j) cells. At most 256 code-pair
+blocks then give exact Cartesian products. Mixed-radix rank/unrank within
+these finite cells implements the full fiber bijection. It is effective
+for every integer output, not merely zero. The executable validates the
+literal forward result of every decode, and tests arbitrary nonzero
+outputs, endpoint tags, all 256 zero-output blocks, and large integers.
+
+Fixed known frames, unbounded exact integers, the specified relative grid,
+and complete output access are assumptions of this interface theorem.
+Input-dependent frames, mode-changing frames, prescribed finite ranges,
+later extra refinement and longer parity-changing chains are not proved.
+Arbitrary-precision arithmetic, finite storage, quotient workspace, owner
+access, routing, reversible cleanup and restoration are unpriced. The
+52-bit result alone does not discharge any selected framework assumption.
+
+The output function H_U changes with U. Postcomposing by U^−1 does not
+in general restore the unframed K(K(2x)) output. If a corrected procedure
+must return exactly that unframed output with only a recovery tag and no
+additional retained side data, its maximum fiber is again A2, forcing
+56 packed bits. An actual accepting caller or a completely charged
+restoration interface is required before asserting a physical benefit.
+See COST_SCOPE.md for the reachable source witness and symbolic ledger.
+
+The theorem resolves the two-step mixed-refinement question of #5444
+within the full mode-preserving integer frame class, including all
+parity-changing frames in that class. General mode-changing frames and
+physical realization remain open. All five selected assumptions remain;
+No new κ.
+
+A concrete limitation prevents blindly extending the Fourier argument to
+three parity-changing stages. Let q3∈Q(s), q2∈Q(s+56q3), and
+q1∈Q(s+56(q2+q3)). The character sum Σ(−1)^(q2+q3) equals 13 at s=0
+but −14 at s=2. For s=2 the outer (q2,q3)-parity counts are
+38,39,39,39, with signed sum −1; every inner Q has length 13 except
+(q2,q3)=(0,0), whose length is12. Thus the sum is 13·(−1)−1=−14.
+The corresponding zero-mode sum is 13. This explicitly disproves the
+same componentwise zero-coefficient majorant for three quotient parities.
+It does not disprove a three-stage optimum or any different counting
+argument. The exact two-case negative control is registered in this package.
+
+Prepared for @CubeJerry with substantial OpenAI Codex assistance in
+primary derivation/codec, separate source-frame construction, independent
+proof/checker review, and the caller-cost audit. Credit zxv/#5444 for the
+precision question and source one-step/code facts, Ali Romman/#5323 for
+same-grid source counts, Brian/#5035 for the literal rounded kernel, and
+all retained native/caller contributors. Character duality and mixed-radix
+coding are classical. New proof and code are Apache-2.0. Independent human
+acceptance or formal proof-kernel admission is not claimed.
diff --git a/research/refined-native-recovery/README.md b/research/refined-native-recovery/README.md
new file mode 100644
index 0000000000..a5d15573e1
--- /dev/null
+++ b/research/refined-native-recovery/README.md
@@ -0,0 +1,116 @@
+# Optimal refined recovery with a mode-preserving integer frame
+
+**Sharp abstract 52-bit recovery tag on the actual 112-owner source;
+No new κ.** For two rounded native invocations, with one relative precision
+bit before the first, an explicit integer frame reduces the exact worst-case
+recovery alphabet to **2,601,832,488,601,921 states**, requiring **52 bits**.
+This is optimal over every fixed known integer unimodular frame preserving
+the eight native mode projections. The parity-I subclass requires 56 bits.
+
+The output function changes with the frame. These are abstract tag counts,
+not a physical memory or runtime saving at an existing caller. Restoring
+the exact unframed output without retaining additional side data restores
+its 56-bit lower bound. [COST_SCOPE.md](COST_SCOPE.md) gives the explicit
+reachable witness, full symbolic cost obligations and remaining interface.
+
+## Technical result and novelty
+
+With the inherited matrix M and literal half-away rounded map
+
+    K(z)=z−M R(Mᵀz/52),     H_U(x)=K(U K(2x)),
+
+let G contain all U∈GL_112(Z) satisfying MᵀU=Mᵀ. Then
+
+    min_(U∈G) max_y |H_U^−1(y)|
+      = ((13^8+14·13^4+1)/16)^2 = 2,601,832,488,601,921.
+
+A frame attains this minimum exactly when the binary images of M and
+U^−1M intersect only at zero. The package supplies a sparse rank-four
+transvection U=I+VE, its exact inverse, source identities and dual witnesses
+proving that condition. Zero output attains the maximum; an independent
+all-output Fourier argument proves no output has a larger fiber.
+
+This resolves the two-step mixed-refinement question from
+[`precision-state-frontier/README.md`](../precision-state-frontier/README.md),
+[zxv's #5444](https://github.com/CrocSwap/integer-mult-bounds/pull/5444),
+within the entire mode-preserving integer-frame class. It does not settle
+mode-changing frames. The predecessor one-step frontier, source binary code
+and same-grid history counts remain predecessor work. The new result is
+the complete composition theorem, optimal-frame criterion, explicit source
+construction and effective full-output recovery codec.
+
+As a complementary result, every fixed sequence of mode-preserving
+parity-I frames has sharp finite-depth maximum
+
+    A_t=(13^(8t)+14·13^(4t)+1)/16.
+
+At t=2 this is 41,588,538,787,713,121 states. It is strictly below the
+naive product of isolated maxima, but both require 56 bits. Explicit
+parity-I frames fail to commute with the rounded kernel and each other.
+This all-finite-depth theorem is in [CHAIN_PROOF.md](CHAIN_PROOF.md);
+the optimal two-stage theorem is in [PROOF.md](PROOF.md).
+
+`optimal_codec.py` ranks and unranks every attained output using at most
+256 code-pair blocks and at most 169 scalar candidates per mode. It checks
+literal forward replay after decoding. `recovery.py` supplies the companion
+parity-I chain codec for depths 1 through 8. These exact integer programs
+are not reversible bit/tape implementations or paid native callers.
+
+## Reproduce and verification
+
+From the repository root, CPython 3.12 and the standard library:
+
+```sh
+python3 -B scripts/research_package.py --package research/refined-native-recovery
+```
+
+Expected markers include `PASS_REFINED_NATIVE_RECOVERY`,
+`PASS_INDEPENDENT_REFINED_NATIVE_RECOVERY`,
+`PASS_INDEPENDENT_OPTIMAL_FRAME`, and `PASS_REGISTERED_RESEARCH_PACKAGE`.
+The registered commands run normal and optimized Python. They check the
+literal source, exact frame/inverse and dual identities, scalar tie cases,
+all zero-output parity blocks, arbitrary-output codec roundtrips and
+rejecting controls. Separately written checkers import no primary code.
+[VALIDATION.md](VALIDATION.md) records exact executed coverage and limits;
+[RESULT.json](RESULT.json) binds the package and source hashes.
+
+The canonical base is `a7638a4ce2a29947457ae8d6bf8cd70a234dfeac`.
+[SOURCES.json](SOURCES.json) pins the actual fixture, predecessor question
+and proof sources, and task context. Only the fixture is a live external
+input. No predecessor executable or selected artifact is changed.
+The selected conditional κ=0.003125804 remains unchanged.
+
+## Scope and limitations
+
+The theorem assumes fixed known frames, unrestricted exact integer inputs,
+the stated relative grid, and final output plus a retained tag. It does
+not automatically apply on a prescribed finite box. Source access,
+finite-width arithmetic, intermediate workspace, physical movement,
+cleanup and accepting/restoring the changed output remain unpaid.
+
+## Open next questions
+
+1. What is the sharp optimum for a genuinely mode-changing two-step frame?
+   Derive its coupled quotient equations; common-mode scalar recursion
+   no longer applies.
+2. Can a named physical caller accept this output map with a favorable
+   complete paid bill? Bind its grids, range, workspace, source access,
+   routing, restoration and cleanup before claiming a supplier gain.
+3. What is the optimal recovery alphabet for longer parity-changing chains
+   or nonuniform refinement? The finite-depth theorem here covers only
+   the parity-I class.
+
+All five selected assumptions remain: native_all_columns, owned_erasure,
+compiler, precision_tape and analytic_recovery. No selected cold replay,
+physical caller admission, formal proof-kernel build or human acceptance
+is claimed. Structured scope and next steps are in [TASK.json](TASK.json).
+
+## Credit
+
+Prepared for **@CubeJerry** with substantial **OpenAI Codex assistance** in
+primary derivation and codec, complementary sparse-frame construction,
+independent mathematical/implementation checking and caller-cost audit.
+Credit zxv/#5444, Ali Romman/#5323, Brian/#5035 and the retained source,
+normalizer, native/caller and precision contributors. Character duality,
+binary linear algebra and mixed-radix coding are classical. New proofs and
+code are Apache-2.0; no general literature-priority claim is made.
diff --git a/research/refined-native-recovery/RESULT.json b/research/refined-native-recovery/RESULT.json
new file mode 100644
index 0000000000..5c18b6e1e0
--- /dev/null
+++ b/research/refined-native-recovery/RESULT.json
@@ -0,0 +1,64 @@
+{
+  "codewords": 16,
+  "gram_entries": 64,
+  "interval_depths": [
+    1,
+    2,
+    3
+  ],
+  "maximum_tested_depth": 6,
+  "no_new_kappa": true,
+  "noncommutation_witnesses": 2,
+  "optimal_two_stage": {
+    "arbitrary_output_codec_roundtrips": 144,
+    "distinct_arbitrary_outputs": 48,
+    "distinct_joint_tables": 12,
+    "linear_observer_spanning_determinant": 5250000,
+    "linear_observer_spanning_inputs": 4,
+    "optimal_packed_bits": 52,
+    "optimal_rejecting_controls": 12,
+    "optimal_states": 2601832488601921,
+    "rank_four_basis_inverse_checks": 224,
+    "reachable_output_contract_defect": [
+      4,
+      2,
+      2,
+      2
+    ],
+    "reachable_witness_input_norm_infinity": 13,
+    "three_stage_character_011_at_s0_s2": [
+      13.0,
+      -14.0
+    ],
+    "walsh_scalar_parameters": 417,
+    "walsh_scalar_points": 70277,
+    "zero_code_pair_blocks": 256
+  },
+  "package_sha256": {
+    "CHAIN_PROOF.md": "5b64a5a4a42f99ae8e094fdd20a9fbbcb54c2af4fbabfea8e58a351991a4e06a",
+    "COST_SCOPE.md": "daa5cf8f0895916f7ea479cf170c2f30f88b2368eeb46be1f208cfc06a3f932a",
+    "PROOF.md": "d54eac2e7d464ff30f9eada02b049435ca48dfb335e37e74a3c1cc67871aedb9",
+    "README.md": "59bc2410dd267df849831eff8db65579f856ed40cdf77172c505d84c4b894df1",
+    "REVIEW.md": "43287e227222aa3924c3887891f7d8b11df98a4a1bf48bc922bb2a0e31bb49b4",
+    "SOURCES.json": "6a3b8207bafcefbbeb49824255caed804a654a76bb251a64c9d6958a0fd403fb",
+    "TASK.json": "20f68b06253f8448be4cb13eb6cc3bdf414efaaa3d84a0185d20e3570f14fbdc",
+    "VERIFY.json": "7a9082a9d2f0d8449c1acd6a44b5d9fef544444f2341c6e113bd73ef3df67a9c",
+    "construction.py": "dc3d8de42055262389c1fe4ab6635367807a4ce7fbec088fddffabd3466a4e09",
+    "independent_check.py": "34f157fa77df9843023e6b1edb4b35a0898c1b40ecf8b427f41c24db5c2baa6d",
+    "independent_optimal.py": "ca8c10a15c33ea802132433842d8c42c8db51023ebbcb78e7bae43b779433772",
+    "optimal_codec.py": "bd22cdca435a3677b2ab29da3a5c32b5fb2e0fa452fcf2e280484983fde288cd",
+    "optimal_verify.py": "e5a5d88a715801ed34ddab3d992a5aeda969738bccd538fbf2426ac5c9fe385c",
+    "recovery.py": "1c85b2f24b279d82179bc32dba3a0ceb70a96c723a1423ce2904bf1df1a30ba1",
+    "verify.py": "f42ac8c9f69659f0832abbba2e1caadc1af56204dac64c0d1ec2ad1a858add28"
+  },
+  "parity_I_naive_two_step_product": 41608923949414081,
+  "parity_I_two_step_packed_bits": 56,
+  "parity_I_two_step_state_reduction": 20385161700960,
+  "parity_I_two_step_states": 41588538787713121,
+  "rejecting_controls": 12,
+  "scalar_input_points": 248283,
+  "schema": "refined-native-recovery-result-v2",
+  "shear_basis_vectors": 224,
+  "source_sha256": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8",
+  "source_sized_codec_roundtrips": 384
+}
diff --git a/research/refined-native-recovery/REVIEW.md b/research/refined-native-recovery/REVIEW.md
new file mode 100644
index 0000000000..f58e24f42f
--- /dev/null
+++ b/research/refined-native-recovery/REVIEW.md
@@ -0,0 +1,145 @@
+# Independent review of the optimal two-stage recovery theorem
+
+Reviewed source: canonical base `a7638a4ce2a29947457ae8d6bf8cd70a234dfeac`,
+fixture SHA256 `2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8`.
+The final scientific draft reviewed is
+`worker-b/research/refined-native-recovery/PROOF.md`, headed “Optimal two-stage
+refined recovery over mode-preserving integer frames”. Its source construction
+has selectors `(0,1,2,4)` and the four columns independently transcribed in
+`independent_optimal.py`.
+
+Prepared for @CubeJerry with substantial OpenAI Codex assistance by a separate
+review agent. This is an adversarial mathematical review, not human acceptance
+or formal proof-kernel admission. No new κ.
+
+## Review conclusion
+
+No mathematical objection remains to the exact minimax theorem in the stated
+class of fixed integer unimodular frames preserving Mᵀ. The sharp minimum is
+`51,008,161² = 2,601,832,488,601,921`, requiring 52 packed abstract tag bits.
+Binary image separation is both necessary and sufficient. The explicit source
+frame satisfies it. This changes the declared output function; no physical
+storage, selected supplier, accepted caller, or multiplication-bound improvement
+is inferred.
+
+## Independent reasoning
+
+1. **Full fibers and half ties.** The reverse formula is
+   `2x = U⁻¹(y+Mq2)+Mq1`. Writing `s=Mᵀy`, the scalar quotient conditions are
+   `q2∈Q(s)` and `q1∈Q(s+56q2)`. Consequently `T=q1+q2` determines
+   `q2=T−R((s+56T)/52)`, with no appeal to translation invariance of half-away
+   rounding. Such invariance would be false at some half ties. Integrality of
+   the displayed reverse formula is the entire lattice obligation. Actual
+   mode preservation gives both literal rounded quotients; distinct T have
+   distinct mode vectors `2Mᵀx=s+56T` and thus distinct inputs.
+
+2. **Universal lower bound and necessity.** At zero, q2 lies in `[-6,6]^8`
+   and q1 lies in `[-6,6]^8−14q2`. The shift is even and both scalar parity
+   counts are positive. The `C×C` quotient parities therefore give exactly
+   F² distinct actual inputs for every admissible U. If a nonzero vector lies
+   in both binary images of M and U⁻¹M, select the two nonkernel quotient
+   parity cosets mapping to that vector. Every coordinate parity has a lift
+   in the corresponding 13-element interval. These yield additional actual
+   zero preimages, disjoint from the F² family by the quotient uniqueness
+   just proved. Therefore equality requires disjoint binary images.
+
+3. **All-integer Walsh bound.** I independently derived the endpoint rules
+   for Q(s), including the removed half-away endpoints, and verified the
+   author's exact three-case formula for s=4k+2. For s not congruent to 2
+   modulo 4, the inner interval is Q(s)−14q2. For s≥34 in the tie class,
+   all inner parameters are at most −78, so their endpoint convention is
+   uniform. Negation preserves both parities. Thus only the eight positive
+   exceptional values 2,6,…,30 remain, and their literal quotient counts
+   match all eight displayed tables. This is an exhaustive analytic
+   reduction, independent of the finite census below. Their absolute Walsh
+   coefficients are bounded componentwise by `(169,1,13,13)`.
+
+   A separate derivation is possible from inner alternating parity sums:
+   every inner interval has length 13 except a possible single length-12
+   interval; the preferred inner parity has at most one sign change as q2
+   increases. The alternating outer sum bounds the T-parity coefficient
+   by 1. The other coefficients are bounded by 169,13,13; the only outer
+   odd-length/short-inner cases are s=±30 and give magnitude 12. This
+   corroborates why the exceptional tables do not invalidate the bound.
+
+4. **Sufficiency and Fourier normalization.** Disjoint binary images give
+   one affine coset of `C×C` in `(q1,q2)` parities, or no solution. The
+   invertible change `(q1,q2)↦(q1+q2,q2)` preserves `C×C`. Its orthogonal
+   subspace has 256 elements, so the character formula has coefficient
+   1/256. The nonnegative zero-table Walsh coefficients bound every output
+   by the zero output. At zero, direct q1,q2 parity weights factor and give
+   exactly F². This proves sufficiency and the minimax value.
+
+5. **Actual source witness.** I checked the integer Gram identity, MᵀV=0,
+   EV=0, both inverse compositions on every owner basis vector, and mode
+   preservation. Independently enumerating all 256 binary mode masks gives
+   two 16-element source images whose intersection is `{0}`. This direct
+   image calculation does not reuse the author's rank-elimination routine
+   or dual proof. I also checked the exact dual witnesses LM even and LV=I.
+
+6. **Codec.** I read `optimal_codec.py` and independently checked its
+   syndrome derivation: δ=Ly; `Mp=y+Vδ` and `EMq=δ+Ey`. The Cartesian
+   joint-cell blocks are disjoint and complete. The displayed rank/unrank
+   operations use consistent block and mixed-radix order. Its forward and
+   inverse formulas agree with the literal source-sized trajectories in
+   the independent checker. The proof makes clear that abstract tag width
+   does not include workspace or arithmetic costs.
+
+## Independent executable evidence
+
+`independent_optimal.py` imports no primary module. It authenticates the pinned
+fixture, transcribes the four source columns independently, and AST-checks that
+the primary construction declares the same constants without executing it.
+It uses direct quotient enumeration and direct 112-bit binary image grouping;
+it does not reuse the primary interval algorithm, binary-rank implementation,
+codec, or character-sum count.
+
+Executed in both ordinary and optimized Python, with identical JSON output:
+
+```
+python -I -W error -B independent_optimal.py --source ../precision-state-frontier/FIXTURE.json --construction construction.py
+python -I -O -W error -B independent_optimal.py --source ../precision-state-frontier/FIXTURE.json --construction construction.py
+```
+
+The explicit scratch paths were used for the review runs; the shown relative
+paths are the equivalent package commands. Results:
+
+- All 20,001 scalar parameters in `[-10000,10000]`, including the eight
+  exceptional tables, satisfy the exact Q classification and Walsh caps.
+- All 65,536 binary quotient pairs are grouped into 256 actual source
+  parity syndromes; the maximum is the stated F², attained at syndrome zero.
+- All 224 inverse basis compositions pass.
+- 1,152 source-sized forward/reverse checks pass: three representatives in
+  every one of 256 zero parity blocks and 384 arbitrary-input trajectories,
+  giving 384 distinct sampled outputs.
+- Removing one frame column creates binary intersection size two and raises
+  the zero count to `5,201,116,111,850,821`, explicitly detecting the
+  necessity of complete image separation.
+- Identity frame count is independently `41,588,538,787,713,121`.
+- Controls detect changed mode coefficient, nonnilpotent selector, image
+  overlap, half-away tie errors, the false entrywise-domination argument,
+  omitted inverse frame, and the false optimality of the identity frame.
+
+These finite counts corroborate the universal proof; they are not presented
+as proving a statement by searching a finite domain. The script SHA256 is
+`ca8c10a15c33ea802132433842d8c42c8db51023ebbcb78e7bae43b779433772`.
+
+
+## Final reviewed-file binding
+
+The final three-stage addendum was reviewed independently. Directly enumerating
+q3∈Q(s), q2∈Q(s+56q3), and q1∈Q(s+56(q2+q3)) gives character sums 13 at
+s=0 and −14 at s=2. At s=2 only (q2,q3)=(0,0) has a length-12 inner
+interval; every other inner interval has length 13. The displayed reasoning
+and narrowly stated failure of that particular Fourier majorant are correct.
+It does not claim to disprove a three-stage optimum. The cost discussion
+explicitly requires an accepting caller or charged restoration; the separate
+cost-scope audit is credited separately and is not included in this review's
+mathematical verdict.
+
+This review is bound to the following final package bytes (SHA256):
+
+- `PROOF.md`: `d54eac2e7d464ff30f9eada02b049435ca48dfb335e37e74a3c1cc67871aedb9`
+- `optimal_codec.py`: `bd22cdca435a3677b2ab29da3a5c32b5fb2e0fa452fcf2e280484983fde288cd`
+- `construction.py`: `dc3d8de42055262389c1fe4ab6635367807a4ce7fbec088fddffabd3466a4e09`
+- `independent_optimal.py`: `ca8c10a15c33ea802132433842d8c42c8db51023ebbcb78e7bae43b779433772`
diff --git a/research/refined-native-recovery/SOURCES.json b/research/refined-native-recovery/SOURCES.json
new file mode 100644
index 0000000000..fe10df3373
--- /dev/null
+++ b/research/refined-native-recovery/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "a7638a4ce2a29947457ae8d6bf8cd70a234dfeac",
+  "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/precision-state-frontier/FIXTURE.json",
+      "usage": "input",
+      "git_blob": "0aa9f7816378c3eb11ec2e3d63ed9e85cfaa893c",
+      "sha256": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8"
+    },
+    {
+      "path": "research/precision-state-frontier/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "79090050d47de95750b7321d89848143cc945abe",
+      "sha256": "f7e4d410cc108bc8b148ed8641c09be20c4c864fbc3908c533fa889b59dae341"
+    },
+    {
+      "path": "research/precision-state-frontier/README.md",
+      "usage": "provenance",
+      "git_blob": "9c21dc65e529bc234ddafc8683f311185b644c01",
+      "sha256": "0a62a71cea7e8ec40cf1a175b84b2d42cd81a3d94c7ab106ea7d6c765d75d8d2"
+    }
+  ]
+}
diff --git a/research/refined-native-recovery/TASK.json b/research/refined-native-recovery/TASK.json
new file mode 100644
index 0000000000..7d733006e2
--- /dev/null
+++ b/research/refined-native-recovery/TASK.json
@@ -0,0 +1,103 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "a7638a4ce2a29947457ae8d6bf8cd70a234dfeac",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Optimal two-stage recovery alphabet over all fixed mode-preserving integer unimodular frames, explicit rank-four source construction, full-output codec, and complementary all-depth parity-I theorem.",
+  "scope_change_reason": "The completed parity-I family led to parity-changing shears. A source-sized rank-four construction and independent Fourier proof settle the full mode-preserving class; no selected physical caller is discharged.",
+  "bottleneck_link": "Exact history accounting is required before numerical precision can be implemented reversibly. This result fixes composition-state accounting for the inherited rounded inverse interface; it does not improve a supplier invoice.",
+  "budget_minutes": 120,
+  "stop_rule": "Stop at the sharp mode-preserving two-stage theorem, explicit source frame, full-output codec and independent replay; preserve changed-output and unpriced physical costs, without expanding to mode-changing frames.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; CHAIN_PROOF.md; COST_SCOPE.md; generated RESULT.json; normal/optimized primary and two independent checkers; VALIDATION.md.",
+  "author": "@CubeJerry",
+  "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, implementation, independent proof/checker review, and writing.",
+  "open_questions": [
+    {
+      "question": "What is the sharp fiber for one mode-changing frame in the two-step refined chain?",
+      "why_it_matters": "It would extend recovery accounting beyond the mode-preserving subgroup.",
+      "first_step": "Derive the actual two-step coupled quotient congruences for one exact unimodular source frame.",
+      "blocked_by": "The scalar common-mode recursion no longer applies."
+    },
+    {
+      "question": "Can a named physical caller realize this frame/grid contract with favorable paid recovery cost?",
+      "why_it_matters": "An optimal information alphabet is not a reversible implementation or supplier saving.",
+      "first_step": "Bind exact input/output grids, finite range, quotient workspace and restoration schedule at one actual caller.",
+      "blocked_by": "Unpriced arithmetic, routing, finite storage and cleanup; no actual caller supplied."
+    },
+    {
+      "question": "What is the optimal recovery alphabet for longer parity-changing chains or nonuniform refinement?",
+      "why_it_matters": "The sharp all-depth formula here covers the parity-I class only.",
+      "first_step": "Derive the complete joint quotient parity constraints for one explicit three-step source chain.",
+      "blocked_by": "The direct three-quotient zero-Fourier majorant fails: character (0,1,1) is -14 at s=2 versus13 at s=0. This is a method limitation, not a proof that a three-stage optimum fails."
+    }
+  ],
+  "track_seed": 64,
+  "originating_pr": 5444,
+  "overlap": {
+    "root_survey": "Read current selected/review/priorities, metadata archive and relevant #5444 descendants. Targeted #5444 search located #5530 on numerator width, a distinct scope; no located later resolution of this restricted composition.",
+    "limits": "Bounded survey, incomplete archive prose and unpublished work; no universal novelty claim.",
+    "coordination": "Lead maintains allocation; Discussion mutation unavailable. No public claim asserted."
+  },
+  "local_unpublished_development_ancestor": "f19fdfd69bb207d5f6f5e2c6f858b41029039ad1"
+}
diff --git a/research/refined-native-recovery/VALIDATION.md b/research/refined-native-recovery/VALIDATION.md
new file mode 100644
index 0000000000..91a2c8e9ff
--- /dev/null
+++ b/research/refined-native-recovery/VALIDATION.md
@@ -0,0 +1,126 @@
+# Executed verification and boundaries
+
+Environment: Linux, CPython 3.12.14, standard library only. Scientific input:
+`research/precision-state-frontier/FIXTURE.json`, Git blob
+`0aa9f7816378c3eb11ec2e3d63ed9e85cfaa893c`, SHA256
+`2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8`.
+Its bytes are unchanged from canonical base
+`a7638a4ce2a29947457ae8d6bf8cd70a234dfeac`.
+
+## Registered execution
+
+Executed successfully from the repository root:
+
+```sh
+python -B scripts/research_package.py --package research/refined-native-recovery --check-only
+python -B scripts/research_package.py --package research/refined-native-recovery
+```
+
+All six registered commands pass: primary `verify.py`, separately written
+`independent_check.py`, and separately written `independent_optimal.py`, each
+under ordinary and optimized (`-O`) Python with isolation, warnings-as-errors
+and bytecode disabled. Standalone ordinary primary and optimal-independent
+runs also pass. Optimized execution retains explicit exceptions as gates;
+acceptance never depends on Python assertions.
+
+The primary checker covers the complete source Gram matrix and 16-word code,
+248,283 scalar inputs for the finite-chain interval calculation, 224 parity-I
+frame-basis tests, 384 parity-I codec roundtrips and twelve rejecting controls.
+For the optimal two-stage construction it additionally checks 224 inverse
+basis compositions, all 256 zero code-pair blocks, 144 arbitrary-output codec
+roundtrips over 48 distinct outputs (including first/last tags and 30-digit
+inputs),417 scalar parameters containing 70,277 total-quotient points, all 12
+joint-table shapes, and twelve rejecting controls. Thus the optimal codec
+has 400 complete encode/decode checks. A reachable norm 13 witness detects
+failure of inverse-frame-only output restoration. Four additional reachable
+inputs check the observer spanning matrix and its determinant 5,250,000.
+The exact three-stage character control returns 13 at s=0 and −14 at s=2;
+this only limits an attempted proof-method extension.
+
+The original independent checker imports no primary code. It checks 627
+scalar interval cases containing 495,891 integers, all 16 pair-parity coset
+counts, 224 frame basis cases, 288 actual source forward/reconstruction cases
+and six semantic controls. Its SHA256 is
+`34f157fa77df9843023e6b1edb4b35a0898c1b40ecf8b427f41c24db5c2baa6d`.
+
+The optimal independent checker also imports no primary code. It reads the
+pinned fixture, independently transcribes the frame, and compares declared
+constants through AST parsing without executing the primary construction.
+Its different methods directly enumerate quotient trajectories and 112-bit
+binary images rather than reuse the primary interval, rank or codec code.
+It covers all 20,001 scalar parameters in [-10000,10000], all 65,536 binary
+quotient pairs grouped into 256 actual source syndromes, 224 inverse basis
+compositions and 1,152 source-sized forward/reverse checks. The latter include
+three representatives of each 256 zero block and 384 other trajectories with
+384 distinct outputs. Forty-eight vectors use deterministic seed 908173;
+this is bounded verification, not a randomized optimization search. Removing
+one frame column creates image intersection size 2 and increases the zero
+count to 5,201,116,111,850,821. Seven explicit semantic controls detect mode,
+inverse, overlap, tie, domination, omitted-frame and identity-optimality
+errors. Its SHA256 is
+`ca8c10a15c33ea802132433842d8c42c8db51023ebbcb78e7bae43b779433772`.
+
+The independently written mathematical review is retained in REVIEW.md,
+with exact hashes of the reviewed proof and implementation. This is AI-assisted
+independent reasoning and code, not independent human acceptance or a formal
+proof-kernel certificate. All finite domains above corroborate the written
+universal arguments; none is substituted for an all-integer proof.
+
+## Actual-file negative controls
+
+Twenty-eight mutated-file executions on isolated temporary copies reject:
+11 semantic mutations in both Python modes, plus changed fixture bytes in
+all three checkers in both modes. The semantic mutations omit initial
+refinement, reverse the scalar quotient sign, change the denominator,
+change the code enumerator, reverse the parity-I inverse sign, remove its
+parity constraint, change a rank-four source coefficient, reverse the
+rank-four inverse sign, omit the output syndrome, omit the quotient
+syndrome, and corrupt the optimal count. Every mutation compiles as valid
+Python; rejection is a mathematical or codec gate, not a syntax failure.
+The fixture-byte control preserves parseable JSON but violates its pin.
+
+The source construction was separately corroborated before integration by
+all 674 owner-axis/large-input trajectories and 768 zero-block witnesses in
+both modes. The independent cost audit also checked the reachable output
+defect and observer matrix in both modes. These extra development checks
+are disclosed for provenance; the registered package commands above are
+the supported reproduction path.
+
+## Reproduction and unrun obligations
+
+RESULT.json is generated by `verify.py --output RESULT.json`. It binds the
+source and all package files except itself and this execution record, avoiding
+circular hashing. The all-depth parity-I counts are labelled separately
+from the optimal two-stage count. Exact package transport/export checks
+are recorded below.
+
+Not run or claimed: selected cold replay, physical/native caller admission,
+complete supplier invoice, bit/tape realization, Lean or another proof
+kernel, hosted CI or independent human review. The deliberately shallow
+partial checkout prevents a full-history preflight; no unshallow fetch was
+performed just for that check. Base-parent and actual consumed input
+identities are verified separately from any complete ancestry assertion.
+
+AST parsing, tabnanny, and `git diff --check` pass on the final code. No
+external static analyzer or repository-wide unrelated suite is claimed.
+
+## Final byte transport and offline export
+
+`check_research_commit.py --check-modes` passes for all 17 package files and
+the one declared fixture. The official `export_research_package.py export`
+and `check --check-inputs` commands pass, authenticating the same 18 source
+and input files. The export also includes its integrity manifest.
+
+All six direct commands additionally pass from the read-only Git-free export
+with an empty PATH. All 19 exported files retain their exact hashes and modes;
+no output or bytecode is generated inside the bundle. The final publication
+commit changes only this research package relative to the canonical base.
+The earlier local, unpublished development commit is retained as an ancestor;
+no source or upstream branch was rewritten. Generated bytecode discovered by
+the byte-inventory preflight was removed before the successful comparison.
+
+Full source-history validation remains deliberately unrun because the
+acquisition is shallow. The canonical base is the development ancestor's
+parent, and the consumed fixture blob and bytes match that base directly.
+No full-history or hosted-CI equivalence is inferred from these transport
+checks.
diff --git a/research/refined-native-recovery/VERIFY.json b/research/refined-native-recovery/VERIFY.json
new file mode 100644
index 0000000000..2a7bfb2a1c
--- /dev/null
+++ b/research/refined-native-recovery/VERIFY.json
@@ -0,0 +1,86 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/precision-state-frontier/FIXTURE.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact source geometry, refined fiber/count or independent quotient replay, and rejecting semantic controls; all-depth claim proved separately."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact source geometry, refined fiber/count or independent quotient replay, and rejecting semantic controls; all-depth claim proved separately."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/independent_check.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact source geometry, refined fiber/count or independent quotient replay, and rejecting semantic controls; all-depth claim proved separately."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/independent_check.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact source geometry, refined fiber/count or independent quotient replay, and rejecting semantic controls; all-depth claim proved separately."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/independent_optimal.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent scalar quotient and Fourier census; direct binary image separation/coset count; source-sized construction and actual inverse trajectories; meaningful negative controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/independent_optimal.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent scalar quotient and Fourier census; direct binary image separation/coset count; source-sized construction and actual inverse trajectories; meaningful negative controls."
+    }
+  ]
+}
diff --git a/research/refined-native-recovery/construction.py b/research/refined-native-recovery/construction.py
new file mode 100644
index 0000000000..103bf000b5
--- /dev/null
+++ b/research/refined-native-recovery/construction.py
@@ -0,0 +1,131 @@
+"""Explicit source-sized rank-four mode-preserving shear.
+
+Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0.
+This module constructs a mathematical integer map, not a physical cost claim.
+"""
+from itertools import product
+
+SELECTORS = (0, 1, 2, 4)
+COLUMNS = (
+    ((64, 1), (65, -1), (96, -1), (97, 1)),
+    ((10, 1), (11, -1), (62, 1), (63, -1)),
+    ((14, 1), (15, -1), (41, 1), (42, -1)),
+    ((18, 1), (19, -1), (39, 1), (40, -1)),
+)
+DUAL_ROWS = ((4, 64), (10, 70), (14, 52), (18, 54))
+
+
+def require(value, message):
+    if not value:
+        raise ValueError(message)
+
+
+def matrices():
+    e = [[int(i == k) for i in range(112)] for k in SELECTORS]
+    v = [[0] * 4 for _ in range(112)]
+    l = [[int(i in pair) for i in range(112)] for pair in DUAL_ROWS]
+    for j, column in enumerate(COLUMNS):
+        for i, value in column:
+            v[i][j] = value
+    return e, v, l
+
+
+def transpose(m):
+    return list(map(list, zip(*m)))
+
+
+def multiply(a, b):
+    cols = transpose(b)
+    return [[sum(x*y for x,y in zip(row,col)) for col in cols] for row in a]
+
+
+def f2rank(rows):
+    pivots = {}
+    for row in rows:
+        value = sum((x & 1) << j for j,x in enumerate(row))
+        while value:
+            pivot = value.bit_length()-1
+            if pivot in pivots:
+                value ^= pivots[pivot]
+            else:
+                pivots[pivot] = value
+                break
+    return len(pivots)
+
+
+def validate(m, e, v, l):
+    require(len(m) == 112 and all(len(row) == 8 for row in m), 'matrix shape')
+    require(len(e) == len(l) == 4 and all(len(row) == 112 for row in e+l), 'row shapes')
+    require(len(v) == 112 and all(len(row) == 4 for row in v), 'column shape')
+    require(all(type(x) is int for a in (m,e,v,l) for row in a for x in row), 'integer matrices')
+    require(multiply(transpose(m),m) == [[56*int(i==j) for j in range(8)] for i in range(8)], 'source Gram')
+    require(multiply(transpose(m),v) == [[0]*4 for _ in range(8)], 'exact native-mode kernel')
+    require(multiply(e,v) == [[0]*4 for _ in range(4)], 'nilpotent shear')
+    require(all(x%2 == 0 for row in multiply(l,m) for x in row), 'dual annihilator')
+    require(multiply(l,v) == [[int(i==j) for j in range(4)] for i in range(4)], 'dual quotient basis')
+    require(f2rank(m) == 4 and f2rank(multiply(e,m)) == 4, 'full code row space')
+    require(f2rank([a+b for a,b in zip(m,v)]) == 8, 'quotient independence')
+    code = [mask for mask in range(256) if all(sum(x*((mask>>j)&1) for j,x in enumerate(row))%2==0 for row in m)]
+    em = [sum((x&1)<<j for j,x in enumerate(row)) for row in multiply(e,m)]
+    rowcode = {0}
+    for row in em:
+        rowcode |= {x^row for x in rowcode}
+    require(set(code) == rowcode and len(code) == 16, 'self-dual Hamming code equality')
+    require(all((x&y).bit_count()%2 == 0 for x,y in product(code,repeat=2)), 'code orthogonality')
+    return code
+
+
+def apply_u(x, inverse=False):
+    require(len(x) == 112 and all(type(a) is int for a in x), 'integer owner vector')
+    out = list(x)
+    sign = -1 if inverse else 1
+    for source, column in zip(SELECTORS,COLUMNS):
+        for destination,value in column:
+            out[destination] += sign*value*x[source]
+    return out
+
+
+def project(m,x):
+    return [sum(row[j]*a for row,a in zip(m,x)) for j in range(8)]
+
+
+def lift(m,q):
+    return [sum(a*b for a,b in zip(row,q)) for row in m]
+
+
+def nearest(n):
+    require(type(n) is int, 'round exact integer')
+    return ((abs(n)+26)//52)*(1 if n>=0 else -1)
+
+
+def kernel(m,x):
+    correction=lift(m,[nearest(a) for a in project(m,x)])
+    return [a-b for a,b in zip(x,correction)]
+
+
+def forward(m,x):
+    return kernel(m,apply_u(kernel(m,[2*a for a in x])))
+
+
+def scalar_step(s,t):
+    return t-nearest(s+56*t)
+
+
+def inverse_from_total(m,y,total):
+    require(len(y)==112 and len(total)==8 and all(type(a) is int for a in y+total), 'exact inverse dimensions')
+    s=project(m,y)
+    q2=[scalar_step(a,t) for a,t in zip(s,total)]
+    require(all(scalar_step(a,q)==0 for a,q in zip(s,q2)), 'scalar total outside two-step inverse')
+    q1=[t-q for t,q in zip(total,q2)]
+    back=apply_u([a+b for a,b in zip(y,lift(m,q2))],inverse=True)
+    numerator=[a+b for a,b in zip(back,lift(m,q1))]
+    require(all(a%2==0 for a in numerator), 'nonintegral inverse')
+    x=[a//2 for a in numerator]
+    require(forward(m,x)==y, 'literal two-step inverse replay')
+    return x
+
+
+def total_for_input(m,x,y):
+    delta=[2*a-b for a,b in zip(project(m,x),project(m,y))]
+    require(all(a%56==0 for a in delta), 'integer total quotient')
+    return [a//56 for a in delta]
diff --git a/research/refined-native-recovery/independent_check.py b/research/refined-native-recovery/independent_check.py
new file mode 100644
index 0000000000..e7b6c04227
--- /dev/null
+++ b/research/refined-native-recovery/independent_check.py
@@ -0,0 +1,262 @@
+#!/usr/bin/env python3
+"""Independent exact checks of the refined native recovery chain.
+
+No primary recovery implementation is imported. Literal quotient trajectories,
+scalar interval enumeration and pair-parity convolution provide separate checks.
+Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0.
+Source matrix and one-step construction: zxv #5444, Ali Romman #5323 and lineage.
+"""
+import argparse
+import hashlib
+import json
+from collections import Counter
+from pathlib import Path
+
+
+SOURCE_SHA256 = "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8"
+V = {1: 1, 12: 1, 0: -1, 16: -1}
+W = {0: 1, 8: 1, 2: -1, 6: -1}
+FRAMES = ((V, 2), (W, 3), (V, 2))
+
+
+def check(ok, label):
+    if not ok:
+        raise ValueError(label)
+
+
+def rounded(n):
+    magnitude = (abs(n) + 26) // 52
+    return magnitude if n >= 0 else -magnitude
+
+
+def scalar(s, q):
+    return q - rounded(s + 56 * q)
+
+
+def scalar_power(s, q, depth):
+    for _ in range(depth):
+        q = scalar(s, q)
+    return q
+
+
+def load_matrix(path):
+    raw = path.read_bytes()
+    check(hashlib.sha256(raw).hexdigest() == SOURCE_SHA256, "source hash")
+    columns = json.loads(raw)["mode_columns"]
+    check(len(columns) == 8 and all(len(c) == 112 for c in columns), "shape")
+    matrix = [list(row) for row in zip(*columns)]
+    check(all(type(x) is int for row in matrix for x in row), "exact integers")
+    check(gram_ok(matrix), "source Gram")
+    return matrix
+
+
+def gram_ok(matrix):
+    return all(sum(row[i] * row[j] for row in matrix) == 56 * (i == j)
+               for i in range(8) for j in range(8))
+
+
+def modes(matrix, x):
+    return [sum(matrix[i][j] * x[i] for i in range(112)) for j in range(8)]
+
+
+def lift(matrix, q):
+    return [sum(row[j] * q[j] for j in range(8)) for row in matrix]
+
+
+def shifted(x, frame, reverse=False):
+    null, source = frame
+    y = list(x)
+    amount = (-2 if reverse else 2) * x[source]
+    for index, value in null.items():
+        y[index] += amount * value
+    return y
+
+
+def native(matrix, x):
+    q = [rounded(z) for z in modes(matrix, x)]
+    correction = lift(matrix, q)
+    return [a - b for a, b in zip(x, correction)], q
+
+
+def literal_chain(matrix, x, frames):
+    current = [2 * z for z in x]
+    total = [0] * 8
+    for stage in range(len(frames) + 1):
+        if stage:
+            current = shifted(current, frames[stage - 1])
+        current, q = native(matrix, current)
+        total = [a + b for a, b in zip(total, q)]
+    return current, total
+
+
+def reverse_total(matrix, y, total, frames, omit_frames=False):
+    s = modes(matrix, y)
+    residual = list(total)
+    quotients = []
+    for _ in range(len(frames) + 1):
+        q = [rounded(a + 56 * b) for a, b in zip(s, residual)]
+        quotients.append(q)
+        residual = [a - b for a, b in zip(residual, q)]
+    check(residual == [0] * 8, "total quotient endpoint")
+    current = list(y)
+    for stage in range(len(quotients) - 1, -1, -1):
+        correction = lift(matrix, quotients[stage])
+        current = [a + b for a, b in zip(current, correction)]
+        if stage and not omit_frames:
+            current = shifted(current, frames[stage - 1], reverse=True)
+    check(all(x % 2 == 0 for x in current), "input integrality")
+    return [x // 2 for x in current]
+
+
+def source_code(matrix):
+    code = {0}
+    for row in matrix:
+        mask = sum((entry % 2) << j for j, entry in enumerate(row))
+        code |= {word ^ mask for word in tuple(code)}
+    check(len(code) == 16, "source binary rank")
+    check(all((a & b).bit_count() % 2 == 0 for a in code for b in code),
+          "source code self-dual")
+    check(Counter(x.bit_count() for x in code) == {0: 1, 4: 14, 8: 1},
+          "source weight enumerator")
+    return sorted(code)
+
+
+def scalar_census():
+    cases = 0
+    checked_inputs = 0
+    for s in range(-104, 105):
+        interval = [0]
+        for depth in range(1, 4):
+            low = -((26 + s + 52 * interval[-1]) // 4)
+            high = (26 - s - 52 * interval[0]) // 4
+            scan = range(low - 1, high + 2)
+            found = [q for q in scan if scalar_power(s, q, depth) == 0]
+            check(found and found == list(range(found[0], found[-1] + 1)),
+                  "scalar preimage is not an interval")
+            check(len(found) <= 13 ** depth, "scalar cardinality")
+            if s == 0:
+                radius = (13 ** depth - 1) // 2
+                check(found == list(range(-radius, radius + 1)), "sharp fiber")
+            interval = found
+            cases += 1
+            checked_inputs += len(scan)
+    return cases, checked_inputs
+
+
+def pair_convolution(code):
+    pairs = []
+    totals = []
+    for q2 in range(-7, 8):
+        if rounded(56 * q2) != q2:
+            continue
+        for q1 in range(-14 * q2 - 7, -14 * q2 + 8):
+            if rounded(56 * (q1 + q2)) == q1:
+                pairs.append((q1 & 1, q2 & 1))
+                totals.append(q1 + q2)
+    check(sorted(totals) == list(range(-84, 85)), "169 distinct quotient sums")
+    table = Counter(pairs)
+    check(table == {(0, 0): 49, (0, 1): 42, (1, 0): 42, (1, 1): 36},
+          "literal pair-parity census")
+    parity = [sum(n for (a, b), n in table.items() if (a ^ b) == p)
+              for p in (0, 1)]
+    cosets = {tuple(sorted(word ^ mask for word in code)) for mask in range(256)}
+    counts = []
+    for coset in sorted(cosets):
+        count = 0
+        for word in coset:
+            term = 1
+            for j in range(8):
+                term *= parity[(word >> j) & 1]
+            count += term
+        counts.append(count)
+    expected = (13 ** 16 + 14 * 13 ** 8 + 1) // 16
+    check(len(cosets) == 16 and max(counts) == expected, "exact coset maximum")
+    return table, counts, expected
+
+
+def frame_census(matrix):
+    for frame in FRAMES[:2]:
+        null, source = frame
+        vector = [null.get(i, 0) for i in range(112)]
+        check(modes(matrix, vector) == [0] * 8 and null.get(source, 0) == 0,
+              "mode-preserving unimodular transvection")
+        for j in range(112):
+            e = [int(i == j) for i in range(112)]
+            changed = shifted(e, frame)
+            check(shifted(changed, frame, True) == e, "frame inverse")
+            check(modes(matrix, changed) == modes(matrix, e), "mode preservation")
+            check(all((a - b) % 2 == 0 for a, b in zip(e, changed)), "parity")
+    e3 = [int(i == 3) for i in range(112)]
+    uv = shifted(shifted(e3, FRAMES[1]), FRAMES[0])
+    vu = shifted(shifted(e3, FRAMES[0]), FRAMES[1])
+    check([a - b for a, b in zip(uv, vu)] == [-4 * V.get(i, 0) for i in range(112)],
+          "two frames genuinely fail to commute")
+    x = [52 * int(i == 2) for i in range(112)]
+    ku, _ = native(matrix, shifted(x, FRAMES[0]))
+    k, _ = native(matrix, x)
+    uk = shifted(k, FRAMES[0])
+    check([a - b for a, b in zip(ku, uk)] == [8 * V.get(i, 0) for i in range(112)],
+          "frame genuinely fails to commute with native map")
+    return 224
+
+
+def roundtrip_census(matrix, code):
+    checks = 0
+    omitted_frame_rejected = False
+    for depth in range(1, 5):
+        frames = FRAMES[:depth - 1]
+        radius = (13 ** depth - 1) // 2
+        for word in code:
+            for choice in range(3):
+                total = [(-radius + ((word >> j) & 1)) *
+                         (-1 if choice == 1 or (choice == 2 and j % 2) else 1)
+                         for j in range(8)]
+                x = reverse_total(matrix, [0] * 112, total, frames)
+                y, actual = literal_chain(matrix, x, frames)
+                check(y == [0] * 112 and actual == total, "attaining reconstruction")
+                if depth > 1:
+                    mutant = reverse_total(matrix, y, total, frames, True)
+                    omitted_frame_rejected |= literal_chain(matrix, mutant, frames)[0] != y
+                checks += 1
+        for seed in range(24):
+            x = [((i * (seed + 3) + seed * seed) % 107) - 53 for i in range(112)]
+            y, total = literal_chain(matrix, x, frames)
+            check(reverse_total(matrix, y, total, frames) == x, "arbitrary-output reconstruction")
+            check([2 * a - b for a, b in zip(modes(matrix, x), modes(matrix, y))]
+                  == [56 * q for q in total], "mode invariant")
+            checks += 1
+    check(omitted_frame_rejected, "omitted inverse-frame control did not reject")
+    return checks
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument("--source", type=Path,
+                        default=Path(__file__).resolve().parents[1] /
+                        "precision-state-frontier/FIXTURE.json")
+    args = parser.parse_args()
+    matrix = load_matrix(args.source)
+    code = source_code(matrix)
+    scalar_cases, scalar_inputs = scalar_census()
+    table, cosets, maximum = pair_convolution(code)
+    frames = frame_census(matrix)
+    roundtrips = roundtrip_census(matrix, code)
+    altered = [row[:] for row in matrix]
+    altered[0][0] += 1
+    check(not gram_ok(altered), "altered Gram control did not reject")
+    check(rounded(26) == 1 and rounded(-26) == -1, "half-away tie controls")
+    check(maximum != 169 ** 8, "omitted lattice constraint control")
+    check(maximum != ((13 ** 8 + 14 * 13 ** 4 + 1) // 16) * 13 ** 8,
+          "naive multiplication control")
+    check(scalar(0, 13) == -1 and scalar(0, -13) == 1, "wrong recursion sign")
+    result = {"scalar_interval_cases": scalar_cases, "scalar_inputs": scalar_inputs,
+              "pair_parities": {str(k): v for k, v in sorted(table.items())},
+              "coset_counts": sorted(cosets), "two_step_maximum": maximum,
+              "frame_basis_checks": frames, "source_sized_roundtrips": roundtrips,
+              "controls": 6, "source_sha256": SOURCE_SHA256}
+    print(json.dumps(result, sort_keys=True))
+    print("PASS_INDEPENDENT_REFINED_NATIVE_RECOVERY")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/research/refined-native-recovery/independent_optimal.py b/research/refined-native-recovery/independent_optimal.py
new file mode 100644
index 0000000000..d008190bd2
--- /dev/null
+++ b/research/refined-native-recovery/independent_optimal.py
@@ -0,0 +1,279 @@
+#!/usr/bin/env python3
+"""Independent source-sized check of the two-stage optimal frame.
+
+No imports of the construction, codec, or primary verifier. This checker uses
+literal integer quotient enumeration and direct binary image enumeration.
+Finite replay corroborates, and does not replace, the all-integer proof.
+Prepared for @CubeJerry with substantial OpenAI Codex assistance.
+Apache-2.0.
+"""
+import argparse
+import ast
+from collections import Counter
+import hashlib
+import itertools
+import json
+from math import prod
+from pathlib import Path
+import random
+
+SOURCE_SHA = '2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8'
+SELECT = (0, 1, 2, 4)
+SPARSE = (
+    ((64, 1), (65, -1), (96, -1), (97, 1)),
+    ((10, 1), (11, -1), (62, 1), (63, -1)),
+    ((14, 1), (15, -1), (41, 1), (42, -1)),
+    ((18, 1), (19, -1), (39, 1), (40, -1)),
+)
+DUALS = ((4, 64), (10, 70), (14, 52), (18, 54))
+CAPS = (169, 1, 13, 13)
+CHARACTERS = ((0, 0), (1, 0), (0, 1), (1, 1))
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def dot(x, y):
+    return sum(a * b for a, b in zip(x, y))
+
+
+def add(x, y):
+    return [a + b for a, b in zip(x, y)]
+
+
+def round52(n):
+    # Quotient/remainder implementation, including signed half ties.
+    quotient, remainder = divmod(abs(n), 52)
+    result = quotient + (2 * remainder >= 52)
+    return result if n >= 0 else -result
+
+
+def quotient_set(s):
+    # The closed residual interval supplies candidates only; every accepted
+    # candidate is tested with the original rounded identity.
+    lo = -((26 + s) // 4)
+    hi = (26 - s) // 4
+    return [q for q in range(lo, hi + 1) if round52(s + 56 * q) == q]
+
+
+def joint_table(s):
+    table = [[0, 0], [0, 0]]
+    totals = set()
+    for last in quotient_set(s):
+        for first in quotient_set(s + 56 * last):
+            total = first + last
+            need(total not in totals, 'two quotient pairs share a total')
+            totals.add(total)
+            step = total - round52(s + 56 * total)
+            need(step == last and step - round52(s + 56 * step) == 0,
+                 'literal total dynamics disagree with quotient enumeration')
+            table[total & 1][last & 1] += 1
+    need(totals and max(totals) - min(totals) + 1 == len(totals),
+         'two-stage total set is not an interval')
+    return table
+
+
+def walsh(table):
+    return tuple(sum((-1) ** (a * p + b * q) * table[p][q]
+                     for p, q in itertools.product(range(2), repeat=2))
+                 for a, b in CHARACTERS)
+
+
+def apply_frame(x, inverse=False, columns=SPARSE, selectors=SELECT):
+    result = list(x)
+    factor = -1 if inverse else 1
+    for source, col in zip(selectors, columns):
+        for target, coefficient in col:
+            result[target] += factor * coefficient * x[source]
+    return result
+
+
+def bitvector(vector):
+    return sum((value & 1) << i for i, value in enumerate(vector))
+
+
+def load_source(path):
+    blob = Path(path).read_bytes()
+    need(hashlib.sha256(blob).hexdigest() == SOURCE_SHA, 'source SHA mismatch')
+    raw = json.loads(blob)['mode_columns']
+    need(len(raw) == 8 and all(len(col) == 112 for col in raw), 'source dimensions')
+    need(all(type(v) is int for col in raw for v in col), 'noninteger source')
+    return list(zip(*raw)), raw
+
+
+def check_declared_constants(path):
+    tree = ast.parse(Path(path).read_text())
+    actual = {}
+    for node in tree.body:
+        if isinstance(node, ast.Assign) and len(node.targets) == 1:
+            target = node.targets[0]
+            if isinstance(target, ast.Name) and target.id in ('SELECTORS', 'COLUMNS', 'DUAL_ROWS'):
+                actual[target.id] = ast.literal_eval(node.value)
+    need(actual == {'SELECTORS': SELECT, 'COLUMNS': SPARSE, 'DUAL_ROWS': DUALS},
+         'primary frame constants differ from independently checked witness')
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--source', type=Path, default=Path(__file__).resolve().parent.parent / 'precision-state-frontier' / 'FIXTURE.json')
+    parser.add_argument('--construction', type=Path, default=Path(__file__).resolve().with_name('construction.py'))
+    args = parser.parse_args()
+    matrix, columns = load_source(args.source)
+    check_declared_constants(args.construction)
+    projection = lambda x: [dot(col, x) for col in columns]
+    lift = lambda q: [dot(row, q) for row in matrix]
+    kernel = lambda x: add(x, [-v for v in lift([round52(a) for a in projection(x)])])
+    forward = lambda x: kernel(apply_frame(kernel([2 * a for a in x])))
+
+    for j, col in enumerate(columns):
+        need(projection(col) == [56 * (i == j) for i in range(8)], 'source Gram')
+    vcols = []
+    for sparse in SPARSE:
+        dense = [0] * 112
+        for i, coefficient in sparse:
+            dense[i] = coefficient
+        vcols.append(dense)
+        need(projection(dense) == [0] * 8, 'exact mode preservation')
+        need(all(dense[i] == 0 for i in SELECT), 'E V is not zero')
+    for i, pair in enumerate(DUALS):
+        need(all(sum(matrix[k][j] for k in pair) % 2 == 0 for j in range(8)), 'dual does not annihilate M')
+        need([sum(v[k] for k in pair) for v in vcols] == [int(i == j) for j in range(4)], 'dual V is not identity')
+    for i in range(112):
+        e = [int(i == j) for j in range(112)]
+        need(apply_frame(apply_frame(e), True) == e and apply_frame(apply_frame(e, True)) == e,
+             'integer inverse failure')
+        need(projection(apply_frame(e)) == projection(e), 'basis mode failure')
+
+    binary = [[(mask >> j) & 1 for j in range(8)] for mask in range(256)]
+    images = [bitvector(lift(q)) for q in binary]
+    moved = [bitvector(apply_frame(lift(q), True)) for q in binary]
+    need(len(set(images)) == len(set(moved)) == 16, 'binary source rank')
+    need(set(images) & set(moved) == {0}, 'binary image separation')
+    code = [i for i, image in enumerate(images) if image == 0]
+    need(len(code) == 16, 'code size')
+    need(Counter(c.bit_count() for c in code) == {0: 1, 4: 14, 8: 1}, 'source weight enumerator')
+    need(all((a & b).bit_count() % 2 == 0 for a in code for b in code), 'code self-orthogonality')
+    em_kernel = [q for q in range(256) if all(dot(matrix[k], binary[q]) % 2 == 0 for k in SELECT)]
+    need(em_kernel == code, 'selector code kernel')
+
+    # Full quotient census, not a sampled floating-point model.
+    exceptional = {}
+    for s in range(-10000, 10001):
+        q = quotient_set(s)
+        expected_length = 12 if s % 4 == 2 and abs(s) <= 26 else 13
+        need(len(q) == expected_length and q == list(range(q[0], q[-1] + 1)), 'scalar Q classification')
+        table = joint_table(s)
+        transform = walsh(table)
+        need(all(abs(a) <= b for a, b in zip(transform, CAPS)), 'Walsh cap failed')
+        if s in range(2, 31, 4):
+            exceptional[str(s)] = {'table': table, 'walsh': transform}
+    zero = joint_table(0)
+    need(zero == [[49, 36], [42, 42]] and walsh(zero) == CAPS, 'zero scalar count')
+
+    # Enumerate all binary q1,q2, group by literal 112-bit inverse syndrome.
+    # This counts all 256 zero-mode affine parity cosets without Fourier code.
+    weights = [prod(7 if bit == 0 else 6 for bit in q) for q in binary]
+    syndrome_counts = Counter()
+    for first in range(256):
+        for last in range(256):
+            syndrome_counts[images[first] ^ moved[last]] += weights[first] * weights[last]
+    one_stage = sum(weights[c] for c in code)
+    maximum = syndrome_counts[0]
+    need(len(syndrome_counts) == 256, 'combined binary rank')
+    need(maximum == max(syndrome_counts.values()) == one_stage ** 2 == 2601832488601921,
+         'optimal source count')
+    need((maximum - 1).bit_length() == 52, 'packed tag width')
+
+    # Reconstruct every zero-fiber parity block at three different corners.
+    # The full Cartesian count is exact; these are finite trajectory controls.
+    roundtrips = 0
+    for first in code:
+        for last in code:
+            for choice in range(3):
+                q2 = []
+                q1 = []
+                for j in range(8):
+                    choices2 = [q for q in range(-6, 7) if q % 2 == binary[last][j]]
+                    b = choices2[(0, len(choices2) // 2, -1)[choice]]
+                    choices1 = [q for q in range(-6, 7) if q % 2 == binary[first][j]]
+                    a = choices1[(0, len(choices1) // 2, -1)[choice]] - 14 * b
+                    q2.append(b)
+                    q1.append(a)
+                numerator = add(apply_frame(lift(q2), True), lift(q1))
+                need(all(a % 2 == 0 for a in numerator), 'zero block parity failure')
+                x = [a // 2 for a in numerator]
+                need(forward(x) == [0] * 112, 'zero block forward replay')
+                need(projection([2 * a for a in x]) == [56 * (a + b) for a, b in zip(q1, q2)], 'zero total pin')
+                roundtrips += 1
+
+    # Arbitrary outputs from literal source-sized inputs; no codec imported.
+    rng = random.Random(908173)
+    inputs = [[(1 if i == j else 0) * magnitude for i in range(112)]
+              for j in range(112) for magnitude in (-26, 1, 52)]
+    inputs.extend([[rng.randrange(-200, 201) for _ in range(112)] for _ in range(48)])
+    omitted_frame_detected = False
+    outputs = set()
+    for x in inputs:
+        y = forward(x)
+        outputs.add(tuple(y))
+        s = projection(y)
+        raw_total = [2 * a - b for a, b in zip(projection(x), s)]
+        need(all(a % 56 == 0 for a in raw_total), 'total quotient not integral')
+        total = [a // 56 for a in raw_total]
+        q2 = [t - round52(a + 56 * t) for a, t in zip(s, total)]
+        q1 = [t - q for t, q in zip(total, q2)]
+        need(all(q in quotient_set(a) and first in quotient_set(a + 56 * q)
+                 for a, q, first in zip(s, q2, q1)), 'reverse quotient membership')
+        numerator = add(apply_frame(add(y, lift(q2)), True), lift(q1))
+        need(numerator == [2 * a for a in x], 'actual inverse chronology')
+        omitted_frame_detected |= add(add(y, lift(q2)), lift(q1)) != numerator
+        roundtrips += 1
+
+    # Necessary separation is tested by deliberately restoring one overlap.
+    # All parity pairs have positive scalar weights, so every new nonzero
+    # image intersection contributes strictly more than the C x C baseline.
+    missing = SPARSE[:-1] + ((),)
+    badimages = [bitvector(apply_frame(lift(q), True, columns=missing)) for q in binary]
+    intersection = set(images) & set(badimages)
+    need(len(intersection) > 1, 'negative separation control has no overlap')
+    badzero = sum(weights[a] * weights[b] for a in range(256) for b in range(256)
+                  if images[a] == badimages[b])
+    need(badzero > maximum, 'positive extra overlap inputs not detected')
+    badcolumn = list(SPARSE)
+    badcolumn[0] = ((64, 2),) + SPARSE[0][1:]
+    badv = [0] * 112
+    for i, v in badcolumn[0]:
+        badv[i] = v
+    need(projection(badv) != [0] * 8, 'negative mode control survived')
+    badselectors = (64, 1, 2, 4)
+    e = [int(i == 64) for i in range(112)]
+    need(apply_frame(apply_frame(e, selectors=badselectors), True, selectors=badselectors) != e,
+         'negative inverse control survived')
+    need(round52(26) == 1 and round52(-26) == -1, 'half-away tie control')
+    need(min(sum(joint_table(2), [])) > min(sum(zero, [])), 'entrywise-domination false control')
+    need(omitted_frame_detected, 'omitted inverse frame was not detected')
+    identityzero = sum(weights[a] * weights[b] for a in range(256) for b in range(256)
+                       if images[a] == images[b])
+    need(identityzero > maximum, 'identity frame should not be optimal')
+
+    print(json.dumps({
+        'status': 'PASS_INDEPENDENT_OPTIMAL_FRAME', 'source_sha256': SOURCE_SHA,
+        'scalar_cases': 20001, 'scalar_domain': [-10000, 10000],
+        'exceptional_tables': exceptional, 'binary_quotient_pairs': 65536,
+        'affine_binary_cosets': len(syndrome_counts), 'source_image_intersection_size': 1,
+        'one_stage_states': one_stage, 'optimal_two_stage_states': maximum, 'tag_bits': 52,
+        'basis_inverse_checks': 224, 'zero_parity_blocks': 256,
+        'actual_forward_reverse_checks': roundtrips, 'distinct_sample_outputs': len(outputs),
+        'removed_column_intersection_size': len(intersection),
+        'removed_column_zero_states': badzero, 'identity_zero_states': identityzero,
+        'negative_controls': ['mode coefficient', 'inverse selector', 'image overlap',
+                              'half-away ties', 'entrywise domination', 'omitted inverse frame',
+                              'identity frame optimality'],
+        'scope': 'Exact finite checks plus source identities; universal Walsh proof is in PROOF.md; no physical cost or new kappa claim.'
+    }, indent=2, sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/refined-native-recovery/optimal_codec.py b/research/refined-native-recovery/optimal_codec.py
new file mode 100644
index 0000000000..5d1ebf6ab2
--- /dev/null
+++ b/research/refined-native-recovery/optimal_codec.py
@@ -0,0 +1,108 @@
+"""Exact 52-bit worst-case abstract codec for the explicit rank-four frame.
+
+For @CubeJerry, substantial OpenAI Codex assistance. Apache-2.0.
+The changed output contract and unpriced physical costs are explicit in PROOF.md.
+"""
+from itertools import product
+from math import prod
+
+import construction as c
+import recovery as r
+
+
+def max_states():
+    return ((13 ** 8 + 14 * 13 ** 4 + 1) // 16) ** 2
+
+
+def parity_pairs(matrix, output):
+    """The exact affine coset of C x C from the binary dual witnesses."""
+    syndrome = [sum(output[i] for i in pair) & 1 for pair in c.DUAL_ROWS]
+    adjusted = list(output)
+    for value, column in zip(syndrome, c.COLUMNS):
+        for i, coefficient in column:
+            adjusted[i] += value * coefficient
+    totals = r.parity_options(matrix, adjusted)
+    target = [(value + output[i]) & 1
+              for value, i in zip(syndrome, c.SELECTORS)]
+    masks = [sum((value & 1) << j for j, value in enumerate(matrix[i]))
+             for i in c.SELECTORS]
+    last = [q for q in range(256)
+            if all((q & row).bit_count() % 2 == bit
+                   for row, bit in zip(masks, target))]
+    return product(totals, last)
+
+
+def joint_cells(s):
+    low, high = r.total_interval(s, 2)
+    cells = {(p, q): [] for p, q in product(range(2), repeat=2)}
+    for total in range(low, high + 1):
+        cells[total & 1, r.scalar_step(s, total) & 1].append(total)
+    return cells
+
+
+def blocks(matrix, output):
+    r.require(len(output) == 112 and all(map(r.exact_int, output)),
+              "output must be an exact owner vector")
+    tables = [joint_cells(s) for s in r.project(matrix, output)]
+    result = []
+    for p, q in parity_pairs(matrix, output):
+        cells = [table[(p >> j) & 1, (q >> j) & 1]
+                 for j, table in enumerate(tables)]
+        count = prod(map(len, cells))
+        if count:
+            result.append(((p, q), cells, count))
+    return result
+
+
+def fiber_count(matrix, output):
+    return sum(count for _, _, count in blocks(matrix, output))
+
+
+def unrank_total(matrix, output, tag):
+    r.require(r.exact_int(tag) and tag >= 0, "invalid optimal recovery tag")
+    for _, cells, count in blocks(matrix, output):
+        if tag >= count:
+            tag -= count
+            continue
+        total = [0] * 8
+        for j in range(7, -1, -1):
+            tag, index = divmod(tag, len(cells[j]))
+            total[j] = cells[j][index]
+        r.require(tag == 0, "unconsumed optimal recovery tag")
+        return total
+    raise ValueError("tag exceeds the actual optimal-frame output fiber")
+
+
+def rank_total(matrix, output, total):
+    r.require(len(total) == 8 and all(map(r.exact_int, total)),
+              "total must be eight exact integers")
+    s = r.project(matrix, output)
+    p = sum((value & 1) << j for j, value in enumerate(total))
+    q = sum((r.scalar_step(a, b) & 1) << j
+            for j, (a, b) in enumerate(zip(s, total)))
+    offset = 0
+    for pair, cells, count in blocks(matrix, output):
+        if pair != (p, q):
+            offset += count
+            continue
+        rank = 0
+        for value, cell in zip(total, cells):
+            r.require(value in cell, "total outside its joint scalar cell")
+            rank = rank * len(cell) + cell.index(value)
+        return offset + rank
+    raise ValueError("total fails the optimal-frame output syndrome")
+
+
+def decode(matrix, output, tag):
+    c.validate(matrix, *c.matrices())
+    total = unrank_total(matrix, output, tag)
+    return c.inverse_from_total(matrix, list(output), total)
+
+
+def encode(matrix, vector):
+    c.validate(matrix, *c.matrices())
+    r.require(len(vector) == 112 and all(map(r.exact_int, vector)),
+              "input must be an exact owner vector")
+    output = c.forward(matrix, vector)
+    total = c.total_for_input(matrix, vector, output)
+    return output, rank_total(matrix, output, total)
diff --git a/research/refined-native-recovery/optimal_verify.py b/research/refined-native-recovery/optimal_verify.py
new file mode 100644
index 0000000000..3ee4379c4f
--- /dev/null
+++ b/research/refined-native-recovery/optimal_verify.py
@@ -0,0 +1,193 @@
+"""Exact source, full-output codec, and Fourier-bound corroboration.
+
+For @CubeJerry, substantial OpenAI Codex assistance. Apache-2.0.
+The universal mathematical proof is PROOF.md; this is bounded validation.
+"""
+from copy import deepcopy
+from itertools import product
+
+import construction as c
+import optimal_codec as o
+import recovery as r
+
+
+def source_checks(matrix):
+    c.validate(matrix, *c.matrices())
+    for i in range(112):
+        x = [int(i == j) for j in range(112)]
+        r.require(c.apply_u(c.apply_u(x), True) == x, "left frame inverse")
+        r.require(c.apply_u(c.apply_u(x, True)) == x, "right frame inverse")
+        r.require(c.project(matrix, c.apply_u(x)) == c.project(matrix, x),
+                  "rank-four frame changed modes")
+    return {"rank_four_basis_inverse_checks": 224}
+
+
+def walsh_checks():
+    points, tables = 0, set()
+    for s in range(-208, 209):
+        cells = o.joint_cells(s)
+        counts = tuple(len(cells[p, q]) for p, q in product(range(2), repeat=2))
+        tables.add(counts)
+        for (a, b), bound in zip(((0, 0), (1, 0), (0, 1), (1, 1)),
+                                 (169, 1, 13, 13)):
+            value = sum((-1) ** (a * p + b * q) * len(cells[p, q])
+                        for p, q in product(range(2), repeat=2))
+            r.require(abs(value) <= bound, "absolute Fourier bound failed")
+        points += sum(counts)
+    r.require(len(tables) == 12, "scalar tie-table coverage changed")
+    return {"walsh_scalar_parameters": 417, "walsh_scalar_points": points,
+            "distinct_joint_tables": 12}
+
+
+def zero_codec_checks(matrix):
+    zero, offset, cases = [0] * 112, 0, 0
+    parts = o.blocks(matrix, zero)
+    r.require(len(parts) == 256, "rank-four code pair partition changed")
+    for _, _, size in parts:
+        tag = offset + size // 2
+        x = o.decode(matrix, zero, tag)
+        r.require(o.encode(matrix, x) == (zero, tag), "zero block roundtrip")
+        offset += size
+        cases += 1
+    r.require(offset == o.max_states() == 2601832488601921,
+              "sharp optimal-frame count changed")
+    r.require((offset - 1).bit_length() == 52, "optimal packed width changed")
+    return {"zero_code_pair_blocks": cases, "optimal_states": offset,
+            "optimal_packed_bits": 52}
+
+
+def arbitrary_codec_checks(matrix):
+    outputs = set()
+    for sample in range(48):
+        x = [((sample + 3) * (i * i + 17) % 127) - 63 for i in range(112)]
+        if sample == 47:
+            x = [((-1) ** i) * (10 ** 30 + i) for i in range(112)]
+        y, tag = o.encode(matrix, x)
+        outputs.add(tuple(y))
+        r.require(o.decode(matrix, y, tag) == x, "arbitrary output roundtrip")
+        count = o.fiber_count(matrix, y)
+        r.require(0 < count <= o.max_states(), "arbitrary output maximum")
+        for edge in (0, count - 1):
+            decoded = o.decode(matrix, y, edge)
+            r.require(o.encode(matrix, decoded) == (y, edge),
+                      "arbitrary output endpoint rank")
+    r.require(len(outputs) == 48, "nonzero-output coverage collapsed")
+    return {"distinct_arbitrary_outputs": len(outputs),
+            "arbitrary_output_codec_roundtrips": 144}
+
+
+def rejected(function, label):
+    try:
+        function()
+    except ValueError:
+        return 1
+    raise ValueError("control was accepted: " + label)
+
+
+def matrix_controls(matrix):
+    e, v, ell = c.matrices()
+    count = 0
+    for name in ("kernel", "nilpotence", "dual", "quotient", "code"):
+        ee, vv, ll = deepcopy((e, v, ell))
+        if name == "kernel":
+            vv[64][0] = 2
+        elif name == "nilpotence":
+            ee[0][64] = 1
+        elif name == "dual":
+            ll[0][0] = 1
+        elif name == "quotient":
+            for row in vv:
+                row[1] = row[0]
+        else:
+            ee[3] = list(ee[0])
+        count += rejected(lambda: c.validate(matrix, ee, vv, ll), name)
+    return count
+
+
+def controls(matrix):
+    zero = [0] * 112
+    cases = [(lambda: o.decode(matrix, zero, -1), "negative tag"),
+             (lambda: o.decode(matrix, zero, o.max_states()), "large tag"),
+             (lambda: o.decode(matrix, zero, True), "Boolean tag"),
+             (lambda: o.encode(matrix, [0.0] * 112), "inexact input"),
+             (lambda: c.inverse_from_total(matrix, zero, [1] + [0] * 7),
+              "nonintegral total")]
+    count = matrix_controls(matrix)
+    count += sum(rejected(function, label) for function, label in cases)
+    cells = o.joint_cells(2)
+    r.require(min(map(len, cells.values())) > 36,
+              "false entrywise-domination negative control disappeared")
+    unreachable = [0] * 112
+    unreachable[3] = 1
+    r.require(o.fiber_count(matrix, unreachable) == 0,
+              "outside-image output accepted")
+    return {"optimal_rejecting_controls": count + 2}
+
+
+def output_contract_checks(matrix):
+    mode = matrix[0]
+    numerator = [-13 * value for value in c.lift(matrix, mode)]
+    numerator[0] += 52
+    r.require(all(value % 2 == 0 for value in numerator), "reachable witness parity")
+    x = [value // 2 for value in numerator]
+    h = [52 * int(i == 0) for i in range(112)]
+    r.require(c.kernel(matrix, numerator) == h, "first native output witness")
+    restored = c.apply_u(c.forward(matrix, x), True)
+    baseline = c.kernel(matrix, h)
+    gram_column = [sum(a * b for a, b in zip(matrix[i], mode))
+                   for i in c.SELECTORS]
+    r.require(gram_column == [4, 2, 2, 2], "selected Gram witness")
+    expected = [0] * 112
+    for coefficient, column in zip(gram_column, c.COLUMNS):
+        for i, value in column:
+            expected[i] += coefficient * value
+    r.require([a - b for a, b in zip(restored, baseline)] == expected,
+              "inverse frame silently restored baseline output")
+    r.require(any(expected) and max(map(abs, x)) == 13, "nonzero reachable defect")
+    return {"reachable_output_contract_defect": gram_column,
+            "reachable_witness_input_norm_infinity": 13}
+
+
+def three_stage_control():
+    results = []
+    for s in (0, 2):
+        value = 0
+        lo, hi = r.quotient_interval(s)
+        for q3 in range(lo, hi + 1):
+            lo2, hi2 = r.quotient_interval(s + 56 * q3)
+            for q2 in range(lo2, hi2 + 1):
+                lo1, hi1 = r.quotient_interval(s + 56 * (q2 + q3))
+                value += (-1) ** (q2 + q3) * (hi1 - lo1 + 1)
+        results.append(value)
+    r.require(results == [13, -14], "three-stage method boundary changed")
+    return {"three_stage_character_011_at_s0_s2": results}
+
+
+def observer_checks(matrix):
+    gram = [[sum(a * b for a, b in zip(matrix[i], matrix[j]))
+             for j in c.SELECTORS] for i in c.SELECTORS]
+    expected = [[2 + 2 * int(i == j) for j in range(4)] for i in range(4)]
+    r.require(gram == expected, "observer spanning Gram changed")
+    for column, source in enumerate(c.SELECTORS):
+        x = [26 * int(i == source) for i in range(112)]
+        h = c.kernel(matrix, [2 * a for a in x])
+        expected_column = [52 * int(i == column) - gram[i][column]
+                           for i in range(4)]
+        r.require([h[i] for i in c.SELECTORS] == expected_column,
+                  "observer witness does not span")
+        baseline = c.kernel(matrix, h)
+        changed = c.forward(matrix, x)
+        r.require(c.project(matrix, changed) == c.project(matrix, baseline),
+                  "mode observer changed")
+    return {"linear_observer_spanning_inputs": 4,
+            "linear_observer_spanning_determinant": 42 * 50 ** 3}
+
+
+def checks(matrix):
+    report = {}
+    for check in (source_checks, zero_codec_checks, arbitrary_codec_checks,
+                  controls, output_contract_checks, observer_checks):
+        report.update(check(matrix))
+    report.update(walsh_checks())
+    report.update(three_stage_control())
+    return report
diff --git a/research/refined-native-recovery/recovery.py b/research/refined-native-recovery/recovery.py
new file mode 100644
index 0000000000..1ad1b086fa
--- /dev/null
+++ b/research/refined-native-recovery/recovery.py
@@ -0,0 +1,221 @@
+"""Exact interface codec for a scoped refined native chain.
+
+Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0.
+The literal matrix and one-step interface are credited to #5444/#5323.
+No physical or reversible-machine implementation is claimed.
+"""
+from math import prod
+
+
+MAX_DEPTH = 8
+U = (((1, 1), (12, 1), (0, -1), (16, -1)), 2, 2)
+V = (((0, 1), (8, 1), (2, -1), (6, -1)), 3, 2)
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def exact_int(value):
+    return type(value) is int
+
+
+def nearest(numerator, denominator=52):
+    """Nearest integer, with exact half ties away from zero."""
+    require(exact_int(numerator) and exact_int(denominator)
+            and denominator > 0, "invalid rounding operands")
+    magnitude = (2 * abs(numerator) + denominator) // (2 * denominator)
+    return magnitude if numerator >= 0 else -magnitude
+
+
+def project(matrix, vector):
+    require(len(vector) == len(matrix), "wrong vector dimension")
+    return [sum(row[j] * value for row, value in zip(matrix, vector))
+            for j in range(8)]
+
+
+def lift(matrix, vector):
+    require(len(vector) == 8, "wrong mode dimension")
+    return [sum(a * b for a, b in zip(row, vector)) for row in matrix]
+
+
+def kernel(matrix, vector):
+    quotient = [nearest(value) for value in project(matrix, vector)]
+    correction = lift(matrix, quotient)
+    return [a - b for a, b in zip(vector, correction)]
+
+
+def scalar_step(s, value):
+    return value - nearest(s + 56 * value)
+
+
+def quotient_interval(s):
+    lower = -((26 + s) // 4)
+    upper = (26 - s) // 4
+    values = [q for q in range(lower, upper + 1)
+              if nearest(s + 56 * q) == q]
+    require(values and len(values) <= 13, "invalid scalar inverse interval")
+    require(values == list(range(values[0], values[-1] + 1)),
+            "nonconsecutive scalar inverse interval")
+    return values[0], values[-1]
+
+
+def total_interval(s, depth):
+    require(exact_int(s) and exact_int(depth) and 1 <= depth <= MAX_DEPTH,
+            "unsupported scalar interval")
+    lower = upper = 0
+    for _ in range(depth):
+        low_q = quotient_interval(s + 56 * upper)
+        high_q = quotient_interval(s + 56 * lower)
+        lower, upper = upper + low_q[0], lower + high_q[1]
+    return lower, upper
+
+
+def validate_shear(matrix, shear):
+    terms, source, coefficient = shear
+    require(exact_int(source) and 0 <= source < len(matrix), "invalid source")
+    require(exact_int(coefficient) and coefficient % 2 == 0,
+            "frame must be identity modulo two")
+    require(len(terms) <= len(matrix), "oversized shear")
+    indices = [i for i, _ in terms]
+    require(len(set(indices)) == len(indices), "duplicate shear coordinate")
+    require(all(exact_int(i) and 0 <= i < len(matrix) and exact_int(v)
+                for i, v in terms), "invalid shear terms")
+    require(all(i != source or v == 0 for i, v in terms),
+            "shear is not the declared unimodular transvection")
+    require(all(sum(matrix[i][j] * v for i, v in terms) == 0
+                for j in range(8)), "frame does not preserve native modes")
+
+
+def apply_shear(vector, shear, inverse=False):
+    terms, source, coefficient = shear
+    result = list(vector)
+    scale = coefficient * vector[source] * (-1 if inverse else 1)
+    for index, value in terms:
+        result[index] += scale * value
+    return result
+
+
+def validate_chain(matrix, depth, frames):
+    require(exact_int(depth) and 1 <= depth <= MAX_DEPTH,
+            "unsupported chain depth")
+    require(len(frames) == depth - 1, "wrong number of frames")
+    for shear in frames:
+        validate_shear(matrix, shear)
+
+
+def forward(matrix, vector, frames):
+    depth = len(frames) + 1
+    validate_chain(matrix, depth, frames)
+    require(len(vector) == len(matrix) and all(map(exact_int, vector)),
+            "input must be an exact integer vector")
+    result = kernel(matrix, [2 * value for value in vector])
+    for shear in frames:
+        result = kernel(matrix, apply_shear(result, shear))
+    return result
+
+
+def parity_options(matrix, output):
+    masks = [sum((value & 1) << j for j, value in enumerate(row))
+             for row in matrix]
+    return [mask for mask in range(256)
+            if all((mask & row).bit_count() % 2 == (value & 1)
+                   for row, value in zip(masks, output))]
+
+
+def parity_interval(interval, parity):
+    lower, upper = interval
+    first = lower + ((parity - lower) & 1)
+    return first, max(0, (upper - first) // 2 + 1)
+
+
+def blocks(matrix, output, depth):
+    require(len(output) == len(matrix) and all(map(exact_int, output)),
+            "output must be an exact integer vector")
+    intervals = [total_interval(s, depth) for s in project(matrix, output)]
+    result = []
+    for mask in parity_options(matrix, output):
+        cells = [parity_interval(interval, (mask >> j) & 1)
+                 for j, interval in enumerate(intervals)]
+        count = prod(size for _, size in cells)
+        if count:
+            result.append((mask, cells, count))
+    return result
+
+
+def max_states(depth):
+    require(exact_int(depth) and 1 <= depth <= MAX_DEPTH, "unsupported depth")
+    length = 13 ** depth
+    return (length ** 8 + 14 * length ** 4 + 1) // 16
+
+
+def fiber_count(matrix, output, depth):
+    return sum(count for _, _, count in blocks(matrix, output, depth))
+
+
+def unrank_total(matrix, output, depth, tag):
+    require(exact_int(tag) and tag >= 0, "invalid recovery tag")
+    for _, cells, count in blocks(matrix, output, depth):
+        if tag >= count:
+            tag -= count
+            continue
+        total = [0] * 8
+        for j in range(7, -1, -1):
+            first, size = cells[j]
+            tag, index = divmod(tag, size)
+            total[j] = first + 2 * index
+        require(tag == 0, "unconsumed recovery tag")
+        return total
+    raise ValueError("recovery tag exceeds the actual output fiber")
+
+
+def rank_total(matrix, output, depth, total):
+    offset = 0
+    mask = sum((value & 1) << j for j, value in enumerate(total))
+    for candidate, cells, count in blocks(matrix, output, depth):
+        if candidate != mask:
+            offset += count
+            continue
+        rank = 0
+        for value, (first, size) in zip(total, cells):
+            delta = value - first
+            require(delta % 2 == 0 and 0 <= delta // 2 < size,
+                    "total quotient outside its scalar interval")
+            rank = rank * size + delta // 2
+        return offset + rank
+    raise ValueError("total quotient fails the output parity syndrome")
+
+
+def decode(matrix, output, frames, tag):
+    depth = len(frames) + 1
+    validate_chain(matrix, depth, frames)
+    total = unrank_total(matrix, output, depth, tag)
+    s = project(matrix, output)
+    states = [total]
+    for _ in range(depth):
+        states.append([scalar_step(a, b) for a, b in zip(s, states[-1])])
+    require(states[-1] == [0] * 8, "scalar endpoint does not close")
+    current = list(output)
+    for i in range(depth - 1, -1, -1):
+        q = [a - b for a, b in zip(states[i], states[i + 1])]
+        current = [a + b for a, b in zip(current, lift(matrix, q))]
+        if i:
+            current = apply_shear(current, frames[i - 1], inverse=True)
+    require(all(value % 2 == 0 for value in current), "input is not integral")
+    result = [value // 2 for value in current]
+    require(forward(matrix, result, frames) == list(output),
+            "decoded input fails literal native replay")
+    return result
+
+
+def encode(matrix, vector, frames):
+    output = forward(matrix, vector, frames)
+    initial_modes = project(matrix, vector)
+    final_modes = project(matrix, output)
+    differences = [2 * a - b for a, b in zip(initial_modes, final_modes)]
+    require(all(value % 56 == 0 for value in differences),
+            "mode difference is not an integer quotient")
+    total = [value // 56 for value in differences]
+    tag = rank_total(matrix, output, len(frames) + 1, total)
+    return output, tag
diff --git a/research/refined-native-recovery/verify.py b/research/refined-native-recovery/verify.py
new file mode 100644
index 0000000000..777d624d61
--- /dev/null
+++ b/research/refined-native-recovery/verify.py
@@ -0,0 +1,196 @@
+#!/usr/bin/env python3
+"""Bounded exact corroboration of the refined-chain theorem and codec.
+
+For @CubeJerry, substantial OpenAI Codex assistance. Apache-2.0.
+The mathematical proof is PROOF.md; these finite checks are not that proof.
+"""
+import argparse
+from collections import Counter
+import hashlib
+import json
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+sys.path.insert(0, str(HERE))
+import recovery as r
+import optimal_verify
+
+SOURCE = HERE.parent / "precision-state-frontier" / "FIXTURE.json"
+SOURCE_HASH = "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8"
+
+
+def rejected(function, message):
+    try:
+        function()
+    except (ValueError, TypeError):
+        return 1
+    raise ValueError("control failed to reject: " + message)
+
+
+def source_facts(matrix):
+    r.require(len(matrix) == 112 and all(len(row) == 8 for row in matrix),
+              "source matrix has wrong dimensions")
+    r.require(all(type(x) is int and x in (-1, 0, 1)
+                  for row in matrix for x in row), "invalid source coefficients")
+    r.require(all(sum(x != 0 for x in row) == 4 for row in matrix),
+              "source support changed")
+    gram = [[sum(row[i] * row[j] for row in matrix) for j in range(8)]
+            for i in range(8)]
+    r.require(gram == [[56 * (i == j) for j in range(8)] for i in range(8)],
+              "source Gram identity changed")
+    row_code = {0}
+    for row in matrix:
+        mask = sum((x & 1) << i for i, x in enumerate(row))
+        row_code |= {a ^ mask for a in tuple(row_code)}
+    kernel = set(r.parity_options(matrix, [0] * 112))
+    r.require(row_code == kernel and len(kernel) == 16, "self-dual code changed")
+    r.require(Counter(x.bit_count() for x in kernel) == {0: 1, 4: 14, 8: 1},
+              "code weight enumerator changed")
+    return {"gram_entries": 64, "codewords": len(kernel)}
+
+
+def scalar_checks():
+    points = 0
+    for s in range(-52, 53):
+        for depth in range(1, 4):
+            lo, hi = r.total_interval(s, depth)
+            r.require(hi - lo + 1 <= 13 ** depth, "scalar capacity exceeded")
+            for total in range(lo - 2, hi + 3):
+                value = total
+                for _ in range(depth):
+                    value = r.scalar_step(s, value)
+                r.require((value == 0) == (lo <= total <= hi),
+                          "inverse interval differs from literal scalar replay")
+                points += 1
+    for depth in range(1, 9):
+        radius = (13 ** depth - 1) // 2
+        r.require(r.total_interval(0, depth) == (-radius, radius),
+                  "zero-output interval does not attain the bound")
+    r.require([r.nearest(x) for x in [-78, -26, 26, 78]] == [-2, -1, 1, 2],
+              "half-away convention changed")
+    return {"scalar_input_points": points, "interval_depths": [1, 2, 3]}
+
+
+def shear_checks(matrix):
+    for shear in (r.U, r.V):
+        r.validate_shear(matrix, shear)
+        for i in range(112):
+            e = [int(i == j) for j in range(112)]
+            u = r.apply_shear(e, shear)
+            r.require(r.apply_shear(u, shear, True) == e, "inverse shear failed")
+            r.require(r.project(matrix, u) == r.project(matrix, e),
+                      "shear changed mode projection")
+            r.require(all((a - b) % 2 == 0 for a, b in zip(e, u)),
+                      "shear changed parity")
+    e = [0] * 112
+    e[2] = 52
+    lhs = r.kernel(matrix, r.apply_shear(e, r.U))
+    rhs = r.apply_shear(r.kernel(matrix, e), r.U)
+    expected = [0] * 112
+    for i, value in r.U[0]:
+        expected[i] = 8 * value
+    r.require([a - b for a, b in zip(lhs, rhs)] == expected,
+              "source-sized noncommutation witness changed")
+    e[2], e[3] = 0, 1
+    uv = r.apply_shear(r.apply_shear(e, r.V), r.U)
+    vu = r.apply_shear(r.apply_shear(e, r.U), r.V)
+    r.require([a - b for a, b in zip(uv, vu)] == [-v // 2 for v in expected],
+              "two frame shears unexpectedly commute")
+    return {"shear_basis_vectors": 224, "noncommutation_witnesses": 2}
+
+
+def chosen_frames(depth):
+    return [r.U if i % 2 == 0 else r.V for i in range(depth - 1)]
+
+
+def codec_checks(matrix):
+    cases = 0
+    for depth in range(1, 7):
+        frames, zero = chosen_frames(depth), [0] * 112
+        count = r.fiber_count(matrix, zero, depth)
+        r.require(count == r.max_states(depth), "sharp zero fiber failed")
+        offset = 0
+        for _, _, size in r.blocks(matrix, zero, depth):
+            for tag in sorted({offset, offset + size // 2, offset + size - 1}):
+                vector = r.decode(matrix, zero, frames, tag)
+                r.require(r.encode(matrix, vector, frames) == (zero, tag),
+                          "attaining block witness did not round-trip")
+                cases += 1
+            offset += size
+    for depth in range(1, 5):
+        frames = chosen_frames(depth)
+        for sample in range(24):
+            vector = [((sample + 3) * (i * i + 17) % 127) - 63
+                      for i in range(112)]
+            output, tag = r.encode(matrix, vector, frames)
+            r.require(r.decode(matrix, output, frames, tag) == vector,
+                      "arbitrary input did not round-trip")
+            r.require(r.fiber_count(matrix, output, depth) <= r.max_states(depth),
+                      "arbitrary output exceeds the proved maximum")
+            cases += 1
+    return {"source_sized_codec_roundtrips": cases, "maximum_tested_depth": 6}
+
+
+def controls(matrix):
+    zero = [0] * 112
+    mutated = [list(row) for row in matrix]
+    mutated[0][0] = 0
+    checks = [
+        (lambda: source_facts(mutated), "changed native matrix"),
+        (lambda: r.validate_shear(matrix, (r.U[0], 2, 1)), "odd frame"),
+        (lambda: r.validate_shear(matrix, (((0, 1),), 2, 2)), "mode-changing frame"),
+        (lambda: r.validate_shear(matrix, (r.U[0], 1, 2)), "non-unimodular shear"),
+        (lambda: r.decode(matrix, zero, [r.U], r.max_states(2)), "oversized tag"),
+        (lambda: r.decode(matrix, zero, [r.U], -1), "negative tag"),
+        (lambda: r.total_interval(0, 0), "zero depth"),
+        (lambda: r.total_interval(0, 9), "operational depth cap"),
+        (lambda: r.forward(matrix, [0.0] * 112, []), "inexact input"),
+        (lambda: r.require(r.max_states(2) == r.max_states(1) * 13 ** 8,
+                           "false product"), "multiplying one-step maxima"),
+    ]
+    count = sum(rejected(function, label) for function, label in checks)
+    original = r.scalar_step
+    try:
+        r.scalar_step = lambda s, t: t + r.nearest(s + 56 * t)
+        count += rejected(lambda: r.decode(matrix, zero, [r.U], 0),
+                          "reversed quotient sign")
+    finally:
+        r.scalar_step = original
+    output = [0] * 112
+    output[0] = 1
+    r.require(r.fiber_count(matrix, output, 2) == 0, "invalid parity accepted")
+    return {"rejecting_controls": count + 1}
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--output", type=Path)
+    args = parser.parse_args()
+    raw = SOURCE.read_bytes()
+    r.require(hashlib.sha256(raw).hexdigest() == SOURCE_HASH, "source hash mismatch")
+    fixture = json.loads(raw)
+    matrix = list(map(list, zip(*fixture["mode_columns"])))
+    report = {"schema": "refined-native-recovery-result-v2", "no_new_kappa": True}
+    for check in (source_facts, shear_checks, codec_checks, controls):
+        report.update(check(matrix))
+    report.update(scalar_checks())
+    report["optimal_two_stage"] = optimal_verify.checks(matrix)
+    report["parity_I_two_step_states"] = r.max_states(2)
+    report["parity_I_naive_two_step_product"] = r.max_states(1) * 13 ** 8
+    report["parity_I_two_step_state_reduction"] = report["parity_I_naive_two_step_product"] - r.max_states(2)
+    report["parity_I_two_step_packed_bits"] = (r.max_states(2) - 1).bit_length()
+    report["source_sha256"] = SOURCE_HASH
+    report["package_sha256"] = {path.name: hashlib.sha256(path.read_bytes()).hexdigest()
+                                for path in sorted(HERE.iterdir()) if path.is_file()
+                                and path.name not in {"RESULT.json", "VALIDATION.md"}}
+    rendered = json.dumps(report, indent=2, sort_keys=True) + "\n"
+    if args.output:
+        with args.output.open("x", encoding="utf-8") as stream:
+            stream.write(rendered)
+    print(rendered, end="")
+    print("PASS_REFINED_NATIVE_RECOVERY")
+
+
+if __name__ == "__main__":
+    main()