aligned_beats_perturbed

formal source

 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
 147  rw [Jcost_unit0]
 148  exact list_sum_pos costs hlen hpos
 149
 150/-! ## Part 4: Full Derivation Certificate -/
 151
 152theorem gcic_derivation_cert :
 153    (∀ lam δ, Jtilde lam 0 ≤ Jtilde lam δ) ∧
 154    (∀ (costs : List ℝ), 0 < costs.length → (∀ c ∈ costs, 0 < c) → Jcost 1 < costs.sum) ∧
 155    (Jcost 1 = 0) :=
 156  ⟨phase_alignment_minimizes_Jtilde, aligned_beats_perturbed, Jcost_unit0⟩
 157
 158end
 159
 160end IndisputableMonolith.Papers.GCIC.GCICDerivation