mass_geometric
plain-language theorem explainer
Masses on the phi-ladder obey the recurrence that the value at rung k+1 equals phi times the value at rung k for any base unit m_unit. Quark mass modelers working in Recognition Science cite this to establish the exact geometric progression in the six-quark spectrum. The proof is a direct algebraic reduction that unfolds the mass_at_rung definition, applies the successor power identity, and closes by ring simplification.
Claim. For any base mass unit $m_0$ in the reals and any natural number $k$, the mass at rung $k+1$ defined by $m_0 · φ^k$ satisfies $m(k+1) = m(k) · φ$.
background
The module derives the CKM quark mass hierarchy by placing the six quarks on the phi-ladder, where the mass function is defined as mass_at_rung m_unit k := m_unit * phi ^ k. This supplies the explicit scaling between consecutive rungs using the golden ratio phi. The local theoretical setting is the RS reading of the Standard Model spectrum, with rung assignments u:8, d:9, s:14, c:17, b:22, t:30 as stated in the module documentation.
proof idea
The proof unfolds the definition of mass_at_rung to expose the power expression, rewrites the exponent via the successor rule pow_succ, and finishes with the ring tactic to obtain the required identity.
why it matters
This supplies the geometric clause inside the CKMHierarchyFromPhiLadderCert structure and is invoked by ckm_hierarchy_one_statement to record that adjacent rungs differ by exactly phi. It realizes the self-similar scaling forced by phi in the Recognition framework, supporting the structural claim that the top-to-up ratio equals phi^22.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.