inv_4pi_lower_v2
plain-language theorem explainer
This lemma establishes the concrete lower bound 0.07957 < 1/(4π) in the reals. It is invoked inside the interval proof for the electron-to-muon mass step in the lepton-ladder necessity argument. The short tactic proof obtains an upper bound on π from pi_lt_d6_local, confirms positivity of 4π, and applies the reciprocal monotonicity rule together with a norm_num reduction.
Claim. $0.07957 < 1/(4π)$
background
In the Recognition Science derivation of lepton generations the electron-to-muon step is written as 11 + 1/(4π) minus a small α² correction, where the 1/(4π) term originates from the spherical geometry implicit in the cube-face construction. The module proves that muon and tau masses are forced once the electron structural mass, E_passive = 11, cube faces = 6, wallpaper groups = 17 and α are fixed. The local lemma pi_lt_d6_local supplies the concrete upper bound Real.pi < 3.141593 needed to turn the symbolic expression into a numerical interval.
proof idea
The proof is a short tactic sequence. It obtains h_pi_lt : Real.pi < 3.141593 from pi_lt_d6_local, establishes positivity of 4π by positivity, then executes a calc block that reduces the target by norm_num to the comparison 0.07957 < 1/(4·3.141593) and finishes by one_div_lt_one_div_of_lt applied to the positive quantity 4π together with mul_lt_mul_of_pos_left on the pi upper bound.
why it matters
The bound is required by step_e_mu_bounds_v2, which in turn supplies the interval used inside the main theorem lepton_ladder_forced_from_T9 that discharges T10. It therefore closes the numerical gap for the passive-edge contribution to the muon mass step, relying on the eight-tick octave, the derived value of α, and the exact geometric constants E_passive and W already obtained upstream. No open scaffolding remains; the lemma simply discharges a concrete inequality required for the mass-matching claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.