Natural latents: a bound below seven🔗

For every joint law p on finite alphabets, the minimum deterministic latent error T(p) and the infimum finite stochastic latent error \tau(p) satisfy T(p)\le (13999/2000)\,\tau(p), with 13999/2000=6.9995<7. The pages prove the exact bound T(p)\le(5249623/750000)\,\tau(p); Lean carries its rounding up to 13999/2000. One deterministic code, chosen from p alone and with at most |\mathcal X\times\mathcal Y| values, has error at most (13999/2000) times the error of every finite stochastic latent of p. Both bounds are invariant under changing between nats and bits; no positivity or independence assumption is imposed on p.

The proof builds on DLorell/stochtodet, pull request #5 by Satya Benson, and pull request #6 by Jeremy Gillen, whose method this route follows.

Read the proof overview. The chapters reproduce the page statements and link their cited Lean counterparts with strict resolution. The retained Lean notes describe exactly which conclusions each declaration states.

kernel-verified: the cited Lean declarations together prove the whole statement.

partly kernel-verified: the cited Lean declarations prove only part of the statement; the proof block opens with "Lean proves: ..." and names that part.

paper proof: the node has no cited Lean declaration and relies on the paper proof.

The component cost identity links the declaration names of its private Lean proofs, as identified in the page notes. Information quantities are in nats until the table-form chapter, which uses bits.