pith. sign in
module module moderate

IndisputableMonolith.RRF.Physics.QuarkMasses

show as:
view Lean formalization →

The module supplies explicit definitions for the ideal residues of the six quarks on the phi-ladder within the Recognition Science mass hierarchy. Researchers extending the T9 ledger-fraction derivation to the quark sector would cite these residue expressions. The module consists entirely of named definitions for mass_exp and res objects, with no theorems or proofs.

claimThe module defines the ideal residues $r_t, r_b, r_c, r_s, r_d, r_u$ on the phi-ladder together with the corresponding mass expressions $m_q = y_0 · φ^{k_q}$ for each quark flavor $q$.

background

Recognition Science places all masses on the phi-ladder via the formula yardstick times phi to the power (rung minus 8 plus gap(Z)). The imported Constants module fixes the RS time quantum at τ₀ = 1 tick. PhiSupport records the identity φ² = φ + 1, while PhiBounds and Pow supply the interval arithmetic needed for rigorous bounds on powers of φ. ElectronMass formalizes the T9 ledger-fraction hypothesis for the electron, and ElectronMass.Necessity proves that this mass is forced from T8 ledger quantization.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The residue definitions extend the T9 electron-mass result to the quark sector and supply the ideal values required for any later comparison of experimental quark masses against the phi-ladder. They sit directly under the general mass formula introduced in ElectronMass and prepare the ground for RRF-level mass hierarchies.

scope and limits

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (25)