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') :=
proof body
Term-mode proof.
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
depends on (22)
Lean names referenced from this declaration's body.