pith. sign in
module module high

IndisputableMonolith.Masses.AnchorPolicy

show as:
view Lean formalization →

AnchorPolicy supplies the SDGT rung table for up quarks as the discrete set {4, 17, 28} to anchor masses on the phi-ladder. Mass spectrum calculations in the Recognition framework reference these tables when invoking rung_sdgt or predict_mass. The module is purely definitional and extends the canonical constants without any proof content.

claimThe SDGT rung table for up quarks is the set $r = 4, 17, 28$.

background

The module sits in the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the canonical mass constants centralized in Anchor. Those constants are derived from first principles in the Model layer with no experimental claims. It introduces policy definitions for rung selection, including AnchorPolicy and canonicalPolicy, to support mass predictions via the phi-ladder formula yardstick · ϕ^(rung - 8 + gap(Z)).

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the predict_mass and rung_sdgt functions that compute anchored masses. It fills the rung table requirement in the mass derivation chain from the Anchor module, supporting the overall parameter-free mass spectra in Recognition Science.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (20)