Registry · Theorem IV.T14 tau-effective formalized

IV.T14 — Level 0 Range

R₀ ∈ (1831, 1836) at 6-digit approximation. Deviation from CODATA < 1%. Proved by native_decide on 60-digit Nat arithmetic avoiding subtraction.

Book IV Part 3 Ch. 25

Dependency Graph

Depends on (2)

IV.D47 IV.T13

Lean Formalization

Module: TauLib.BookIV.Calibration.MassRatioFormula

Symbol: Tau.BookIV.Calibration.r0_in_range