spherical_bound
The inequality 1/(4π) > 0 holds for the spherical normalization factor and bounds the geometric correction in the electron-to-muon mass transition. Recognition Science mass derivations cite it to confirm that the sub-leading term stays positive and perturbative relative to the leading integer rung. The proof is a direct one-line application of the positivity tactic to the explicit real constant.
claim$1/(4π) > 0$
background
The lepton sub-leading corrections module treats the e→μ transition as E_pass + 1/(4π) − α², where the spherical term normalizes the solid angle of the unit sphere in D=3. This normalization follows from the Recognition Science forcing of three spatial dimensions via the eight-tick octave and simplicial ledger edge lengths. Upstream structures on spectral emergence fix the gauge content and three-generation count that motivate the geometric factors, while phi-forcing derived J-cost structures calibrate the underlying mass ladder.
proof idea
The proof is a one-line wrapper that applies the positivity tactic directly to the constant expression 1/(4 * Real.pi).
why it matters in Recognition Science
This bound secures positivity for the spherical correction inside the lepton mass formula and aligns with the T8 derivation of D=3 together with the solid-angle normalization required by the Recognition Composition Law. It supports the module's claim that corrections remain O(1) or smaller relative to the integer cube counts. The module doc notes that full uniqueness of the correction form is left open.
scope and limits
- Does not prove that 1/(4π) is the unique geometric correction possible.
- Does not supply the numerical value of the bound or its comparison to α.
- Does not address higher-order or non-spherical corrections.
formal statement (Lean)
90theorem spherical_bound : 1 / (4 * Real.pi) > (0 : ℝ) := by positivity
proof body
Term-mode proof.
91
92/-- The spherical correction 1/(4π) is bounded below by 0.
93 (Full positivity of e→μ sub-leading requires α < 1/(4π),
94 which holds since α ≈ 1/137 << 1/(4π) ≈ 0.08.) -/