mass_ratio_from_rung_difference
plain-language theorem explainer
Mass ratios on the Recognition Science phi-ladder satisfy m2/m1 = phi^(r2-r1) for coherent energy scale E_coh > 0 and integer rungs r1, r2. Researchers deriving particle mass hierarchies from rung assignments in the RS framework would invoke this identity. The proof reduces the ratio by canceling E_coh after non-zero checks and applies the real exponent addition law.
Claim. Let $m_1 = E_coh · ϕ^{r_1}$ and $m_2 = E_coh · ϕ^{r_2}$ with $E_coh > 0$. Then $m_2 / m_1 = ϕ^{r_2 - r_1}$.
background
The phi-ladder expresses masses as m = E_coh · ϕ^r for integer rung r, where ϕ > 1 is the self-similar fixed point. Rung maps assign integers to sectors (leptons, quarks) via noncomputable definitions in AnchorPolicy and RSBridge.Anchor, with explicit values such as rung(e) = 2 and rung(u) = 4. The module supplies algebraic proofs that all such ratios are exact ϕ-powers, resting on Mass as ℝ and the positivity facts imported from PhiForcing.
proof idea
The tactic proof introduces the mass definitions via reflexivity, proves E_coh ≠ 0 by linarith, shows ϕ^{r1} ≠ 0 via phi_pos and positivity, cancels via field_simp, rewrites the exponents with Real.rpow_add, and finishes by congruence on the difference after simp.
why it matters
This supplies the elementary ratio step that supports mass_ordering_from_rungs in the same module and the general phi-ladder mass formula. It closes the algebraic gap between rung assignments and observable ratios inside the forcing chain, without touching open questions on specific particle spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.