[apoursh]

Scoped proof with exact finite corroboration; no κ. Package: research/refined-recovery-max-fiber.

Result

Theorem. Take any depth and any frame sequence in G. Suppose its zero fiber is within ε* = (1/13)/((23/12)⁸−1) ≈ 4.25·10⁻⁴ (relative) of its Fourier main term 2^(dim D−4t)·13^(8t). Then max_y |fiber(y)| = |fiber(0)|.

Corollary (exact depth-27 optimum).

min_U max_y |fiber(y)| = (1 + 12ρ₂²⁵ + 3ρ₂²⁶)·F²⁷ ≈ 15.7897746·F²⁷  →  696 tag bits

This is the first exact value past PR6660's range t ≤ 26, and it answers PR6660's open question 1 at t = 27.

• The lower bound is Refined recovery at depth 27: exact minimum zero fiber (1+12ρ₂²⁵+3ρ₂²⁶)·F²⁷, realized by explicit frames; floors for all t≥27 (no κ) #6828's exact minimum zero fiber.
• The upper bound uses Refined recovery at depth 27: exact minimum zero fiber (1+12ρ₂²⁵+3ρ₂²⁶)·F²⁷, realized by explicit frames; floors for all t≥27 (no κ) #6828's FRAMES27 frames, whose ε₀ = 5.45·10⁻⁶ is 78× below the threshold.
• This also closes Refined recovery at depth 27: exact minimum zero fiber (1+12ρ₂²⁵+3ρ₂²⁶)·F²⁷, realized by explicit frames; floors for all t≥27 (no κ) #6828's open question 1.

Why the box lemma is not enough, and what replaces it

For y ≠ 0 the per-stage boxes can depend on the chain history, and the overlapping stage cosets block PR6660's stage-by-stage count. The proof has four steps:

1. Factorization. Poisson summation over H = ker Φ writes the fiber as a sum over h ∈ H^⊥. Each term is a product of eight one-coordinate signed chain sums Z_k, because each coordinate's box depends only on its own history.
2. Ties are the only adaptivity. Without a rounding tie, each box is a fixed 13-interval shifted by an even amount, so |Z_k| equals its y = 0 value.
   • At ties, s = 4x+2. The state follows x ↦ −13x + 14r.
   • Only the 16 states x ∈ [−8,7] can still meet a 12-element box. All other states alternate between two classes forever, and their boxes stay fixed.
3. Bounding the tie states. For those states Z is a product of 10×10 transfer matrices. An interval family on the 1/12 grid is exactly closed under T₀/13 and T₁, which gives |Z_k| ≤ (23/12)·13^(zeros) at every depth.
   • The constant is essentially attained (above 1.9166 at depth 27).
   • The naive majorant with constant 1 fails, e.g. Z₋₂₂(1,0,1) = 24.
4. The penalty. Every state whose ratio exceeds 1 starts with a 12-element box, so the main term loses a factor 12/13. That loss beats (23/12)⁸·ε₀ whenever ε₀ ≤ ε*.

Verification

verify.py (stdlib, exact rationals) prints PASS_REFINED_RECOVERY_MAX_FIBER in about 45 s, in both normal and -O mode. It checks:

• C and ρ₂, derived from the pinned M;
• the box lemma for |s| ≤ 3000;
• the transfer matrices against direct chain recursion (|s| ≤ 150, depth ≤ 4);
• the closed interval family and the cap for each state;
• the Poisson identity on six random t = 2 instances, with random D and tie coordinates;
• ε* and ε₀ exactly, and the 696-bit count;
• two controls: the failing naive majorant, and t = 26 direct sums (ε₀ ≈ 0.0128) lying outside the threshold. PR6660's box lemma covers those instead.

Both scripts/research_package.py --package and scripts/check_research_commit.py --check-source-history --check-modes pass.

Limitations

• Unreplayed premises. The corollary relies on Refined recovery at depth 27: exact minimum zero fiber (1+12ρ₂²⁵+3ρ₂²⁶)·F²⁷, realized by explicit frames; floors for all t≥27 (no κ) #6828's exact minimum and its FRAMES27 realization (unmerged), and on PR6660's chain bijection (unmerged fork head b6de532e). They are cited, not replayed.
• Open beyond depth 27. The exact optimum for t ≥ 28 is still open.
• Not supplied. No codec, physical tag or restoration cost. κ, the selected frontier and its five assumptions are unchanged.
• No independent review. No independent human or proof-kernel review is claimed.

Credit

Nick Petalas (PR6660: chain bijection, depth law, the open question); CubeJerry (PR6327: chain model, F, box facts); zxv (#5444: M).

AI disclosure: Anthropic Claude (Claude Code) found the argument, wrote the verifier and ran the checks, under apoursh's direction.

🤖 Generated with Claude Code