inv_4pi_lower
plain-language theorem explainer
Researchers deriving forced lepton masses in the Recognition Science framework cite this lower bound on the reciprocal of four pi to anchor the electron-muon step function. It supplies the numerical floor 0.0795 required when E_passive is combined with the spherical-geometry term. The argument reduces the claim to a decimal comparison against 1 over four times 3.141593 and then applies the monotonicity of the reciprocal on positive reals.
Claim. $0.0795 < 1/(4π)$
background
The module proves T10 necessity for the lepton ladder, replacing two original axioms with derived bounds once the electron mass (T9) and geometric constants are fixed. Key constants include E_passive = 11 (passive cube edges), six cube faces, W = 17 (wallpaper groups), and the term 1/(4π) arising from spherical geometry; these combine with α to define rung steps on the phi-ladder. The upstream lemma pi_lt_d6_local states that π < 3.141593, which is invoked directly to obtain the strict inequality.
proof idea
The proof obtains Real.pi < 3.141593 from pi_lt_d6_local, verifies 0.0795 < 1/(4 * 3.141593) by norm_num, then applies one_div_lt_one_div_of_lt together with mul_lt_mul_of_pos_left (using positivity of 4π) to transfer the inequality to the target 1/(4 * Real.pi).
why it matters
The lemma is invoked by inv_4pi_bounds to produce the two-sided estimate on 1/(4π) that enters step_e_mu = E_passive + 1/(4π) - α². In the lepton necessity module it closes the numerical gap needed to prove muon and tau masses are forced from the electron mass and cube-derived constants. It fills the T10 step of the forcing chain by supplying a concrete inequality that replaces an earlier axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.