Prove optimal refined recovery for longer mode-preserving chains (no κ)

research/refined-recovery-longer-chains/FRAMES.json

@@ -0,0 +1 @@
+{"schema":"refined-recovery-longer-chains-frames-v1","E_coords":[0,1,2,4],"stages":26,"lattice_basis_rows":[3,5,6,7,8,9,10,31],"V_blocks":[[[[3,-1],[5,1],[9,-1],[11,1]],[[3,-2],[5,1],[6,-2],[7,1],[9,-3],[10,-1],[12,1],[31,2]],[[3,-2],[5,1],[6,-2],[7,1],[8,1],[9,-2],[10,-1],[13,1],[31,2]],[[3,-2],[5,1],[6,-2],[7,1],[8,1],[9,-3],[14,1],[31,2]]],[[[3,-1],[6,-2],[7,1],[8,1],[9,-2],[10,-1],[15,1],[31,2]],[[3,-2],[5,1],[6,-1],[7,2],[9,-3],[10,-1],[16,1],[31,2]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,2],[10,1],[17,1],[31,-2]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,3],[18,1],[31,-2]]],[[[3,1],[6,1],[7,-2],[8,-1],[9,2],[10,1],[19,1],[31,-2]],[[3,-2],[5,1],[6,-1],[7,1],[9,-3],[20,1],[31,2]],[[3,-1],[6,-1],[7,1],[9,-2],[10,-1],[21,1],[31,2]],[[3,2],[5,-1],[6,1],[7,-1],[8,-1],[9,2],[22,1],[31,-2]]],[[[3,1],[6,1],[7,-1],[8,-1],[9,1],[10,1],[23,1],[31,-2]],[[3,1],[6,1],[7,-1],[8,-1],[9,2],[24,1],[31,-2]],[[3,4],[5,-2],[6,3],[7,-3],[8,-2],[9,6],[10,2],[25,1],[26,1],[31,-6]],[[3,4],[5,-2],[6,3],[7,-4],[8,-3],[9,6],[10,2],[25,1],[27,1],[31,-6]]],[[[3,4],[5,-2],[6,3],[7,-4],[8,-2],[9,7],[10,2],[25,1],[28,1],[31,-6]],[[3,4],[5,-2],[6,3],[7,-4],[8,-2],[9,6],[10,3],[25,1],[29,1],[31,-6]],[[3,5],[5,-3],[6,3],[7,-4],[8,-2],[9,7],[10,2],[25,1],[30,1],[31,-6]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,3],[10,1],[25,1],[31,-3]]],[[[3,2],[5,-1],[6,1],[7,-3],[8,-1],[9,4],[10,1],[25,1],[31,-4],[32,1]],[[3,2],[5,-1],[6,1],[7,-3],[8,-1],[9,3],[10,2],[25,1],[31,-4],[33,1]],[[3,3],[5,-2],[6,1],[7,-3],[8,-1],[9,4],[10,1],[25,1],[31,-4],[34,1]],[[3,2],[5,-1],[6,2],[7,-2],[8,-2],[9,3],[10,1],[25,1],[31,-4],[35,1]]],[[[3,2],[5,-1],[7,-2],[8,-1],[9,3],[25,1],[31,-2],[36,1]],[[3,1],[7,-2],[8,-1],[9,2],[10,1],[25,1],[31,-2],[37,1]],[[3,2],[5,-1],[6,2],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[38,1]],[[3,2],[5,-1],[6,2],[7,-3],[8,-2],[9,3],[10,2],[25,1],[31,-4],[39,1]]],[[[3,3],[5,-2],[6,2],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[40,1]],[[3,2],[5,-1],[7,-1],[8,-1],[9,2],[25,1],[31,-2],[41,1]],[[3,1],[7,-1],[8,-1],[9,1],[10,1],[25,1],[31,-2],[42,1]],[[3,1],[7,-1],[8,-1],[9,2],[25,1],[31,-2],[43,1]]],[[[3,3],[5,-1],[6,1],[7,-2],[8,-1],[9,4],[10,1],[25,1],[31,-4],[44,1]],[[3,3],[5,-1],[6,1],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[45,1]],[[3,3],[5,-1],[6,1],[7,-3],[8,-1],[9,4],[10,2],[25,1],[31,-4],[46,1]],[[3,4],[5,-2],[6,1],[7,-3],[8,-1],[9,5],[10,1],[25,1],[31,-4],[47,1]]],[[[3,1],[5,-1],[7,-2],[8,-1],[9,1],[10,1],[25,1],[31,-2],[48,1]],[[3,1],[5,-1],[7,-2],[8,-1],[9,2],[25,1],[31,-2],[49,1]],[[7,-2],[8,-1],[9,1],[10,1],[25,1],[31,-2],[50,1]],[[3,1],[5,-1],[7,-1],[9,1],[10,1],[25,1],[31,-2],[51,1]]],[[[3,1],[5,-1],[7,-1],[9,2],[25,1],[31,-2],[52,1]],[[7,-1],[9,1],[10,1],[25,1],[31,-2],[53,1]],[[3,1],[5,-1],[7,-1],[8,-1],[9,1],[25,1],[31,-2],[54,1]],[[7,-1],[8,-1],[10,1],[25,1],[31,-2],[55,1]]],[[[7,-1],[8,-1],[9,1],[25,1],[31,-2],[56,1]],[[3,1],[7,-1],[8,-1],[9,1],[25,1],[31,-2],[57,1]],[[3,3],[5,-2],[6,2],[7,-3],[8,-2],[9,4],[10,2],[25,1],[31,-4],[58,1]],[[3,3],[5,-2],[6,2],[7,-3],[8,-2],[9,5],[10,1],[25,1],[31,-4],[59,1]]],[[[3,2],[5,-1],[6,2],[7,-3],[8,-2],[9,4],[10,2],[25,1],[31,-4],[60,1]],[[3,1],[7,-2],[8,-1],[9,2],[25,1],[31,-2],[61,1]],[[3,1],[7,-2],[8,-1],[9,1],[10,1],[25,1],[31,-2],[62,1]],[[3,2],[5,-1],[7,-2],[8,-1],[9,2],[25,1],[31,-2],[63,1]]],[[[3,3],[5,-2],[6,2],[7,-2],[8,-2],[9,4],[10,1],[25,1],[31,-4],[64,1]],[[3,2],[5,-1],[6,2],[7,-2],[8,-2],[9,3],[10,2],[25,1],[31,-4],[65,1]],[[3,2],[5,-1],[6,2],[7,-2],[8,-2],[9,4],[10,1],[25,1],[31,-4],[66,1]],[[3,3],[5,-2],[6,1],[7,-3],[8,-1],[9,4],[10,2],[25,1],[31,-4],[67,1]]],[[[3,3],[5,-2],[6,1],[7,-3],[8,-1],[9,5],[10,1],[25,1],[31,-4],[68,1]],[[3,2],[5,-1],[6,1],[7,-3],[8,-1],[9,4],[10,2],[25,1],[31,-4],[69,1]],[[3,3],[5,-2],[6,1],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[70,1]],[[3,2],[5,-1],[6,1],[7,-3],[8,-2],[9,3],[10,2],[25,1],[31,-4],[71,1]]],[[[3,2],[5,-1],[6,1],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[72,1]],[[3,3],[5,-2],[6,1],[7,-2],[8,-1],[9,4],[10,1],[25,1],[31,-4],[73,1]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,3],[10,2],[25,1],[31,-4],[74,1]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,4],[10,1],[25,1],[31,-4],[75,1]]],[[[3,2],[5,-1],[6,1],[7,-2],[8,-2],[9,3],[10,1],[25,1],[31,-4],[76,1]],[[3,4],[5,-2],[6,3],[7,-4],[8,-2],[9,6],[10,2],[25,1],[31,-6],[77,1]],[[3,-1],[6,-1],[9,-1],[25,1],[78,1]],[[3,3],[5,-1],[6,1],[7,-3],[8,-1],[9,4],[10,1],[25,1],[31,-4],[79,1]]],[[[3,1],[5,-1],[7,-2],[8,-1],[9,2],[10,1],[25,1],[31,-2],[80,1]],[[3,3],[5,-1],[6,2],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[81,1]],[[3,1],[5,-1],[7,-1],[8,-1],[9,1],[10,1],[25,1],[31,-2],[82,1]],[[3,1],[5,-1],[7,-1],[8,-1],[9,2],[25,1],[31,-2],[83,1]]],[[[7,-1],[8,-1],[9,1],[10,1],[25,1],[31,-2],[84,1]],[[3,-1],[9,-1],[85,1]],[[3,1],[5,-1],[6,2],[7,-1],[8,-1],[9,2],[10,1],[31,-2],[86,1]],[[3,1],[5,-1],[6,1],[7,-2],[8,-1],[9,2],[10,1],[31,-2],[87,1]]],[[[3,1],[5,-1],[6,1],[7,-1],[9,2],[10,1],[31,-2],[88,1]],[[3,1],[5,-1],[6,1],[7,-1],[8,-1],[9,1],[10,1],[31,-2],[89,1]],[[3,1],[5,-1],[6,1],[7,-1],[8,-1],[9,2],[31,-2],[90,1]],[[6,1],[7,-1],[8,-1],[9,1],[10,1],[31,-2],[91,1]]],[[[3,-2],[5,1],[6,-2],[7,1],[8,1],[9,-3],[10,-1],[31,2],[92,1]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,3],[10,1],[31,-2],[93,1]],[[3,-2],[5,1],[6,-1],[7,1],[9,-3],[10,-1],[31,2],[94,1]],[[3,2],[5,-1],[6,1],[7,-1],[8,-1],[9,2],[10,1],[31,-2],[95,1]]],[[[3,2],[5,-1],[6,1],[7,-1],[8,-1],[9,3],[31,-2],[96,1]],[[3,1],[6,1],[7,-1],[8,-1],[9,2],[10,1],[31,-2],[97,1]],[[6,-1],[7,-1],[98,1]],[[6,-1],[8,1],[99,1]]],[[[6,-1],[9,-1],[100,1]],[[6,-1],[10,-1],[101,1]],[[3,-1],[5,1],[6,-1],[9,-1],[102,1]],[[7,-1],[8,-1],[103,1]]],[[[7,1],[9,-1],[104,1]],[[7,1],[10,-1],[105,1]],[[3,-1],[5,1],[7,1],[9,-1],[106,1]],[[8,-1],[9,-1],[107,1]]],[[[8,-1],[10,-1],[108,1]],[[3,-1],[5,1],[8,-1],[9,-1],[109,1]],[[9,-1],[10,1],[110,1]],[[3,1],[5,-1],[111,1]]]]}

research/refined-recovery-longer-chains/PROOF.md

@@ -0,0 +1,148 @@
+# Longer refined chains over mode-preserving frames
+
+All objects are those of CubeJerry's PR6327 (`research/refined-native-recovery`),
+for the literal 112×8 matrix M pinned from #5444 in
+`research/precision-state-frontier/FIXTURE.json`.
+
+## 1. Statement
+
+R is nearest-integer rounding with half ties away from zero, and
+K(z)=z−M R(Mᵀz/52). The source facts are MᵀM=56I, C=ker_F2(M mod 2) is the
+self-dual [8,4,4] code, and F=W_C(13,1)/16=(13^8+14·13^4+1)/16=51,008,161.
+Let G={U∈GL_112(Z): MᵀU=Mᵀ}. Fix t≥1 and U_1,…,U_(t−1)∈G with no parity
+restriction. The chain is
+
+    z_1=K(2x),   z_(j+1)=K(U_j z_j),   y=z_t.
+
+Write W_j=(U_(j−1)⋯U_1)^−1 (W_1=I) and N_j=im_F2(W_j M mod 2).
+
+**Theorem.**
+
+(a) Every frame sequence has |fiber(0)| ≥ F^t. Equality holds exactly when
+N_1,…,N_t form a direct sum.
+
+(b) If N_1,…,N_t form a direct sum, every output has fiber at most F^t.
+The maximum fiber is then exactly F^t.
+
+(c) For this M, every N_j lies in one fixed 104-dimensional subspace and has
+dimension 4. A direct sum therefore needs t≤26. FRAMES.json gives an
+explicit sequence for t=26, so every t≤26 is attained by a prefix.
+
+Consequently, over all mode-preserving frame sequences,
+
+    min_U max_y |fiber(y)| = F^t     for 1≤t≤26,
+    min_U max_y |fiber(y)| > F^t     for t≥27.
+
+The minimum packed tag at depth t≤26 is ceil(t·log2 F) bits. That is 26,
+52, 77, … and 666 bits at t=26, compared with ceil(log2 A_t) for the
+parity-I class. At t=2 this recovers PR6327's 52-bit theorem and its
+direct-sum criterion (2).
+
+## 2. Fiber parametrization
+
+Put m_j=Mᵀz_j. Since MᵀU_j=Mᵀ and MᵀM=56I, the j-th kernel call has quotient
+q_j=R(Mᵀ(U_(j−1)z_(j−1))/52)=R(m_(j−1)/52), with m_0=2Mᵀx, and
+m_j=m_(j−1)−56q_j. Going backward from s=Mᵀy,
+
+    q_t∈Q(s),  q_(t−1)∈Q(s+56q_t),  …,  q_1∈Q(s+56(q_2+⋯+q_t)),       (1)
+
+per mode coordinate, where Q(s)={q: R((s+56q)/52)=q}. Reverse execution gives
+
+    2x = Σ_j W_j M q_j + W_t y.                                          (2)
+
+Conversely every chain (1) with integral x in (2) is a preimage: forward
+execution reproduces each m_j, and therefore each q_j. Forward execution is
+deterministic and reproduces the chain of each preimage. The map from
+preimages to chains (1) satisfying the parity condition
+
+    Σ_j (W_j M) q̄_j ≡ W_t y  (mod 2)                                    (3)
+
+is therefore a bijection. verify.py replays (2) on random inputs at depth
+3 and depth 26 for the constructed frames.
+
+PR6327's CHAIN_PROOF Section 2 proves that Q(s) is a nonempty interval of at
+most 13 consecutive integers for every integer s, retaining ties. It also
+proves Q(56w)=[−6,6]−14w. verify.py rechecks both on a finite window. The
+general statement is the predecessor's.
+
+## 3. Box lemma
+
+Let B=I_1×⋯×I_8 with each I_k an interval of at most 13 integers, and let
+c∈F2^8. Then #{q∈B: q̄∈c+C} ≤ F.
+
+Proof. C is self-dual with |C|=16, so 1[v∈c+C]=16^−1 Σ_(h∈C)(−1)^(h·(v+c)).
+Summing over B factorizes per coordinate. The h_k=0 factor is |I_k|≤13.
+The h_k=1 factor is a signed sum of consecutive ±1 values, so it has
+absolute value at most 1. The triangle inequality gives the bound
+16^−1 Σ_(h∈C) 13^(8−wt h)=W_C(13,1)/16=F. verify.py also checks the maximum
+exhaustively at length 13, over every start parity and every coset.
+
+## 4. Proof of (b)
+
+Assume that N_1,…,N_t form a direct sum. The kernel of each W_j M mod 2 is
+C, because W_j is invertible modulo 2. Equation (3) then has no solution,
+or it fixes each component W_j M q̄_j uniquely. Hence there are fixed
+cosets with q̄_j∈c_j+C for all j, and they depend only on y. Count the
+chains (1) from stage t down to stage 1. Once q_t,…,q_(j+1) are fixed,
+q_j ranges over a box of intervals of length at most 13 with parity in
+c_j+C. By Section 3 there are at most F choices. The fiber therefore has
+at most F^t points. This argument conditions stage by stage, so it avoids
+PR6327's joint Fourier majorant, which that package shows fails for three
+quotient parities.
+
+## 5. Proof of (a)
+
+At y=0, (1) with Q(56w)=[−6,6]−14w gives q_j=r_j−14q_(j+1) with free
+r_j∈[−6,6]^8, so q̄_j=r̄_j. The zero fiber is therefore
+
+    Σ_(u∈ker) Π_j 7^(8−wt u_j) 6^(wt u_j),
+    ker = {(u_1,…,u_t): Σ_j W_j M u_j ≡ 0 (mod 2)}.
+
+The kernel contains C^t, and that part contributes exactly
+Π_j W_C(7,6)=F^t. Every term is positive. The kernel equals C^t exactly when
+its dimension is 4t, that is, when dim(N_1+⋯+N_t)=4t, which is the direct
+sum condition. Otherwise the zero fiber exceeds F^t. As a consistency
+check, verify.py evaluates this formula with every N_j=im M for t=1,2,3
+and recovers PR6327's parity-I maximum A_t.
+
+## 6. Proof of (c)
+
+Let K=ker_Z(Mᵀ), a lattice of rank 104. For U∈G, Mᵀ(U^−1−I)=0, so
+W_j M q ∈ Mq+K. Hence every N_j lies in im_F2(M mod 2)+red_2(K), where
+red_2(K)=(K+2Z^112)/2Z^112 has dimension at most rank K=104.
+
+im_F2(M mod 2) lies inside red_2(K). The lattice MᵀZ^112 contains 2Z^8:
+verify.py expresses each 2e_i through eight source rows recorded in
+FRAMES.json. So 28q=Mᵀw for an integer w, and Mq−2w∈K reduces to Mq mod 2.
+All N_j therefore lie in red_2(K), of dimension at most 104. Each N_j has
+dimension 4, so a direct sum requires 4t≤104.
+
+Construction. E has rows e_0ᵀ,e_1ᵀ,e_2ᵀ,e_4ᵀ, as in PR6327, and E M mod 2
+has rank 4 with kernel C. FRAMES.json gives 25 integer blocks V_2,…,V_26
+of four columns each, with MᵀV_j=0 and E V_j=0 (zero on rows 0,1,2,4).
+Put V_1=0 and
+
+    W_j=I+V_jE,     U_j=W_(j+1)^−1 W_j = I+(V_j−V_(j+1))E.
+
+Since E V=0, matrices of the form I+XE multiply by adding the X's. So
+U_j∈GL_112(Z) with inverse I−(V_j−V_(j+1))E, MᵀU_j=Mᵀ, and
+(U_(j−1)⋯U_1)^−1=W_j. verify.py checks MᵀV_j=0 and E V_j=0. It then forms
+all 26 binary images of W_j M directly and finds total rank 104=4·26. Any
+prefix of a direct sum is a direct sum, so this attains (b) for every t≤26.
+
+The blocks are lifts of an F2-basis of the kernel of the map
+u↦Mᵀũ mod 2Λ on the 108 non-E coordinates, with Λ=MᵀZ^112. They are
+chosen to be independent of im M. build_frames.py regenerates FRAMES.json
+deterministically. verify.py does not trust that derivation; it checks the
+stated properties of the committed integers.
+
+## 7. Scope
+
+This is a scoped proof with an exact finite certificate for one interface:
+fixed known frames in G, one relative precision bit before the first call,
+unbounded exact integers and complete output access. It does not cover
+mode-changing frames, input-dependent frames, extra refinement between
+calls, finite ranges or physical tags. It supplies no codec beyond the
+count, no physical memory saving and no κ. The output function changes
+with the frames, as PR6327 notes at t=2. For t≥27 only the strict
+inequality is proved; the exact optimum there is open.

research/refined-recovery-longer-chains/README.md

@@ -0,0 +1,107 @@
+# Refined recovery over longer mode-preserving frame chains
+
+This package answers open question 3 of CubeJerry's
+[PR6327](https://github.com/CrocSwap/integer-mult-bounds/pull/6327)
+(`research/refined-native-recovery`) for every chain depth. That question
+asked for the optimal recovery alphabet of longer parity-changing chains.
+
+The setting is PR6327's. M is the literal 112×8 matrix pinned from #5444.
+K(z)=z−M R(Mᵀz/52) uses half-away rounding. The chain is z_1=K(2x),
+z_(j+1)=K(U_j z_j), with one precision bit and fixed frames U_j∈GL_112(Z)
+satisfying MᵀU_j=Mᵀ and no parity restriction. Put F=51,008,161, PR6327's
+one-step maximum.
+
+## Result
+
+**Theorem** (scoped proof with an exact finite certificate):
+
+- For every depth t and every frame sequence, the zero output has at least
+  F^t preimages. Equality holds exactly when the t binary images of the
+  cumulative framed matrices W_jM form a direct sum.
+- When they form a direct sum, every output has at most F^t preimages.
+- For this M, all such images lie in one 104-dimensional binary subspace,
+  so a direct sum exists only for t≤26. An explicit 26-stage source frame
+  sequence attains it.
+
+Hence the optimal worst-case fiber over all mode-preserving frames is
+**exactly F^t for 1≤t≤26** and **strictly larger than F^t for t≥27**. The
+minimum packed tag is ceil(t·log₂F) bits for t≤26: 26, 52, 77, …, 666 bits.
+At t=2 this reproduces PR6327's 52-bit theorem and its separation criterion.
+For comparison, PR6327's parity-I chains need ceil(log₂A_t) bits, with
+A_t=(13^(8t)+14·13^(4t)+1)/16.
+
+**The new step.** PR6327 shows that its joint Fourier majorant fails for
+three quotient parities. The upper bound here does not use a joint majorant.
+Under a direct sum, each stage's parity coset is fixed by the output alone.
+Conditioning stage by stage then leaves a box of at most 13 values per mode,
+and that box holds at most F points of one C-coset. The dimension cap comes
+from 2Z^8⊂MᵀZ^112, which puts im(M mod 2) inside the reduction of
+ker_Z Mᵀ, a space of dimension at most 104.
+
+[PROOF.md](PROOF.md) gives the argument. [FRAMES.json](FRAMES.json) holds
+the 25 sparse integer blocks V_j. The frames are U_j=I+(V_j−V_(j+1))E,
+with E the rows 0,1,2,4 of PR6327's construction.
+[build_frames.py](build_frames.py) regenerates the blocks deterministically.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library only:
+
+```sh
+python3.12 -I -W error -B research/refined-recovery-longer-chains/verify.py
+python3.12 -I -W error -O -B research/refined-recovery-longer-chains/verify.py
+python3.12 -B scripts/research_package.py --package research/refined-recovery-longer-chains
+python3.12 -B research/refined-recovery-longer-chains/build_frames.py "$SCRATCH/FRAMES.json"
+cmp "$SCRATCH/FRAMES.json" research/refined-recovery-longer-chains/FRAMES.json
+```
+
+Each verifier run prints `PASS_REFINED_RECOVERY_LONGER_CHAINS` in under a
+second. It checks the following exactly:
+
+- the fixture hash, MᵀM=56I, the code C and F=W_C(13,1)/16;
+- that Q(s) is an interval of at most 13 integers on s∈[−4000,4000];
+- the box-coset maximum F, over every start parity and coset;
+- an integer expression of each 2e_i in source rows;
+- the frame blocks: MᵀV_j=0, E V_j=0, and rank 104 of all 26 binary images;
+- the inverse identity 2x=Σ W_jMq_j+W_t y on random inputs at depths 3 and 26;
+- that the zero-fiber formula reproduces PR6327's A_t for parity-I chains at t=1,2,3.
+
+Controls confirm that a perturbed block breaks MᵀV=0 and a repeated frame
+breaks the direct sum.
+
+## Limitations
+
+The all-depth statements are proved in PROOF.md. The finite checks cover the
+source facts, the box lemma at maximal length and the explicit frames. The
+predecessor's interval lemma (Q(s) has at most 13 elements for every s) is
+cited from PR6327's CHAIN_PROOF and only rechecked on a window. For t≥27,
+only the strict inequality is proved. The interface assumptions are PR6327's:
+fixed known frames, unbounded exact integers and complete output access. The
+output function changes with the frames. No codec, physical tag, caller or
+restoration cost is supplied. **No κ change.** The selected frontier and its
+five assumptions are unchanged. No independent human review or formal proof
+kernel check has been done.
+
+## Open next questions
+
+1. **What is the exact optimum at t≥27?** The images must overlap there. The
+   zero-fiber kernel formula in PROOF.md Section 5 gives a lower bound for
+   each overlap pattern. First step: minimize that sum at t=27 over image
+   configurations in the 104-dimensional space. Blocker: with overlapping
+   images, stage cosets are coupled, so the stage-wise box bound no longer
+   applies as stated.
+2. **Mode-changing frames or extra refinement between calls.** First step:
+   derive the coupled quotient congruences for one mode-changing frame at
+   depth two. Blocker: the per-mode scalar recursion no longer separates.
+3. **A physical caller.** Can a caller accept the framed output and use the
+   t·log₂F tag at a favorable complete cost? Blocker: no accepting caller or
+   restoration invoice is known.
+
+## Credit
+
+This package was produced by Nick Petalas. CubeJerry's PR6327 supplies the
+chain model, the scalar interval lemma, the t=2 theorem, the E rows and the
+open question. zxv's #5444 supplies the matrix and the one-step code facts.
+Ali Romman's #5323 and Brian's #5035 are credited for the same-grid counts
+and the rounded kernel, as in PR6327. Character sums over self-dual codes
+are classical. New work is Apache-2.0.

research/refined-recovery-longer-chains/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/precision-state-frontier/FIXTURE.json",
+      "usage": "input",
+      "git_blob": "0aa9f7816378c3eb11ec2e3d63ed9e85cfaa893c",
+      "sha256": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8"
+    },
+    {
+      "path": "research/refined-native-recovery/CHAIN_PROOF.md",
+      "usage": "provenance",
+      "git_blob": "e6af4bbcbb97daf0ccb4361337fd54e871a48553",
+      "sha256": "5b64a5a4a42f99ae8e094fdd20a9fbbcb54c2af4fbabfea8e58a351991a4e06a"
+    },
+    {
+      "path": "research/refined-native-recovery/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "26abf5db19ca6aff04cebd6d9847c37c1021fa6a",
+      "sha256": "d54eac2e7d464ff30f9eada02b049435ca48dfb335e37e74a3c1cc67871aedb9"
+    },
+    {
+      "path": "research/refined-native-recovery/README.md",
+      "usage": "provenance",
+      "git_blob": "a5d15573e107cf814824c3377b1497ace81c90ce",
+      "sha256": "59bc2410dd267df849831eff8db65579f856ed40cdf77172c505d84c4b894df1"
+    }
+  ]
+}