inv_4pi_lower
plain-language theorem explainer
The lemma proves that one over four pi strictly exceeds 0.0795. Researchers deriving forced muon and tau masses under T10 cite it to anchor the electron-muon step function. The tactic proof chains a local upper bound on pi through positivity and the reciprocal inequality via a calculation block.
Claim. $0.0795 < 1/(4π)$
background
The module proves T10 necessity for the lepton ladder by replacing two axioms with derived bounds on muon and tau masses. It starts from the electron structural mass (T9) and combines E_passive equal to 11, cube faces equal to 6, wallpaper count W equal to 17, the fine-structure constant, and pi from spherical geometry. The step function for the electron-muon transition is defined as eleven plus one over four pi minus alpha squared.
proof idea
The proof obtains pi less than 3.141593 from pi_lt_d6_local, confirms positivity of four pi, then executes a calc chain. Norm_num first verifies the inequality against the approximation one over four times 3.141593. One_div_lt_one_div_of_lt together with mul_lt_mul_of_pos_left transfers the strict inequality to the true pi.
why it matters
This lemma supplies the lower half of inv_4pi_bounds, which constrains the step_e_mu term inside the lepton generation predictions. It advances the T10 goal of forcing the full lepton ladder from the phi fixed point, eight-tick octave, and cube geometry without free parameters. The numerical anchor keeps the predicted masses inside the alpha band derived earlier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.