upsilon_star_eq_phi

formal source

  73    Υ★ = φ ≈ 1.618 -/
  74def upsilon_star : ℝ := phi
  75
  76theorem upsilon_star_eq_phi : upsilon_star = phi := rfl
  77
  78theorem upsilon_star_bounds : 1.5 < upsilon_star ∧ upsilon_star < 1.62 := by
  79  unfold upsilon_star
  80  exact ⟨phi_gt_onePointFive, phi_lt_onePointSixTwo⟩
  81
  82/-- Upsilon-star bounds imply positivity of the stellar mass-to-light ratio. -/
  83theorem upsilon_star_bounds_implies_pos (h : 1.5 < upsilon_star ∧ upsilon_star < 1.62) :
  84    0 < upsilon_star := by
  85  linarith [h.1]
  86
  87/-! ## 3. C_ξ (Morphology Coupling) — HAS RS BASIS
  88
  89The morphology coupling coefficient is 2φ⁻⁴.
  90
  91**Physical motivation:** The factor 2 is fundamental (from 2³ = 8 tick structure).
  92The φ⁻⁴ is one power above E_coh = φ⁻⁵. -/
  93
  94/-- The RS-based morphology coupling coefficient.
  95    C_ξ = 2 · φ⁻⁴ ≈ 0.292 -/
  96def C_xi : ℝ := 2 * phi ^ (-(4 : ℝ))
  97
  98/-- C_ξ is positive.
  99    Paper fitted value: 0.298 ± 0.015
 100    RS prediction: 2/φ⁴ ≈ 0.292
 101    Match: 2% -/
 102theorem C_xi_pos : 0 < C_xi := by
 103  unfold C_xi
 104  have hphi_pos := phi_pos
 105  apply mul_pos (by norm_num : (0:ℝ) < 2)
 106  exact Real.rpow_pos_of_pos hphi_pos _