pith. sign in
module module high

IndisputableMonolith.Physics.QuarkMasses

show as:
view Lean formalization →

The module supplies ideal residues for the six quark masses placed on the phi-ladder. Physicists constructing fermion mass hierarchies from Recognition Science would cite these definitions when assembling the full particle spectrum. It consists of explicit residue expressions for top, bottom, charm, strange, down and up quarks, each built from the same yardstick and rung arithmetic used for the electron.

claimIdeal residues $r_q$ on the phi-ladder for quarks $q = t,b,c,s,d,u$, so that $m_q = y_0 · φ^{r-8+g(Z)}$ with $y_0$ the base yardstick and $g(Z)$ the gap function.

background

Recognition Science places all masses on a discrete phi-ladder after T8 fixes three spatial dimensions. The electron mass module (T9) already supplies the ledger-fraction residue and the base yardstick; this module extends the same construction to quarks. Upstream modules supply the time quantum τ₀ = 1 tick, the identity φ² = φ + 1, and rigorous interval bounds on powers of φ.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed the Unified Generation Hierarchy module, which assembles the three-generation structure, and the ParticleSummary that collects all Standard-Model parameters. The module therefore supplies the quark-sector half of the mass formula that follows from the T9 ledger-fraction result and the phi-ladder yardstick.

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)