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 rung positions on the phi-ladder to account for charge skew in RS mass predictions. Mass modelers and SM verification authors cite it when applying the formula m = yardstick(Sector) * phi^(r-8 + gap(Z)). The module is purely definitional with no theorems.

claimThe gap correction is given by $gap(Z) = log_φ(1 + Z/φ)$. It enters the mass law $m = yardstick(Sector) × φ^(r - 8 + gap(Z))$ on the phi-ladder.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants and the canonical mass constants from Anchor. Anchor centralises parameter-free constants derived from first principles in the Model layer. The supplied doc-comment states that gap(Z) corrects the rung position based on the charge-induced skew.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The gap term supplied here appears directly in the mass law used by SMVerification to state RS predictions against PDG 2024 values, by NeutrinoMassExactness to resolve neutrino mass sum discrepancies via Clag corrections, and by HiggsYukawaBridge to express Yukawa couplings as y_f = √2 m_f / v. It completes the gap(Z) slot 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)