theorem
proved
variational_step_reduces_defect
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.VariationalDynamics on GitHub at line 343.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
tick -
tick -
of -
Configuration -
total_defect -
A -
is -
of -
Configuration -
is -
of -
IsVariationalSuccessor -
self_feasible -
is -
of -
A -
is -
A -
trajectory -
next
used by
formal source
340 This follows immediately: the current state is feasible for itself,
341 and the successor minimizes over the feasible set, so the successor's
342 cost is at most the current state's cost. -/
343theorem variational_step_reduces_defect {N : ℕ}
344 (c next : Configuration N)
345 (h : IsVariationalSuccessor c next) :
346 total_defect next ≤ total_defect c :=
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. -/
353def Trajectory (N : ℕ) := ℕ → Configuration N
354
355/-- **Definition**: A trajectory follows the variational dynamics if
356 each successive pair satisfies the variational update rule. -/
357def IsVariationalTrajectory {N : ℕ} (traj : Trajectory N) : Prop :=
358 ∀ t, IsVariationalSuccessor (traj t) (traj (t + 1))
359
360/-- **Theorem (Deterministic Evolution)**:
361 If two trajectories start from the same initial state and both
362 follow the variational dynamics, they are identical.
363
364 This is the equation-of-motion analogue of Laplacian determinism:
365 initial conditions + update rule = unique future. -/
366theorem variational_dynamics_deterministic {N : ℕ} (hN : 0 < N)
367 (traj₁ traj₂ : Trajectory N)
368 (h₁ : IsVariationalTrajectory traj₁)
369 (h₂ : IsVariationalTrajectory traj₂)
370 (h_init : (traj₁ 0).entries = (traj₂ 0).entries) :
371 ∀ t, (traj₁ t).entries = (traj₂ t).entries := by
372 intro t
373 induction t with