Registry · Theorem IV.T13 tau-effective formalized

IV.T13 — Bulk Overshoots

ι_τ^(-7) > R_CODATA even at 6-digit precision (1847.7 > 1838.68). Correction must be subtracted. Proved by native_decide on 50-digit Nat comparison.

Book IV Part 3 Ch. 25

Dependency Graph

Depends on (2)

IV.D46 IV.D27

Depended on by (1)

IV.T14

Lean Formalization

Module: TauLib.BookIV.Calibration.MassRatioFormula

Symbol: Tau.BookIV.Calibration.bulk_overshoots_codata