Registry · Theorem IV.T09 established formalized

IV.T09 — Ledger Count

The complete ledger has exactly 23 entries: 10 couplings + 5 formulas + 2 identities + 3 near-matches + 3 framework. Lean-verified by rfl.

Book IV Part 2 Ch. 15

Dependency Graph

Depends on (1)

IV.D39

Depended on by (1)

IV.T50

Lean Formalization

Module: TauLib.BookIV.Calibration.ConstantsLedger

Symbol: Tau.BookIV.Calibration.ledger_count