inv_4pi_bounds
plain-language theorem explainer
The lemma establishes that the reciprocal of four pi lies strictly between 0.0795 and 0.0796. Researchers deriving numerical bounds on the electron-to-muon mass step in the Recognition Science lepton ladder would cite this to control the spherical geometry contribution. The proof is a one-line term wrapper that pairs the separately established lower and upper bound lemmas.
Claim. $0.0795 < 1/(4π) ∧ 1/(4π) < 0.0796$
background
The module proves T10 necessity for the lepton ladder by replacing axioms with inequalities on steps derived from the electron mass (T9), cube geometry, and constants including E_passive and pi. E_passive is the passive edge count, defined as passive_field_edges D with D equal to 3, yielding the integer 11. The step function step_e_mu combines this count with the spherical term 1/(4 pi) minus alpha squared, as stated in the sibling definition: noncomputable def step_e_mu : ℝ := (E_passive : ℝ) + 1 / (4 * Real.pi) - α ^ 2.
proof idea
The proof is a one-line term wrapper that constructs the conjunction via the pair constructor applied to inv_4pi_lower and inv_4pi_upper. The lower lemma compares against 1/(4 * 3.141593) using pi_lt_d6_local, while the upper lemma compares against 1/(4 * 3.141592) using pi_gt_d6_local and the one_div_lt_one_div_of_lt tactic.
why it matters
This lemma supplies the spherical geometry bound required by the downstream step_e_mu_bounds lemma, which feeds the muon and tau mass predictions under T10. It anchors the contribution of 1/(4 pi) from spherical geometry into the forced lepton rungs alongside E_passive = 11 and the eight-tick structure with D = 3. The result closes part of the necessity argument that replaces the two axioms in LeptonGenerations.lean with proven inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.