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

variational_step_reduces_defect

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)

 343theorem variational_step_reduces_defect {N : ℕ}
 344    (c next : Configuration N)
 345    (h : IsVariationalSuccessor c next) :
 346    total_defect next ≤ total_defect c :=

proof body

Term-mode proof.

 347  h.2 c (self_feasible c)
 348
 349/-! ## Deterministic Evolution -/
 350
 351/-- **Definition**: A ledger trajectory is a sequence of configurations
 352    indexed by tick count. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.