pith. sign in
module module moderate

IndisputableMonolith.Physics.QuarkMasses

show as:
view Lean formalization →

QuarkMasses defines ideal residues for the six quark flavors positioned on the phi-ladder. Researchers assembling the fermion mass spectrum in Recognition Science cite these values to complete the three-generation hierarchy. The module supplies experimental mass anchors together with computed residues that scale via phi-powers and interval bounds drawn from the electron-mass base.

claimResidues $r_t, r_b, r_c, r_s, r_d, r_u$ on the phi-ladder satisfy $m_q = m_e · φ^{r_q + k}$ for quark masses $m_q$, where the offsets $r_q$ are the ideal residues and $k$ incorporates the quarter-ladder steps from mixing geometry.

background

The module extends the T9 electron-mass derivation to the quark sector inside the Recognition Science framework. Upstream, Constants fixes the RS time quantum τ₀ = 1 tick; PhiSupport proves φ² = φ + 1; ElectronMass derives the electron mass from the refined ledger-fraction hypothesis; ElectronMass.Necessity shows this mass is forced from T8 ledger quantization. MixingGeometry supplies the quarter-ladder coordinates used for quarks, while PhiBounds and Pow deliver rigorous interval arithmetic for φ and its powers.

proof idea

This is a definition module, no proofs. It declares experimental mass values for each quark flavor and defines the corresponding ideal residues by direct application of the imported phi-power scaling and bound lemmas.

why it matters in Recognition Science

The residues feed the unified generation hierarchy in Physics.Hierarchy, which unifies discrete ladder positions across all fermion sectors, and populate the standard-model parameters in Physics.ParticleSummary. The hierarchy documentation notes that the quark portion relies on quarter-ladder steps from MixingGeometry and treats them as a hypothesis lane (Gap 6).

scope and limits

used by (2)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (19)