trajectory_defect_monotone

formal source

 400
 401/-- **Theorem (Monotone Defect Along Trajectories)**:
 402    Total defect is non-increasing along any variational trajectory. -/
 403theorem trajectory_defect_monotone {N : ℕ}
 404    (traj : Trajectory N)
 405    (h : IsVariationalTrajectory traj) :
 406    ∀ t, total_defect (traj (t + 1)) ≤ total_defect (traj t) :=
 407  fun t => variational_step_reduces_defect (traj t) (traj (t + 1)) (h t)
 408
 409/-! ## Global Consistency: Non-Locality of the Update -/
 410
 411/-- **Structure (Localized Update)**: An update that modifies only one entry,
 412    holding all others fixed. -/
 413structure LocalUpdate {N : ℕ} (c c' : Configuration N) where
 414  changed_index : Fin N
 415  others_fixed : ∀ i, i ≠ changed_index → c'.entries i = c.entries i
 416
 417/-- **Theorem (Update Is Global)**:
 418    The variational successor generally cannot be achieved by a local update.
 419
 420    Specifically: for N ≥ 2, there exist configurations where the
 421    variational successor modifies more than one entry.
 422
 423    This makes the update rule fundamentally NON-LOCAL — the optimal
 424    evolution of each entry depends on the state of all other entries
 425    through the shared conservation constraint. -/
 426theorem update_is_global :
 427    ∃ (N : ℕ) (hN : 0 < N) (c next : Configuration N),
 428      IsVariationalSuccessor c next ∧
 429      ¬∃ lu : LocalUpdate c next, True := by
 430  use 2, (by norm_num : 0 < 2)
 431  -- Consider c with entries [2, 1/2] (log-charge = 0).
 432  -- The variational successor is [1, 1] (also log-charge = 0).
 433  -- This changes BOTH entries, so no local update suffices.