fermionMassAt_pos
plain-language theorem explainer
The theorem establishes that the recognition-derived fermion mass at any phi-ladder rung stays strictly positive whenever the base mass is positive. Researchers verifying the structural mass spectrum for Standard Model fermions would cite it to confirm the ladder formula preserves physical positivity. The proof is a one-line term-mode reduction that unfolds the mass definition and applies the standard positivity lemmas for multiplication and powers.
Claim. Let $m_0 > 0$ be real and $k$ a natural number. Then the fermion mass at rung $k$, defined by $m_0 · φ^k$, satisfies $m_0 · φ^k > 0$.
background
The Fermion Kinetic Sector module maps the SM fermion kinetic Lagrangian to the recognition picture, with the mass term identified as J-cost on the fermion recognition ratio. The structural prediction states that the fermion mass at rung $k$ is $m_k = m_0 · φ^k$, reproducing the SM spectrum from the already-proved phi-ladder in the mass-ratio modules. The definition fermionMassAt implements this formula directly as $m_0 * phi ^ k$. The upstream Constants structure supplies the required positivity fact for phi.
proof idea
The proof is a term-mode one-liner. It unfolds fermionMassAt to expose the product $m_0 * phi^k$, then applies mul_pos to the hypothesis $0 < m_0$ together with pow_pos applied to Constants.phi_pos.
why it matters
This positivity result is required to build the FermionKineticCert certificate, which bundles fermions per generation, mass positivity, and the adjacent-ratio theorem. It fills the structural forcing step that ensures the phi-ladder mass formula yields positive values, supporting downstream spectrum calculations in the recognition framework. It directly enables the adjacent-ratio theorem used for mass ratios across rungs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.