[apoursh]

Scoped proof with exact finite corroboration; no κ. Package: research/refined-recovery-eps-rate. This answers #6849's open question 2.

Result

Write OPT(t) = 2^(−104)·13^(8t)·(1+ε_t). For every t ≥ 29,

(2^104−1)·13^(−4t·2^104/(2^104−1))  ≤  ε_t  ≤  (2^104−16)·q^t + 14·13^(−4t) + 13^(−8t),   q = (1+14·13⁻⁴+13⁻⁸)/16

• Rate. ε_t decays at between 4.0 and 14.8 bits per stage. At t = 29 the upper bound is 2.48·10⁻⁴.
• Comparison with Refined recovery: optimum → 13^(8t)/2^104 exponentially; exact tag ⌈8t·log₂13⌉−104 at every depth t≥27 (no κ) #6850. Its periodic frames give a decay of about 0.57 bits per stage.

Proof

• Upper bound: exact first moment. In PR6660's family W_j = I + V_jE, the stage maps are φ_j = μ + ψ_j, and ψ_j ranges over all linear maps Q → R′. Here R′ is a 100-dimensional complement of im μ in the 104-dimensional V; verify.py computes it from M.
  • For uniform independent ψ_j (ψ₁ = 0), every χ with a nonzero R′-component sees h_j uniform on C. That gives E[S] = the formula exactly.
  • So some frames achieve it, and by Markov at least half of them achieve twice it.
  • The bound is below Refined recovery: max fiber = zero fiber under an ε₀ threshold; exact depth-27 optimum (1+12ρ₂²⁵+3ρ₂²⁶)·F²⁷, 696 bits (no κ) #6848's threshold, so their max fiber equals their zero fiber.
• Lower bound: Jensen, for all frames. Each χ ↦ χ∘φ_j hits every word of C equally often, so the average total weight is 4t. Convexity of 13^(−x) does the rest.

Verification

verify.py (stdlib, exact rationals) prints PASS_REFINED_RECOVERY_EPS_RATE in under a second, in normal and -O mode. It checks:

• dim R′ = 100 and dim(im μ + R′) = 104, from the pinned M;
• the first-moment formula, by exact full enumeration in toy dimensions with the real C and η;
• the Jensen weight identity;
• E_t < ε* for 29 ≤ t ≤ 60, with the control E₂₈ > ε*.

Both repo package checks pass.

Limitations

• Unreplayed premises. PR6660, Refined recovery: max fiber = zero fiber under an ε₀ threshold; exact depth-27 optimum (1+12ρ₂²⁵+3ρ₂²⁶)·F²⁷, 696 bits (no κ) #6848 and Refined recovery at every depth t≥27: optimum = 13^(8t)/2^104 within 5.5·10⁻⁶; exact tag ⌈8t·log₂13⌉−104 bits (no κ) #6849 are cited, not replayed; all are unmerged.
• Existential upper bound. The upper bound gives no explicit frames.
• Open gap. The gap between 4.0 and 14.8 bits per stage remains open. A Delsarte-type LP bound is the natural next step.
• Not supplied. No codec, physical tag or restoration cost. κ and the selected frontier are unchanged.
• No independent review. No independent human or proof-kernel review is claimed.

AI disclosure: Anthropic Claude (Claude Code) found the argument, wrote the verifier and ran the checks, under apoursh's direction. Credit to Nick Petalas (PR6660), CubeJerry (PR6327) and zxv (#5444).

🤖 Generated with Claude Code