observedDownQuarks
plain-language theorem explainer
observedDownQuarks supplies the empirical down-type quark masses in GeV for the φ-cascade model of fermion hierarchy. Particle physicists modeling mass ratios from Recognition Science constants would reference these values as the base data layer. The definition is a direct record construction that populates the DownQuarkMasses structure with three fixed real numbers and no further computation.
Claim. The observed down-type quark masses are given by the record $m_d = 0.005$, $m_s = 0.095$, $m_b = 4.18$ in GeV units.
background
DownQuarkMasses is the structure holding three real numbers for the down, strange, and bottom quarks. Mass is the alias for ℝ in RS-native units. The module sets the local context as SM-006, deriving the Standard Model fermion hierarchy from the φ-cascade: each generation differs by a geometric factor built from powers of φ, with three generations fixed by the eight-tick octave. Upstream, the Model structure from LawOfExistence supplies the defectMass and energyGap maps that later consume these numerical inputs.
proof idea
The definition is a direct record literal that applies the DownQuarkMasses constructor to the three supplied real constants.
why it matters
This definition supplies the concrete numerical anchor for the φ-cascade derivation of the fermion mass hierarchy. It fills the input slot required by the PRL proposition on mass hierarchy from first principles and connects to the eight-tick structure that forces three generations. No downstream theorems yet cite it, leaving the cascadeMass and koideParameter siblings as the immediate next consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.