mass_at_rung_pos
plain-language theorem explainer
The theorem proves that the mass at any natural-number rung on the phi-ladder is strictly positive whenever the base mass unit is positive. Researchers deriving quark mass hierarchies from the recognition geometry would invoke this to guarantee that all generated masses remain physically positive. The proof is a term-mode reduction that unfolds the definition and applies standard positivity lemmas for multiplication and powers.
Claim. Let $m > 0$ be a real number and let $k$ be a natural number. Then the mass at rung $k$, given by $m$ multiplied by the golden ratio to the power $k$, is strictly positive.
background
In the CKMHierarchyFromPhiLadder module the quark masses are placed on the phi-ladder according to the recognition geometry. The function mass_at_rung parameterizes the mass at rung $k$ by a base unit $m_unit$ via the definition $m_unit$ multiplied by phi to the power $k$. This builds directly on the phi-ladder structure where masses scale geometrically with rung number, as described in the module overview of the quark mass hierarchy from the phi-ladder.
proof idea
The proof is a term-mode reduction. It unfolds the mass_at_rung definition to expose the product $m_unit * phi^k$, then applies the mul_pos lemma to the hypothesis that $m_unit$ is positive together with the pow_pos lemma applied to the positivity of phi.
why it matters
This result secures the positivity of all masses generated on the phi-ladder, which is foundational for the structural predictions of quark masses in the recognition framework. It supports the module's claim that quark masses sit at specific rungs determined by gauge structure, leading to ratios such as phi^22 for the top-to-up quark mass. It touches the T6 phi fixed point and the mass formula yardstick times phi to the power (rung minus 8 plus gap).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.