DownQuarkMasses
plain-language theorem explainer
DownQuarkMasses defines the record type bundling the three down-type quark masses in GeV units. Physicists reconstructing the fermion spectrum from the φ-cascade cite this structure to package the down, strange, and bottom values for insertion into the mass-ladder formulas. The declaration is a pure record introduction with an empty body and no lemmas or tactics.
Claim. The record type DownQuarkMasses consists of three real numbers down, strange, bottom ∈ ℝ that represent the masses of the down, strange, and bottom quarks in GeV.
background
Recognition Science derives the Standard Model fermion mass hierarchy from a geometric φ-cascade generated by the eight-tick octave. Successive generations differ by factors φ² or φ³, so that powers such as φ²⁴ span the observed range from the top quark down to the electron. The module Physics.MassHierarchy therefore supplies one record type per sector so that concrete values can be supplied to the cascade expressions.
proof idea
This is a structure definition that introduces the record type with three fields of type ℝ. No lemmas are applied and the body is empty, as required for a pure inductive record declaration.
why it matters
The structure supplies the down-sector container instantiated by observedDownQuarks. It forms part of the SM-006 construction that accounts for the fermion hierarchy through the φ-cascade, where the eight-tick structure and geometric progression replace the usual Yukawa parameters. The parent result is the overall mass-hierarchy assembly that combines all sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.