closed_ratio_is_phi

formal source

 126
 127Combining with the previous theorem: the only positive ratio that
 128makes a geometric scale sequence closed is φ = (1 + √5)/2. -/
 129theorem closed_ratio_is_phi (S : GeometricScaleSequence)
 130    (h_closed : S.isClosed) : S.ratio = phi := by
 131  have h_eq := closure_forces_golden_equation S h_closed
 132  have h_pos := S.ratio_pos
 133  -- Both S.ratio and φ satisfy x² = x + 1
 134  -- For x > 0, this equation has unique solution φ
 135  have h_phi_eq : phi ^ 2 = phi + 1 := phi_sq_eq
 136  -- The difference (r - φ) satisfies: (r-φ)(r+φ) = r² - φ² = (r+1) - (φ+1) = r - φ
 137  -- So (r - φ)(r + φ - 1) = 0
 138  have h_factor : (S.ratio - phi) * (S.ratio + phi - 1) = 0 := by
 139    have := h_eq  -- r² = r + 1
 140    have := h_phi_eq  -- φ² = φ + 1
 141    ring_nf
 142    nlinarith [sq_nonneg S.ratio, sq_nonneg phi]
 143  -- Since r > 0 and φ > 1, we have r + φ - 1 > 0, so r - φ = 0
 144  rcases mul_eq_zero.mp h_factor with h_diff | h_sum
 145  · linarith
 146  · -- If r + φ - 1 = 0, then r = 1 - φ < 0, contradiction with r > 0
 147    have : S.ratio = 1 - phi := by linarith
 148    have : S.ratio < 0 := by
 149      have hphi : phi > 1 := one_lt_phi
 150      linarith
 151    linarith
 152
 153/-! ## Why Additive Composition? A J-Cost Argument -/
 154
 155/-- The J-cost of a scale ratio -/
 156noncomputable def J (x : ℝ) : ℝ := Cost.Jcost x
 157
 158/-- Exact decomposition of the J-cost composition identity.
 159