pith. machine review for the scientific record. sign in
theorem proved term proof

equilibrium_iff_minimizer

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 517theorem equilibrium_iff_minimizer {N : ℕ}
 518    (c : Configuration N) :
 519    IsEquilibrium c ↔ ∀ c' ∈ Feasible c, total_defect c ≤ total_defect c' := by

proof body

Term-mode proof.

 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. -/

depends on (11)

Lean names referenced from this declaration's body.