 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.
 434  let c : Configuration 2 := {
 435    entries := fun i => if i.val = 0 then 2 else 1/2
 436    entries_pos := fun i => by
 437      fin_cases i <;> norm_num
 438  }
 439  let next : Configuration 2 := {
 440    entries := fun _ => 1
 441    entries_pos := fun _ => by norm_num
 442  }
 443  use c, next

papers checked against this theorem

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