pith. sign in
module module moderate

IndisputableMonolith.RRF.Physics.QuarkMasses

show as:
view Lean formalization →

This module supplies explicit definitions for the ideal mass residues of the six quarks on the phi-ladder, extending the ledger-fraction mass formula from the electron sector. Researchers comparing RS-native quark mass hierarchies to experiment would cite these residues to fix rung assignments and gaps. The module consists of paired definitions for each flavor's exponential mass expression and its corresponding residue, built from phi bounds and power intervals.

claimThe module defines ideal residues $r_q$ on the $phi$-ladder for quark flavors $q$ via the mass formula $m_q = tau_0 phi^{r_q-8+Delta(Z_q)}$ with $tau_0=1$ in RS units, together with the explicit exponential expressions $mass_{top_exp}$, $mass_{bottom_exp}$, $mass_{charm_exp}$, $mass_{strange_exp}$, $mass_{down_exp}$, $mass_{up_exp}$ and their residues $res_{top}$, $res_{bottom}$, $res_{charm}$, $res_{strange}$, $res_{down}$, $res_{up}$.

background

The module operates in the Recognition Science setting where all masses arise from the phi-ladder mass formula introduced in the ElectronMass module. Constants supplies the RS time quantum $tau_0=1$ tick. PhiSupport encodes the defining relation $phi^2=phi+1$. PhiBounds and Pow furnish rigorous interval bounds on $phi=(1+sqrt5)/2$ and on the power function $x^y$ via the exponential-log identity, ensuring all residue calculations remain inside verified intervals. ElectronMass.Necessity establishes that the underlying ledger quantization (T8) forces the electron mass; this module applies the same structure to quarks.

proof idea

This is a definition module, no proofs. It introduces the six mass_exp definitions and their six residue definitions by direct application of the phi-ladder formula, using the imported interval arithmetic to keep every exponent and power inside certified bounds.

why it matters in Recognition Science

The module completes the quark sector of the mass ladder that begins with the T9 electron-mass derivation. It supplies the concrete residues needed for any downstream numerical comparison or hierarchy prediction inside the RRF framework. The doc-comment states the purpose directly: ideal residues on the phi-ladder, thereby anchoring the six quark masses to the self-similar fixed point phi forced at T6.

scope and limits

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (25)