pi_lt_d6_local
plain-language theorem explainer
The lemma asserts that π is strictly less than 3.141593. Researchers deriving lower bounds on 1/(4π) for lepton mass predictions in the T10 necessity module would cite it. The proof is a one-line term that applies Mathlib's pi_lt_d6 directly.
Claim. The constant π satisfies the strict inequality π < 3.141593.
background
This lemma sits inside the module that proves T10: the muon and tau masses are forced from the electron structural mass (T9) together with cube-derived constants E_passive = 11, faces = 6, wallpaper groups W = 17, and α. The bound on π supplies the concrete numerical input needed for spherical-geometry factors that appear in the step functions of the lepton ladder. The module replaces two earlier axioms with proven inequalities that close the chain from T8 (D = 3) through the Recognition Composition Law to the predicted residues.
proof idea
The proof is a one-line term wrapper that invokes Real.pi_lt_d6 from Mathlib.
why it matters
It supplies the π upper bound required by the downstream lemmas inv_4pi_lower and inv_4pi_lower_v2, which in turn feed the main T10 statement that the full lepton ladder is determined by T9 plus the geometric constants. The declaration therefore closes a numerical gap between the eight-tick octave structure and the explicit mass bounds for the muon and tau.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.