mass_ratio_is_phi
plain-language theorem explainer
The ratio of consecutive terms in the mass ladder m_r = y φ^r equals φ for positive y and natural n. Modelers of the Recognition Science fermion spectrum cite this to confirm the constant scaling that yields the Fibonacci recurrence. The proof is a direct algebraic cancellation: positivity of φ^n is asserted, field_simp removes the common factors, and ring reduces the quotient to φ.
Claim. For $y > 0$ and $n$ a natural number, $(y φ^{n+1}) / (y φ^n) = φ$.
background
The Quantum-Gravity Octave Duality module derives κ · ℏ = 8 from the single J-cost functional, with J(x) = (x − 1)² / (2x) exactly the AM-GM gap of the pair {x, x⁻¹}. Constants are fixed as κ = 8φ⁵ and ℏ = φ⁻⁵, so their product is the octave factor 8. The mass spectrum is introduced as m_r = y φ^r; the present theorem isolates the scaling property of this ladder.
proof idea
Term-mode proof. First assert (0 : ℝ) < φ^n via pow_pos. Then field_simp cancels y and φ^n using the two positivity hypotheses to clear denominators. Finally ring reduces the remaining expression to φ.
why it matters
Supports the QG-004 statement that the mass ladder obeys the Fibonacci recurrence m_{r+2} = m_{r+1} + m_r once the constant ratio φ is available. It supplies the algebraic step required by the phi-ladder mass formula and the self-similar fixed point T6. No downstream theorems are recorded, so the result functions as a local lemma inside the octave-duality certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.