J_one_zero

formal source

 272  · linarith [phi_pos]
 273
 274/-- **THEOREM**: J(1) = 0. The identity state has zero cost. -/
 275theorem J_one_zero : Jcost 1 = 0 := Jcost_unit0
 276
 277/-- **THEOREM**: J(φ²) = J(φ+1) by the golden ratio identity φ²=φ+1.
 278    Each step up the φ-ladder is controlled by the Fibonacci recursion. -/
 279theorem J_phi_sq_identity :
 280    Jcost (phi ^ 2) = Jcost (phi + 1) := by
 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]