Registry · Theorem IV.T12 tau-effective formalized

IV.T12 — Correction Smallness

π³α² < 0.002 and > 0.001: the holonomy correction is real but 1000× smaller than √3. Perturbative hierarchy. Proved by simp.

Book IV Part 3 Ch. 24

Dependency Graph

Depends on (1)

IV.D45

Lean Formalization

Module: TauLib.BookIV.Physics.HolonomyCorrection

Symbol: Tau.BookIV.Physics.correction_lt_2_per_mille