observedUpQuarks
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.