IsEquilibrium

formal source

 504
 505/-- **Definition**: A configuration is at equilibrium if it is its own
 506    variational successor. -/
 507def IsEquilibrium {N : ℕ} (c : Configuration N) : Prop :=
 508  IsVariationalSuccessor c c
 509
 510/-- **Theorem (Equilibrium Characterization)**:
 511    A configuration is at equilibrium iff it minimizes total defect
 512    over its feasible set — iff it is the unique minimizer.
 513
 514    For log-charge = 0, this is the unity configuration (all entries = 1).
 515    For general log-charge σ, this is the uniform configuration
 516    (all entries = exp(σ/N)). -/
 517theorem equilibrium_iff_minimizer {N : ℕ}
 518    (c : Configuration N) :
 519    IsEquilibrium c ↔ ∀ c' ∈ Feasible c, total_defect c ≤ total_defect c' := by
 520  constructor
 521  · intro ⟨_, hmin⟩
 522    exact hmin
 523  · intro hmin
 524    exact ⟨self_feasible c, hmin⟩
 525
 526/-- **Theorem**: The unity configuration is an equilibrium when log-charge = 0. -/
 527theorem unity_is_equilibrium {N : ℕ} (hN : 0 < N) :
 528    IsEquilibrium (unity_config N hN) := by
 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.