mass_rung

formal source

 281  rw [phi_sq_eq]
 282
 283/-- The mass-energy at rung n on the φ-ladder. -/
 284def mass_rung (yardstick : ℝ) (n : ℤ) : ℝ :=
 285  yardstick * phi ^ (n : ℝ)
 286
 287/-- **THEOREM**: Moving up one rung scales mass by φ. -/
 288theorem mass_rung_step (ys : ℝ) (n : ℤ) :
 289    mass_rung ys (n + 1) = phi * mass_rung ys n := by
 290  unfold mass_rung
 291  push_cast
 292  rw [Real.rpow_add (by exact phi_pos), Real.rpow_one]
 293  ring
 294
 295/-- **THEOREM**: Mass is positive for positive yardstick. -/
 296theorem mass_rung_pos (ys : ℝ) (hys : 0 < ys) (n : ℤ) :
 297    0 < mass_rung ys n :=
 298  mul_pos hys (Real.rpow_pos_of_pos phi_pos _)
 299
 300/-- **THEOREM**: The ratio of adjacent rungs is exactly φ. -/
 301theorem rung_ratio (ys : ℝ) (hys : 0 < ys) (n : ℤ) :
 302    mass_rung ys (n + 1) / mass_rung ys n = phi := by
 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. -/
 309theorem rung_separation (ys : ℝ) (hys : 0 < ys) (n k : ℤ) :
 310    mass_rung ys (n + k) / mass_rung ys n = phi ^ (k : ℝ) := by
 311  have hmr : mass_rung ys n ≠ 0 := ne_of_gt (mass_rung_pos ys hys n)
 312  rw [div_eq_iff hmr]
 313  unfold mass_rung
 314  rw [show ((n + k : ℤ) : ℝ) = (n : ℝ) + (k : ℝ) from by push_cast; ring]