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

equilibrium_attractive

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)

 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)) :=

proof body

Term-mode proof.

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

depends on (10)

Lean names referenced from this declaration's body.