inv_4pi_bounds
plain-language theorem explainer
The lemma establishes that 0.0795 is a strict lower bound and 0.0796 a strict upper bound for the quantity 1 over 4 pi. Researchers deriving forced muon and tau masses from the electron mass in the Recognition framework cite this to fix the spherical geometry contribution inside the first lepton step. The proof is a direct term-mode conjunction of the separately proved lower and upper bounds.
Claim. $0.0795 < 1/(4π) ∧ 1/(4π) < 0.0796$
background
In the T10 module on lepton ladder necessity, this supplies the numerical interval for the spherical term 1/(4π) that appears in the electron-to-muon step. The step function is defined as E_passive plus 1/(4π) minus alpha squared, where E_passive is the passive edge count 11 obtained from passive_field_edges in three dimensions. Upstream lemmas supply the exact definition of E_passive, the step_e_mu definition, and the local pi bounds pi_lt_d6_local and pi_gt_d6_local that justify the stated interval.
proof idea
The proof is a term-mode construction that directly forms the conjunction of the lower bound lemma inv_4pi_lower and the upper bound lemma inv_4pi_upper. No additional tactics or reductions are applied.
why it matters
This lemma fixes the numerical value of the 1/(4π) term inside step_e_mu, which is then bounded in step_e_mu_bounds to obtain the interval (11.079, 11.080). The parent result step_e_mu_bounds feeds the forced muon mass prediction required by T10. It therefore closes one numerical gap in the chain that replaces the original lepton axioms with inequalities derived from cube geometry and the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.