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

feasible_nonempty

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)

  98theorem feasible_nonempty {N : ℕ} (c : Configuration N) :
  99    Set.Nonempty (Feasible c) := ⟨c, self_feasible c⟩

proof body

Term-mode proof.

 100
 101/-! ## The Variational Update Rule -/
 102
 103/-- **Definition (Update Rule)**: The next state is the configuration
 104    that minimizes total defect subject to conservation of log-charge.
 105
 106    This is the "equation of motion" for the ledger. -/

depends on (19)

Lean names referenced from this declaration's body.