inv_4pi_upper
plain-language theorem explainer
This lemma proves the inequality 1/(4π) < 0.0796. Researchers deriving numerical bounds for the lepton generation steps in the Recognition Science framework cite it to anchor the electron-to-muon step function. The proof invokes a local lower bound on π, applies monotonicity of the reciprocal function, and finishes with numerical comparison.
Claim. In the real numbers, $$1/(4π) < 0.0796$$.
background
The module T10 Necessity shows that the lepton ladder is forced from the electron mass (T9) and geometric constants derived from cube geometry and the golden ratio. The quantity 1/(4π) enters the step function step_e_mu = E_passive + 1/(4π) - α², where E_passive = 11 counts passive cube edges and α is the fine-structure constant derived earlier in the chain.
proof idea
The proof obtains h_pi_gt : 3.141592 < π from pi_gt_d6_local and confirms positivity of 4 * 3.141592 by norm_num. It then applies one_div_lt_one_div_of_lt together with mul_lt_mul_of_pos_left to establish 1/(4π) < 1/(4 * 3.141592), and closes with norm_num to verify the target constant 0.0796.
why it matters
This lemma feeds inv_4pi_bounds, which supplies the two-sided estimate on 1/(4π) used to bound step_e_mu ≈ 11.0795 and the subsequent muon and tau mass predictions. It closes part of the T10 necessity chain by replacing an earlier axiom with a derived inequality that rests on the π lower bound from spherical geometry in the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.