mass_ordering_from_rungs
plain-language theorem explainer
The result shows that masses defined as E_coh times phi to an integer rung increase strictly with the rung when E_coh exceeds zero. Researchers deriving particle spectra from the Recognition Science phi-ladder would invoke it to fix the ordering of states. The proof rewrites the two mass expressions, invokes the real-power monotonicity lemma that rests on one_lt_phi, and closes with nlinarith on the positivity facts.
Claim. Let $m(r) = E_coh · ϕ^r$ for integer $r$. If $r_1 < r_2$ and $E_coh > 0$, then $m(r_1) < m(r_2)$.
background
The module supplies rigorous proofs that all mass ratios on the phi-ladder are exact powers of phi. Masses are expressed in RS-native units where the coherent energy scale E_coh multiplies phi raised to the rung index. The upstream lemma one_lt_phi states that phi exceeds 1 and is proved by comparing sqrt(5) to 2 and applying the monotonicity of the square root.
proof idea
The tactic proof introduces the two mass expressions via rfl, rewrites them into the goal, applies Real.rpow_lt_rpow_of_exponent_lt using one_lt_phi and the hypothesis r1 < r2, then finishes with nlinarith on the two positivity facts Real.rpow_pos_of_pos phi_pos r1 and Real.rpow_pos_of_pos phi_pos r2.
why it matters
The theorem secures monotonicity of the mass formula on the phi-ladder, a direct consequence of the self-similar fixed point phi forced in the T6 step of the unified forcing chain. It supplies the ordering needed for the mass certificate section that follows in the same module and for any later comparison of rung states against observed particle masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.