Pith. sign in
module module high

IndisputableMonolith.Masses.MassLaw

show as:
view Lean formalization →

The MassLaw module defines the gap correction gap(Z) = log base phi of (1 + Z/phi) that shifts the phi-ladder rung to account for charge skew in RS mass formulas. Mass modelers and SM verification authors cite it when applying the yardstick scaling to particle masses. The module is purely definitional with no theorems or proofs.

claimThe gap correction is defined by $ \gap(Z) = \log_\phi (1 + Z/\phi) $, which adjusts the exponent in the mass formula $ m = \text{yardstick} \times \phi^{r-8 + \gap(Z)} $ for charge-induced skew on the phi-ladder.

background

This module sits in the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the canonical mass constants from Anchor. Anchor states that it centralises the parameter-free constants described in the mass manuscripts and that everything lives in the Model layer with no proofs claiming experimental agreement. The gap term appears directly in the mass law used by downstream modules.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the gap(Z) term required by the mass law stated in SMVerification, which formally records RS predictions for all Standard Model particles via m(particle) = yardstick(Sector) × φ^(r - 8 + gap(Z)). It also feeds NeutrinoMassExactness for higher-order corrections and HiggsYukawaBridge for the Yukawa ratio y_f = √2 m_f / v. It completes the charge-skew step in the derivation chain begun in Anchor.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (5)