mass_rung_pos
plain-language theorem explainer
Mass at each rung of the phi-ladder is strictly positive whenever the yardstick is positive. Researchers modeling the Recognition Science mass hierarchy cite this to guarantee all derived particle masses remain positive. The proof is a one-line term that multiplies the positive yardstick by the positive value of phi to any real power.
Claim. Let $y_s > 0$ be a positive real yardstick and let $n$ be any integer. Then the mass at rung $n$, given by $y_s$ times phi to the power $n$, is strictly positive.
background
The Spectral Emergence module derives the Standard Model gauge groups, three generations, and the phi-ladder mass hierarchy from the binary cube Q3 forced by D=3. The mass at rung n equals the yardstick multiplied by phi raised to n, placing energies on discrete tiers scaled by the self-similar fixed point phi. This rests on the J-cost structure and ledger factorization imported from upstream modules.
proof idea
The proof is a one-line term that applies mul_pos to the hypothesis that the yardstick is positive together with the fact that phi to any real power is positive.
why it matters
This result supports rung_ratio and rung_separation, which establish exact phi scaling between any rungs, and feeds the master spectral_emergence theorem that certifies the full Standard Model plus consciousness structure from D=3. It secures positivity for the mass formula on the phi-ladder, consistent with T6 forcing of phi and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.