`variational_dynamics_certificate`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.VariationalDynamics
domain: Foundation
line: 615 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.VariationalDynamics on GitHub at line 615.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 612    subject to a conservation constraint. This is what makes "recognition"
 613    a genuinely non-local process: the optimal state of each ledger entry
 614    depends on every other entry through the shared constraint. -/
 615theorem variational_dynamics_certificate {N : ℕ} (hN : 0 < N)
 616    (c : Configuration N) :
 617    -- 1. A successor exists
 618    (∃ next, IsVariationalSuccessor c next) ∧
 619    -- 2. Defect reduces
 620    (∀ next, IsVariationalSuccessor c next → total_defect next ≤ total_defect c) ∧
 621    -- 3. Unity is equilibrium for zero-charge
 622    IsEquilibrium (unity_config N hN) ∧
 623    -- 4. Equilibrium is attractive (defect bounded below)
 624    (∀ c' : Configuration N, 0 ≤ total_defect c') :=
 625  ⟨variational_step_exists hN c,
 626   fun next h => variational_step_reduces_defect c next h,
 627   unity_is_equilibrium hN,
 628   fun c' => total_defect_nonneg c'⟩
 629
 630end VariationalDynamics
 631end Foundation
 632end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.