phi_coupling_stiffness

formal source

 105  rw [Jtilde_add_int]
 106
 107/-- GCIC stiffness for base φ. -/
 108theorem phi_coupling_stiffness (δ : ℝ) :
 109    (Real.log Constants.phi * distZ δ) ^ 2 / 2 ≤
 110    Jtilde (Real.log Constants.phi) δ :=
 111  Jtilde_stiffness_lb _ δ
 112
 113/-! ## Part 3: Collective Cost Subadditivity from J-Cost -/
 114
 115/-- At alignment (ratio = 1), J-cost is zero. -/
 116theorem aligned_collective_cost_zero : Jcost 1 = 0 := Jcost_unit0
 117
 118/-- Individual perturbed costs are positive. -/
 119theorem perturbed_cost_positive {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
 120    0 < Jcost x :=
 121  Jcost_pos_of_ne_one x hx hne
 122
 123/-- A list of positive reals has positive sum. -/
 124private theorem list_sum_pos :
 125    ∀ (costs : List ℝ), 0 < costs.length → (∀ c ∈ costs, 0 < c) → 0 < costs.sum := by
 126  intro costs hlen hpos
 127  induction costs with
 128  | nil => simp at hlen
 129  | cons hd tl ih =>
 130    simp only [List.sum_cons]
 131    have hhd : 0 < hd := hpos hd (List.mem_cons.mpr (Or.inl rfl))
 132    rcases tl with _ | ⟨hd', tl'⟩
 133    · simp; linarith
 134    · have htl_pos : ∀ c ∈ (hd' :: tl'), 0 < c :=
 135        fun c hc => hpos c (List.mem_cons.mpr (Or.inr hc))
 136      have htl_len : 0 < (hd' :: tl').length := by simp
 137      linarith [ih htl_len htl_pos]
 138