mass_at_rung
plain-language theorem explainer
The definition supplies the closed-form quark mass at integer rung k on the phi-ladder as base unit times phi to the power k. Recognition Science modelers of the CKM hierarchy cite it to obtain the six-quark ratios from rung assignments u:8 through t:30. The definition is a direct algebraic assignment with no reduction steps.
Claim. The mass at rung $k$ is $m(k) = m_0 · ϕ^k$, where $m_0$ is the base mass unit and $ϕ$ is the golden-ratio fixed point.
background
In the CKM Quark Mass Hierarchy module the six quarks occupy rungs on the phi-ladder forced by the recognition geometry: u at rung 8, d at 9, s at 14, c at 17, b at 22, t at 30. The module sets the base unit to $ϕ^{-5}/8$ and derives all masses from the single formula supplied by this definition. The phi-ladder itself originates in the self-similar fixed point of the unified forcing chain (T6) and the Recognition Composition Law.
proof idea
Direct definition that unfolds immediately to the product of the supplied base unit and the power of phi. No lemmas or tactics are invoked.
why it matters
This definition is the primitive that feeds the master certificate CKMHierarchyFromPhiLadderCert and the one-statement theorem ckm_hierarchy_one_statement. It realizes the phi-ladder mass scaling required by Track F7, yielding the structural prediction $m_t/m_u = ϕ^{22} ≈ 39{,}000$ (within factor 2 of the measured 80{,}000) and the strict ordering u < d < s < c < b < t. It closes the link between the eight-tick octave and observable quark masses without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.