unity_is_equilibrium

formal source

 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
 548/-! ## The Uniform Minimizer (Explicit Solution) -/
 549
 550/-- The uniform configuration with charge σ: all entries equal exp(σ/N). -/
 551noncomputable def uniform_config {N : ℕ} (hN : 0 < N) (σ : ℝ) : Configuration N :=
 552  { entries := fun _ => Real.exp (σ / N)
 553    entries_pos := fun _ => Real.exp_pos _ }
 554
 555/-- The uniform configuration has the correct log-charge. -/
 556theorem uniform_config_charge {N : ℕ} (hN : 0 < N) (σ : ℝ) :
 557    log_charge (uniform_config hN σ) = σ := by