pith. machine review for the scientific record. sign in
theorem proved term proof high

rung_ratio

show as:
view Lean formalization →

The ratio of masses on adjacent rungs of the phi-ladder equals phi for any positive yardstick and integer index. Researchers modeling the Recognition Science mass hierarchy would cite this to confirm geometric self-similarity of the spectrum. The proof rewrites the numerator via the adjacent scaling relation, invokes positivity to confirm the denominator is nonzero, and cancels the common factor.

claimFor any positive real $y_s > 0$ and integer $n$, the ratio of the mass-energy at rung $n+1$ to the mass-energy at rung $n$ equals $phi$, where the mass-energy at rung $k$ is $y_s$ times $phi^k$.

background

In the Spectral Emergence module the phi-ladder mass hierarchy is derived from the forced self-similar fixed point phi after T8 fixes D=3 and the eight-tick octave. The mass-energy at rung n is defined as yardstick times phi to the power n. Positivity of this quantity for positive yardstick follows from positivity of phi. The adjacent scaling relation states that the mass-energy at rung n+1 equals phi times the mass-energy at rung n.

proof idea

The proof applies the adjacent scaling theorem to replace the numerator, uses the positivity theorem to obtain that the denominator is nonzero, and cancels via the division cancellation lemma.

why it matters in Recognition Science

This result establishes self-similarity of the phi-ladder, which underpins the mass formula yardstick times phi to the (rung minus 8 plus gap) in the Recognition Science spectrum. It directly supports the module claim that the ratio between any two rungs separated by k steps is phi to the k. The declaration sits downstream of the mass definition, positivity, and scaling lemmas inside the Q3-derived structure that also yields SU(3) x SU(2) x U(1) and three generations.

scope and limits

formal statement (Lean)

 301theorem rung_ratio (ys : ℝ) (hys : 0 < ys) (n : ℤ) :
 302    mass_rung ys (n + 1) / mass_rung ys n = phi := by

proof body

Term-mode proof.

 303  rw [mass_rung_step]
 304  have hmr : mass_rung ys n ≠ 0 := ne_of_gt (mass_rung_pos ys hys n)
 305  rw [mul_div_cancel_right₀ phi hmr]
 306
 307/-- **THEOREM**: The φ-ladder is self-similar: the ratio between
 308    ANY two rungs separated by k steps is φ^k. -/

depends on (9)

Lean names referenced from this declaration's body.