J_phi

formal source

 260
 261/-- J-cost at x = φ: the fundamental coherence cost.
 262    J(φ) = ½(φ + φ⁻¹) - 1 = ½(φ + φ-1) - 1 = ½√5 - 1 ≈ 0.118 -/
 263def J_phi : ℝ := Jcost phi
 264
 265/-- **THEOREM**: J(φ) > 0. Departure from unity always costs. -/
 266theorem J_phi_pos : 0 < J_phi := by
 267  unfold J_phi
 268  rw [Jcost_eq_sq (ne_of_gt phi_pos)]
 269  apply div_pos
 270  · have : phi - 1 ≠ 0 := sub_ne_zero.mpr phi_ne_one
 271    positivity
 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