inv_4pi_upper
plain-language theorem explainer
The lemma establishes that 1 over 4 pi is strictly less than 0.0796. Researchers bounding the muon mass step function in the lepton ladder of Recognition Science cite this numerical anchor. The short tactic proof invokes a local lower bound on pi, applies the reciprocal inequality, and finishes with a norm_num comparison.
Claim. $1/(4π) < 0.0796$
background
This lemma belongs to the T10 necessity module that forces the muon and tau masses from the electron mass (T9) together with geometric constants. The local setting replaces two earlier axioms with derived bounds on predicted lepton masses; the step_e_mu correction term is defined as E_passive + 1/(4π) - α² where E_passive = 11 arises from passive cube edges. The upstream lemma pi_gt_d6_local supplies the concrete inequality (3.141592 : ℝ) < Real.pi drawn from Mathlib.
proof idea
The proof first obtains h_pi_gt from pi_gt_d6_local. It then applies one_div_lt_one_div_of_lt together with mul_lt_mul_of_pos_left to deduce 1/(4π) < 1/(4 * 3.141592). The final norm_num step verifies that the right-hand side lies below 0.0796.
why it matters
The result supplies the upper half of inv_4pi_bounds, which controls the spherical correction inside the lepton rung formulas. It closes part of the T10 chain by giving a numerically safe limit on the 1/(4π) term that appears in the muon mass prediction. The parent lemma inv_4pi_bounds is used downstream to establish the forced intervals for the higher lepton generations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.