Registry · Theorem IV.T15 tau-effective formalized

IV.T15 — Derivation Chain Complete

ALL 10 links in the R derivation chain are tau-effective. Zero conjectural ingredients. 10/10 scope = tau-effective. Proved by native_decide on list filter.

Book IV Part 3 Ch. 25

Dependency Graph

Depends on (3)

IV.D46 IV.D47 IV.D48

Depended on by (3)

IV.P07 IV.P58 IV.R27

Lean Formalization

Module: TauLib.BookIV.Calibration.MassRatioFormula

Symbol: Tau.BookIV.Calibration.chain_all_tau_effective