Pith. sign in
module module moderate

IndisputableMonolith.Physics.QuarkMasses

show as:
view Lean formalization →

Defines ideal residues and experimental mass anchors for the six quarks on the Recognition Science phi-ladder. Supplies the discrete rung offsets (res_*) and measured masses (mass_*_exp) used when comparing quark spectra to the electron-derived yardstick. Hierarchy imports these values to assemble the three-generation fermion ladder. Content is definitional bookkeeping plus named constants, not a forcing proof.

claimFor each quark $q \in \{u,d,s,c,b,t\}$, the module records an ideal ladder residue $\mathrm{res}_q$ and an experimental mass anchor $m_q^{\mathrm{exp}}$, intended for use in the RS mass formula $m = m_{\mathrm{yard}}\,\varphi^{r-8+\mathrm{gap}(Z)}$ on the $\varphi$-ladder.

background

Recognition Science places fermion masses on a discrete $\varphi$-ladder whose yardstick is fixed by the electron sector (T9). The mass formula is yardstick times $\varphi$ raised to a rung offset that includes a species-dependent gap. Quarks sit on the same ladder but with sector-specific residues and, in the hierarchy layer, quarter-ladder step conventions from MixingGeometry.

This module's stated purpose is "Ideal residues on the Phi-ladder." It imports Constants and PhiSupport for $\varphi$, ElectronMass and its Necessity module for the electron yardstick and T9 forcing context, MixingGeometry for quark coordinate conventions, and interval numerics (PhiBounds, Pow) for rigorous $\varphi$ power bounds when residues are evaluated numerically.

Sibling names indicate six residue constants (res_up through res_top) and six experimental mass anchors (mass_up_exp through mass_top_exp). Those are the objects Hierarchy later unifies across generations.

proof idea

This is primarily a definition and constants module, not a forcing argument. It names ideal residues and experimental mass values for the six quarks, wiring them to the electron-mass yardstick and $\varphi$-ladder infrastructure already proved upstream. Any numeric comparisons rely on imported interval bounds for $\varphi$ and powers rather than new analytic lemmas local to this file.

why it matters in Recognition Science

Physics.Hierarchy imports this module to build the unified generation hierarchy across fermion sectors. Hierarchy's doc-comment states that the quark portion uses quarter-ladder step sizes from MixingGeometry and treats those numerics as a hypothesis lane (Gap 6: integer vs quarter-ladder quark coordinates), not as part of the parameter-free integer-rung core spectra model. The residues here therefore feed comparative and structural coherence checks, while the electron T9 necessity chain remains the forced mass anchor. Framework landmarks in play are the $\varphi$-ladder mass formula and the three-generation octave structure downstream of T6--T8, with quark coordinates still carrying an explicit open gap flag at the hierarchy layer.

scope and limits

used by (1)

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)