pi_lt_d6_local
plain-language theorem explainer
This supplies the inequality π < 3.141593 required to bound 1/(4π) from below in the derivations of forced lepton masses. It is cited by any proof that needs a concrete numerical threshold for the spherical geometry steps in the T10 lepton ladder. The proof reduces immediately to Mathlib's pi_lt_d6.
Claim. The inequality $π < 3.141593$ holds.
background
Module T10 establishes that the lepton ladder (muon and tau masses) follows necessarily from the electron mass (T9) together with cube geometry constants and α. The bound on π enters because spherical geometry contributes to the step functions that set the rung spacings on the phi-ladder. This lemma provides the specific decimal comparison used to verify 1/(4π) > 0.0795, which tightens the mass interval predictions. It imports the standard Mathlib fact pi_lt_d6 without further derivation.
proof idea
One-line wrapper that applies Real.pi_lt_d6 from Mathlib.
why it matters
Feeds directly into inv_4pi_lower and inv_4pi_lower_v2, which close the numerical requirements for the main T10 result that muon and tau masses are forced by E_passive=11, F=6, W=17, α, and the electron mass. This completes one link in the chain from T9 to the full lepton spectrum. The framework landmark is the replacement of axioms by derived inequalities in the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.