fermionMassAt
plain-language theorem explainer
The definition sets fermion mass at rung k on the phi-ladder to m0 times phi to the power k. Particle physicists deriving SM mass hierarchies from recognition J-cost would cite this scaling. It is a direct unfolding of the phi-ladder already fixed in the constants and mass-ratio modules.
Claim. $m_k = m_0 φ^k$, where $m_k$ denotes the fermion mass at rung $k$ on the recognition phi-ladder and $m_0$ is the base mass at rung zero.
background
The 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 stated in the module documentation is that fermion mass at any rung k equals m0 times phi to the k, reproducing the SM spectrum from the phi-ladder proved in the mass-ratio modules. Phi itself is the self-similar fixed point forced at step T6 of the unified forcing chain.
proof idea
One-line definition that directly unfolds the phi-ladder scaling already established in Constants.phi_pos and the power rules imported from Mathlib.
why it matters
This definition supplies the explicit mass scaling required by the FermionKineticCert structure, which certifies fermions_per_gen, mass positivity, and adjacent ratios. It implements the structural prediction quoted in the module documentation for the recognition Dirac operator. The scaling connects directly to the mass formula on the phi-ladder and the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.