spherical_correction_nonneg
plain-language theorem explainer
The inequality 1/(4π) ≥ 0 holds for the real numbers. It is cited in derivations of the e to μ lepton mass correction to confirm that the geometric sub-leading term remains positive once the fine-structure constant is inserted. The proof is a one-line wrapper that applies the positivity tactic directly to the constant expression.
Claim. The spherical correction term satisfies $1/(4π) ≥ 0$.
background
The Lepton Sub-Leading Corrections module treats the e→μ transition as E_pass + 1/(4π) − α², where the spherical term 1/(4π) is the unique solid-angle normalization in three spatial dimensions: the surface area of the unit sphere S² equals 4π, yielding the per-steradian factor 1/(4π). This geometric normalization is forced by the cube structure and D=3. The module also records the companion correction μ→τ: F − (2W+3)α/2 with W=17, giving the coefficient 37 = 2W + D. Both corrections remain O(1) or smaller, consistent with perturbative refinements of the integer cube counts {E_pass=11, F=6}. Upstream rung definitions locate the integer ladder steps for each fermion, for example rung(e)=2 and rung(mu)=13.
proof idea
The proof is a one-line wrapper that invokes the positivity tactic on the constant 1/(4 * Real.pi). No lemmas beyond the built-in ordering of the reals are applied.
why it matters
The result supplies the lower bound required for positivity of the full e→μ sub-leading correction, which in turn anchors the mass formula on the phi-ladder. It directly implements the D=3 spatial dimension forced at T8 of the unified forcing chain. The parent context is the geometric forcing of lepton corrections; the open question of full uniqueness of these correction forms remains outside the scope of the present declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.