Registry · Definition IV.D46 tau-effective formalized

IV.D46 — Mass Ratio Bulk Term

ι_τ^(-7) bulk term: numer = 10⁴², denom = 341304⁷. Range: (1846, 1850) at 6-digit approximation, ~1853.6 at exact ι_τ. Proved by native_decide.

Book IV Part 3 Ch. 25

Dependency Graph

Depends on (2)

IV.T10 I.D01

Depended on by (3)

IV.D47 IV.T13 IV.T15

Lean Formalization

Module: TauLib.BookIV.Calibration.MassRatioFormula

Symbol: Tau.BookIV.Calibration.bulk_numer