inv_4pi_upper_v2
plain-language theorem explainer
The inequality 1/(4π) < 0.07958 supplies a concrete numerical upper bound for lepton step calculations. Researchers deriving forced muon and tau masses from electron mass and cube geometry cite it to close interval estimates. The proof invokes a Mathlib lower bound on π then reduces the comparison to a direct numerical check via one_div_lt_one_div_of_lt and norm_num.
Claim. $1/(4π) < 0.07958$
background
The T10 module proves the lepton ladder is forced from the electron mass (T9) together with geometric step functions built from E_passive = 11, cube faces = 6, wallpaper groups W = 17, α, and π. This lemma supplies one half of the reciprocal-4π bounds needed to tighten the electron-to-muon step interval. Upstream, pi_gt_d6_local states (3.141592 : ℝ) < Real.pi and is obtained directly from Mathlib.
proof idea
The tactic proof obtains h_pi_gt from pi_gt_d6_local, establishes positivity of the denominator by norm_num, applies one_div_lt_one_div_of_lt to replace π by its lower bound, then finishes with a direct norm_num comparison of the resulting rational to 0.07958.
why it matters
The lemma is invoked inside step_e_mu_bounds_v2 to produce the tight interval (11.0795, 11.0796) for the electron-muon step. It therefore contributes to the T10 claim that muon and tau masses are forced by the eight-tick octave and cube geometry rather than imposed as axioms. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.