UpQuarkMasses
plain-language theorem explainer
UpQuarkMasses packages the three up-type quark masses as real numbers in GeV. Physicists constructing the fermion spectrum from the Recognition Science φ-cascade cite this structure when assigning concrete values to the up, charm, and top quarks. The declaration is a bare structure definition carrying no proof obligations or computational content.
Claim. A record whose fields are three real numbers denoting the masses of the up, charm, and top quarks, expressed in GeV.
background
Recognition Science obtains the fermion mass hierarchy from a geometric φ-cascade in which each generation differs by factors of φ² or φ³. The module documentation states that the eight-tick octave produces three generations whose ratios span the observed range from the top quark near 173 GeV down to the electron near 0.5 MeV, with the mass formula given by yardstick times φ raised to (rung minus 8 plus gap(Z)). UpQuarkMasses collects the up-type sector; sibling structures handle charged leptons and down-type quarks, all feeding the cascadeMass function that places each particle on the φ-ladder.
proof idea
The declaration is a structure definition with no proof body, no lemmas applied, and no tactics.
why it matters
This structure supplies the concrete mass values instantiated by observedUpQuarks and thereby supports the SM-006 derivation of the full fermion hierarchy from the φ-cascade. It connects directly to the eight-tick octave (T7) and the mass formula yardstick × φ^(rung - 8 + gap(Z)). The parent definition observedUpQuarks uses these fields to anchor the numerical spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.