mesonMass
plain-language theorem explainer
mesonMass supplies the explicit mass at rung k on the phi-ladder as phi raised to k in RS-native units. Hadron spectroscopists cite it when deriving the adjacent-family mass ratios that match the self-similar fixed point. The definition is a direct one-line assignment with no lemmas or computation.
Claim. The mass at level $k$ on the phi-ladder is $m_k = phi^k$ (in units where the base scale is 1).
background
The module places the five canonical meson families (pseudoscalar, vector, scalar, axial-vector, tensor) on the phi-ladder with configDim equal to 5. Adjacent families occupy successive rungs so that their mass ratio equals phi by construction. The phi-ladder itself is the discrete scaling sequence generated by the self-similar fixed point phi forced at T6 of the unified forcing chain.
proof idea
The declaration is a direct definition that sets mesonMass k equal to phi raised to the power k. No lemmas are applied and no tactics are used.
why it matters
The definition is invoked by mass_pos to prove positivity, by mass_ratio to recover the exact phi scaling, and by MesonSpectrumCert to certify the five-family structure with positive masses and phi ratios. It supplies the concrete mass assignment for the S2 depth meson spectrum. In the framework it realizes the phi-ladder component of the general mass formula, consistent with T6 phi fixed point and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.