Pith. sign in
module module moderate

IndisputableMonolith.Physics.QuarkMasses

show as:
view Lean formalization →

Defines ideal residues and closed-form mass expressions for the six quarks on the golden-ratio ladder. Hierarchy and fermion-spectrum work cites these residues when placing quarks relative to the electron yardstick. Content is definitional: named residue constants and phi-power mass formulas assembled from Constants, PhiSupport, and ElectronMass.

claimIdeal residues $r_q$ and ladder mass expressions for the six quarks $q\in\{u,d,s,c,b,t\}$ on the $\varphi$-ladder, written relative to the electron-mass yardstick so that each $m_q$ is a fixed power of $\varphi$ times that yardstick (with residue shifts from the mixing geometry).

background

Recognition Science places fermion masses on a discrete $\varphi$-ladder. The mass formula is yardstick times $\varphi$ to a rung offset (rung minus eight plus a gap term). The electron module (T9) fixes the first break and supplies the yardstick; $\varphi$ itself is the self-similar fixed point from the forcing chain (T6), with $\varphi^2=\varphi+1$ from PhiSupport.

This module records the ideal residues for the six quarks and the corresponding exponential mass expressions. Interval support (PhiBounds, Pow) is imported so residue and power numerics can be certified later. MixingGeometry supplies the quarter-ladder step sizes used for quark coordinates; Hierarchy treats that quarter-step choice as a hypothesis lane (Gap 6), not as part of the integer-rung core spectra model.

Sibling names split into residue constants (res_up through res_top) and mass expressions (mass_up_exp through mass_top_exp). The module doc frames the whole file as ideal residues on the Phi-ladder.

proof idea

Definition module, not a theorem file. It introduces residue constants and mass_exp abbreviations for each quark flavor, built from $\varphi$-powers, Constants, and the electron-mass yardstick. No forcing proof lives here; ElectronMass.Necessity and the T9 stack remain upstream. Numeric interval imports stand ready for bound lemmas but are not themselves the residue definitions.

why it matters in Recognition Science

Feeds IndisputableMonolith.Physics.Hierarchy, which unifies discrete ladder positions across fermion sectors and demonstrates three-generation coherence. Hierarchy explicitly pulls the quark portion from these residues and from MixingGeometry quarter-ladder steps, while warning that quark step numerics are not in the parameter-free integer-rung core. In the broader RS picture this is the quark half of the mass ladder that begins at T9 (electron) and uses the $\varphi$-ladder mass formula from the primer. It does not close Gap 6; it only packages the ideal residues Hierarchy needs.

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)