pi_gt_d6_local
plain-language theorem explainer
This lemma asserts that the mathematical constant π exceeds 3.141592. It is cited in derivations of upper bounds on 1/(4π) that support predicted muon and tau masses within the lepton ladder. The proof is a direct one-line reference to a standard inequality in the real numbers library.
Claim. The mathematical constant π satisfies π > 3.141592.
background
The module proves that the lepton ladder is forced from the electron structural mass (T9) together with geometric constants from cube geometry and the golden ratio φ. Key quantities include E_passive = 11 (passive cube edges), 6 cube faces, W = 17 (wallpaper groups), α, and π from spherical geometry; all derive from the eight-tick structure. This lemma supplies the concrete lower bound on π needed to obtain an upper bound on 1/(4π) for mass step calculations. The upstream result from PrimitiveDistinction.from reduces seven independent axioms to four substantive structural conditions plus three definitional facts.
proof idea
The proof is a one-line term that directly invokes the Mathlib theorem establishing π greater than 3.141592.
why it matters
This lemma supports the upper bound results inv_4pi_upper and inv_4pi_upper_v2, which feed the necessity proofs for muon and tau masses in the lepton ladder. It supplies a numerical inequality for π inside the T10 necessity module, where constants arise from the eight-tick octave and D = 3. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.