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

variational_implies_recognition_step

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)

 481theorem variational_implies_recognition_step {N : ℕ}
 482    (c next : Configuration N)
 483    (h : IsVariationalSuccessor c next)
 484    (tick_val : ℕ) :
 485    ∃ step : RecognitionStep,
 486      step.input.defect = total_defect c ∧
 487      step.output.defect = total_defect next := by

proof body

Term-mode proof.

 488  refine ⟨{
 489    input := {
 490      tick := ⟨tick_val⟩
 491      defect := total_defect c
 492      defect_nonneg := total_defect_nonneg c
 493    }
 494    output := {
 495      tick := ⟨tick_val + 1⟩
 496      defect := total_defect next
 497      defect_nonneg := total_defect_nonneg next
 498    }
 499    tick_advance := rfl
 500    defect_reduce := variational_step_reduces_defect c next h
 501  }, rfl, rfl⟩
 502
 503/-! ## The Equilibrium Fixed Point -/
 504
 505/-- **Definition**: A configuration is at equilibrium if it is its own
 506    variational successor. -/

depends on (22)

Lean names referenced from this declaration's body.