fermionMassAt_succ_ratio
plain-language theorem explainer
The theorem shows fermion masses on the recognition phi-ladder scale by the factor phi at each successive rung. Model builders extracting the SM fermion spectrum from the recognition structure would cite this recursive step. The proof is a one-line wrapper that unfolds the mass definition, rewrites the power successor, and simplifies via ring.
Claim. Let $m_0 > 0$ be real and $k$ a natural number. Then the fermion mass at rung $k+1$, given by $m_0 phi^{k+1}$, equals the mass at rung $k$ multiplied by $phi$.
background
The function fermionMassAt supplies the mass at rung $k$ on the phi-ladder via the explicit formula $m_0 phi^k$. This declaration lives inside the Fermion Kinetic Sector module, which translates the SM Dirac Lagrangian into recognition terms where the mass term is J-cost on the fermion recognition ratio. The upstream definition fermionMassAt directly encodes the phi-ladder scaling that the present theorem makes recursive.
proof idea
The proof is a one-line wrapper. It unfolds the definition of fermionMassAt, rewrites the exponent using the successor power rule, and closes with ring simplification.
why it matters
This step completes the recursive half of the structural prediction $m_k = m_0 phi^k$ that reproduces the SM mass spectrum from the recognition phi-ladder. It is invoked directly by the adjacent-ratio theorem that normalizes consecutive masses to phi. The result sits inside the T6 forcing of phi as self-similar fixed point and the mass-formula yardstick on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.