mass_ladder_strictly_increasing
plain-language theorem explainer
The mass ladder theorem shows that for any positive real y and natural number n the quantity y times phi to the n is strictly less than y times phi to the n plus one. Researchers modeling the Recognition Science fermion spectrum on the phi-ladder would cite this to guarantee that higher rungs carry strictly greater mass. The short tactic proof factors out the positive y and reduces the inequality to the defining property one less than phi via the multiplicative identity.
Claim. For any real number $y > 0$ and natural number $n$, $y phi^n < y phi^{n+1}$.
background
In the Recognition Science framework the mass ladder is given by m_r = y · phi^r, where phi is the self-similar fixed point forced at T6 and satisfying phi > 1. This theorem sits inside the Quantum-Gravity Octave Duality module, whose central result is the proved identity kappa · hbar = 8 arising from the J-cost functional J(x) = (x - 1)^2 / (2x) that encodes the eight-tick octave. The module documentation states that the fermion mass spectrum satisfies the Fibonacci recurrence phi^(n+2) = phi^(n+1) + phi^n, making the strict increase of successive rungs a prerequisite for the mass formula yardstick · phi^(rung - 8 + gap(Z)). Upstream, the lemma one_lt_phi supplies the key inequality phi > 1 used in every ladder comparison.
proof idea
The proof applies mul_lt_mul_of_pos_left to the positive factor y, reducing the claim to phi^n < phi^{n+1}. It rewrites the left side as phi^n · 1 using the theorem mul_one, then applies mul_lt_mul_of_pos_left again with one_lt_phi and the positivity of phi^n, and finishes with the ring tactic to equate the right-hand side with phi^{n+1}.
why it matters
This result underwrites the module claim that the mass spectrum forms a Fibonacci sequence of energies (QG-005). It rests on the phi-ladder structure derived from the single J-cost functional and the eight-tick octave that also forces D = 3 and the alpha band. Because the used-by list is empty, the theorem functions as a local supporting fact rather than a direct parent for further declarations in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.