equilibrium_iff_minimizer

formal source

 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.
 538
 539    The defect sequence {total_defect(traj(t))} is monotone decreasing
 540    and bounded below, hence convergent. -/
 541theorem equilibrium_attractive {N : ℕ}
 542    (traj : Trajectory N)
 543    (h : IsVariationalTrajectory traj) :
 544    (∀ t, total_defect (traj (t + 1)) ≤ total_defect (traj t)) ∧
 545    (∀ t, 0 ≤ total_defect (traj t)) :=
 546  ⟨trajectory_defect_monotone traj h, fun t => total_defect_nonneg (traj t)⟩
 547