527theorem unity_is_equilibrium {N : ℕ} (hN : 0 < N) : 528 IsEquilibrium (unity_config N hN) := by
proof body
Term-mode proof.
529 constructor 530 · exact self_feasible _ 531 · intro c' hc' 532 rw [unity_defect_zero hN] 533 exact total_defect_nonneg c' 534 535/-- **Theorem (Equilibrium Is Attractive)**: 536 Every variational trajectory converges to equilibrium in the sense 537 that total defect is non-increasing and bounded below by zero. 538 539 The defect sequence {total_defect(traj(t))} is monotone decreasing 540 and bounded below, hence convergent. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.