quarkMass
plain-language theorem explainer
The declaration sets the mass of a quark at integer rung k on the phi-ladder to phi raised to k. Researchers deriving coarse quark mass ratios or positivity statements in Recognition Science cite this when building the six-flavour hierarchy. The definition is a direct assignment with no computation or lemmas.
Claim. The mass at rung $k$ on the phi-ladder is given by $m_k = phi^k$.
background
The module places the six quark flavours (up, down, strange, charm, bottom, top) on a phi-ladder mass scale, with six equal to three generations times two charge types. The phi-ladder implements the self-similar fixed point phi from the forcing chain T6. The downstream QuarkMassCert structure records the six-flavour count, the three-times-two partition, the constant adjacent ratio phi, and strict positivity of all masses.
proof idea
One-line definition that directly assigns phi^k to the mass at rung k.
why it matters
This supplies the mass function required by QuarkMassCert to certify the six-flavour count, the partition 6 = 3 * 2, the ratio property, and positivity. It realises the Recognition Science mass scaling on the phi-ladder (T6) and supports the coarse structural hierarchy before finer corrections such as yardstick or gap(Z) terms are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.