corrections_sub_rung
plain-language theorem explainer
The theorem shows that the spherical correction 1/(4π) lies strictly below one rung on the phi-ladder for lepton mass steps. A researcher constructing sub-leading terms in the Recognition Science mass formula cites it to confirm that integer cube counts dominate the rung assignment. The proof is a short algebraic reduction that invokes the bound π > 3 and finishes with linear arithmetic.
Claim. In the Recognition Science lepton mass ladder the spherical correction satisfies $1/(4π) < 1$ (natural units).
background
The module treats sub-leading corrections to the integer cube counts E_pass = 11 and F = 6 that appear in the e → μ and μ → τ steps. The e → μ correction takes the form E_pass + 1/(4π) − α², where 4π is the surface measure of the unit sphere S² in D = 3 spatial dimensions. The module doc-comment states that the integer part dominates because both corrections remain smaller than one rung. Upstream geometric normalizations appear in the Foundation modules on phi-forcing and dimensional analysis.
proof idea
The term proof first records the library fact Real.pi > 3, rewrites the target inequality using the positivity of 4π, and closes with linear arithmetic.
why it matters
The result anchors the claim that integer cube counts dominate the lepton rung assignments, as required by the module doc-comment. It draws on the Recognition Science forcing chain at T8 (D = 3) where the solid-angle factor 4π is forced. The declaration supplies a concrete bound used in higher-level mass formulas that combine the phi-ladder with geometric corrections. It leaves open whether other geometric terms could produce comparable numerical agreement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.