pi_gt_d6_local
plain-language theorem explainer
The lemma asserts that π exceeds 3.141592 in the reals. Researchers deriving upper bounds on 1/(4π) for lepton mass steps cite it to close numerical inequalities in the T10 necessity proofs. The proof is a direct term application of Mathlib's Real.pi_gt_d6.
Claim. The real number π satisfies π > 3.141592.
background
The module proves T10 necessity: the muon and tau masses are forced from the electron structural mass (T9), cube geometry steps (E_passive = 11, faces = 6, W = 17), α, and φ. It replaces prior axioms with concrete inequalities on these constants, including π from spherical geometry. The upstream result PrimitiveDistinction.from reduces seven independent axioms to four substantive structural conditions plus three definitional facts.
proof idea
The proof is a one-line term wrapper that directly invokes Real.pi_gt_d6 from Mathlib.
why it matters
This lemma supplies the lower bound on π required by inv_4pi_upper and inv_4pi_upper_v2, which bound 1/(4π) for the step functions in muon and tau mass predictions. It fills the geometric constant slot in the lepton ladder derivation under the eight-tick octave and cube geometry of the Recognition framework. No open scaffolding questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.