variational_implies_recognition_step

formal source

 478
 479    The variational dynamics generates the defect-reducing steps that
 480    TimeEmergence postulated but never constructed. -/
 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
 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. -/
 507def IsEquilibrium {N : ℕ} (c : Configuration N) : Prop :=
 508  IsVariationalSuccessor c c
 509
 510/-- **Theorem (Equilibrium Characterization)**:
 511    A configuration is at equilibrium iff it minimizes total defect