observedUpQuarks
This definition supplies the measured up-type quark masses as a record of type UpQuarkMasses with components 0.002 GeV, 1.27 GeV and 173 GeV. Modelers comparing Recognition Science φ-cascade predictions to Standard Model data would reference these values as the empirical target. The definition is a direct record literal with no computation or lemmas applied.
claimThe observed up-type quark masses are the record with components $m_u = 0.002$, $m_c = 1.27$, $m_t = 173$ expressed in GeV.
background
The module derives the fermion mass hierarchy from the φ-cascade that follows from the eight-tick structure and the Recognition Composition Law. UpQuarkMasses is the structure that packages the three up-type quark masses as real numbers in GeV units. This definition supplies the numerical inputs that later cascade formulas attempt to reproduce from powers of φ.
proof idea
The definition is a direct record construction that populates the three fields with the listed numerical values.
why it matters in Recognition Science
This definition anchors the φ-cascade mass hierarchy derivation in the Recognition Science framework by providing the empirical targets for the up-type sector. It supports the module's core claim that geometric progression with φ powers accounts for the observed spread from electron to top quark scales. No downstream theorems currently depend on it.
scope and limits
- Does not derive the masses from the φ-ladder or Recognition Composition Law.
- Does not specify renormalization scale or running effects.
- Does not include experimental uncertainties or error bars.
formal statement (Lean)
71noncomputable def observedUpQuarks : UpQuarkMasses := {
proof body
Definition body.
72 up := 0.002, -- GeV (running mass)
73 charm := 1.27, -- GeV
74 top := 173 -- GeV
75}
76
77/-- Down-type quark masses (GeV). -/