aligned_collective_cost_zero

formal source

 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
 139/-- **COLLECTIVE SUBADDITIVITY FROM J-COST** (replaces empirical axiom)
 140
 141    The aligned configuration (J=0) is strictly less costly than any collection
 142    of perturbed boundaries (Σ J(xᵢ) > 0 when xᵢ ≠ 1). -/
 143theorem aligned_beats_perturbed
 144    (costs : List ℝ) (hlen : 0 < costs.length)
 145    (hpos : ∀ c ∈ costs, 0 < c) :
 146    Jcost 1 < costs.sum := by