IndisputableMonolith.Masses.LeptonSubLeadingForcing
The LeptonSubLeadingForcing module supplies geometric solid-angle factors and coupling-coefficient decompositions that generate subleading corrections to lepton masses on the phi-ladder. Mass-spectrum researchers would cite these definitions when extending leading-order predictions to include D=3 directional effects. The module builds its content through a chain of explicit definitions that start from the solid angle of S^{D-1} and terminate at emu_ingredients.
claimThe solid angle of the unit sphere $S^{D-1}$ in $D$ dimensions is $4D = 2D^{D/2}/Gamma(D/2)$, which equals $4pi$ when $D=3$. Per-steradian factors, wallpaper coupling coefficients, and sub-rung corrections are defined from this solid angle to produce the subleading forcing terms for leptons.
background
Recognition Science places lepton masses on a phi-ladder whose leading term is set by the yardstick times phi to the power (rung minus 8 plus gap(Z)). Subleading corrections arise from the geometry of three-dimensional space. The module imports the RS time quantum tau_0 = 1 tick from Constants and the constructive derivation of alpha inverse from the cubic ledger in AlphaDerivation, where 4pi emerges via Gauss-Bonnet from vertex deficits of Q_3.
proof idea
This is a definition module, no proofs. It introduces solid_angle, per_steradian, wallpaper_coupling_coeff, coupling_coeff_decomposition, corrections_sub_rung, and emu_ingredients in direct sequence, each built from the preceding term and the imported 4pi solid-angle result.
why it matters in Recognition Science
The module supplies the geometric subleading terms required by the Recognition mass formula for leptons. It directly extends the 4pi result of AlphaDerivation into the mass domain and prepares the ingredients used by higher-level lepton-mass statements in the framework. No downstream theorems are listed, but the definitions close the gap between leading-order phi-ladder masses and observed fine structure.
scope and limits
- Does not derive numerical mass values for any lepton.
- Does not address quark or boson masses.
- Does not prove the leading-order mass formula.
- Does not compute the fine-structure constant itself.
depends on (2)
declarations in this module (13)
-
def
solid_angle -
def
per_steradian -
theorem
per_steradian_at_D3 -
theorem
per_steradian_pos -
def
wallpaper_coupling_coeff -
theorem
wallpaper_coupling_coeff_eq -
theorem
coupling_coeff_decomposition -
theorem
coupling_half -
theorem
spherical_bound -
theorem
spherical_correction_nonneg -
theorem
corrections_sub_rung -
theorem
emu_ingredients -
theorem
mutau_ingredients