Foundation Variational Dynamics Variational Dynamics Deterministic

/-- **Theorem (Deterministic Evolution)**:
    If two trajectories start from the same initial state and both
    follow the variational dynamics, they are identical.

    This is the equation-of-motion analogue of Laplacian determinism:
    initial conditions + update rule = unique future. -/
theorem variational_dynamics_deterministic {N : ℕ} (hN : 0 < N)
    (traj₁ traj₂ : Trajectory N)
    (h₁ : IsVariationalTrajectory traj₁)
    (h₂ : IsVariationalTrajectory traj₂)
    (h_init : (traj₁ 0).entries = (traj₂ 0).entries) :
    ∀ t, (traj₁ t).entries = (traj₂ t).entries := by
  intro t
  induction t with
  | zero => exact h_init
  | succ n ih =>
    have h1n := h₁ n
    have h2n := h₂ n
    -- Both traj₁(n+1) and traj₂(n+1) are variational successors of their
    -- respective states at time n. Since those states have the same entries
    -- (by induction), the feasible sets are the same.
    -- Uniqueness of the variational step gives the result.
    have h_same_charge : log_charge (traj₁ n) = log_charge (traj₂ n) := by
      unfold log_charge
      congr 1
      funext i
      rw [ih]
    -- Construct the compatibility: traj₂(n+1) is also a variational successor
    -- of traj₁(n) (since feasible sets match).
    have h2n_compat : IsVariationalSuccessor (traj₁ n) (traj₂ (n + 1)) := by
      constructor
      · show log_charge (traj₂ (n + 1)) = log_charge (traj₁ n)
        have := h2n.1
        exact this.trans h_same_charge.symm
      · intro c' hc'
        have hc'_feas2 : c' ∈ Feasible (traj₂ n) := by
          show log_charge c' = log_charge (traj₂ n)
          exact hc'.trans h_same_charge
        exact h2n.2 c' hc'_feas2
    exact variational_step_unique hN (traj₁ n) (traj₁ (n + 1)) (traj₂ (n + 1)) h1n h2n_compat

/-- **Theorem (Variational Step Existence)**:
    A total-defect minimizer always exists in the feasible set.

    The proof constructs the minimizer explicitly: it is the configuration
    where every entry equals exp(log_charge(c) / N), distributing the
    conserved charge equally. This is the AM-GM-optimal configuration. -/
theorem variational_step_exists {N : ℕ} (hN : 0 < N)
    (c : Configuration N) :
    ∃ next : Configuration N, IsVariationalSuccessor c next := by
  let μ := log_charge c / N
  use (constant_config μ : Configuration N)
  constructor
  · show log_charge (constant_config μ : Configuration N) = log_charge c
    rw [constant_config_log_charge]
    unfold μ
    exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN))
  · intro c' _hc'
    rw [constant_config_total_defect]
    have hbound := total_defect_lower_bound hN c'
    rw [_hc'] at hbound
    unfold μ
    exact hbound

/-- **Theorem (Variational Step Uniqueness)**:
    If two configurations both minimize total defect over the feasible set,
    they are identical.

    Proof uses strict convexity of J: if c₁ ≠ c₂ both minimize total J-cost,
    their midpoint (adjusted to satisfy the constraint) would have strictly
    lower cost, contradicting minimality.

    This is the core determinism result: the next state is UNIQUE. -/
theorem variational_step_unique {N : ℕ} (hN : 0 < N)
    (c : Configuration N)
    (next₁ next₂ : Configuration N)
    (h₁ : IsVariationalSuccessor c next₁)
    (h₂ : IsVariationalSuccessor c next₂) :
    next₁.entries = next₂.entries := by
  have h_uniform : IsVariationalSuccessor c (constant_config (log_charge c / N) : Configuration N) := by
    constructor
    · show log_charge (constant_config (log_charge c / N) : Configuration N) = log_charge c
      rw [constant_config_log_charge]
      exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN))
    · intro c' hc'
      rw [constant_config_total_defect]
      have hbound := total_defect_lower_bound hN c'
      rw [hc'] at hbound
      exact hbound
  have h1_eq_min : total_defect next₁ = (N : ℝ) * Jlog (log_charge c / N) := by
    have h1le := h₁.2 (constant_config (log_charge c / N) : Configuration N) h_uniform.1
    have h1ge := h_uniform.2 next₁ h₁.1
    rw [constant_config_total_defect] at h1le h1ge
    exact le_antisymm h1le h1ge
  have h2_eq_min : total_defect next₂ = (N : ℝ) * Jlog (log_charge c / N) := by
    have h2le := h₂.2 (constant_config (log_charge c / N) : Configuration N) h_uniform.1
    have h2ge := h_uniform.2 next₂ h₂.1
    rw [constant_config_total_defect] at h2le h2ge
    exact le_antisymm h2le h2ge
  have h1_const :
      next₁.entries = (constant_config (log_charge next₁ / N) : Configuration N).entries := by
    apply eq_constant_config_of_defect_eq hN next₁
    rw [← h₁.1] at h1_eq_min
    exact h1_eq_min
  have h2_const :
      next₂.entries = (constant_config (log_charge next₂ / N) : Configuration N).entries := by
    apply eq_constant_config_of_defect_eq hN next₂
    rw [← h₂.1] at h2_eq_min
    exact h2_eq_min
  have hcharge1 : log_charge next₁ = log_charge c := h₁.1
  have hcharge2 : log_charge next₂ = log_charge c := h₂.1
  calc
    next₁.entries = (constant_config (log_charge next₁ / N) : Configuration N).entries := h1_const
    _ = (constant_config (log_charge c / N) : Configuration N).entries := by rw [hcharge1]
    _ = (constant_config (log_charge next₂ / N) : Configuration N).entries := by rw [hcharge2]
    _ = next₂.entries := h2_const.symm

/-- **Theorem (Update Is Global)**:
    The variational successor generally cannot be achieved by a local update.

    Specifically: for N ≥ 2, there exist configurations where the
    variational successor modifies more than one entry.

    This makes the update rule fundamentally NON-LOCAL — the optimal
    evolution of each entry depends on the state of all other entries
    through the shared conservation constraint. -/
theorem update_is_global :
    ∃ (N : ℕ) (hN : 0 < N) (c next : Configuration N),
      IsVariationalSuccessor c next ∧
      ¬∃ lu : LocalUpdate c next, True := by
  use 2, (by norm_num : 0 < 2)
  -- Consider c with entries [2, 1/2] (log-charge = 0).
  -- The variational successor is [1, 1] (also log-charge = 0).
  -- This changes BOTH entries, so no local update suffices.
  let c : Configuration 2 := {
    entries := fun i => if i.val = 0 then 2 else 1/2
    entries_pos := fun i => by
      fin_cases i <;> norm_num
  }
  let next : Configuration 2 := {
    entries := fun _ => 1
    entries_pos := fun _ => by norm_num
  }
  use c, next
  constructor
  · constructor
    · -- Feasibility: log_charge [1,1] = log(1) + log(1) = 0
      -- log_charge [2, 1/2] = log(2) + log(1/2) = log(2) - log(2) = 0
      show log_charge next = log_charge c
      unfold log_charge
      simp [Fin.sum_univ_two, next, c]
    · -- Minimality: [1,1] has zero total defect, which is minimal
      intro c' _
      unfold total_defect
      have h_next : ∀ i : Fin 2, next.entries i = 1 := fun _ => rfl
      simp only [h_next, defect_at_one, Finset.sum_const_zero]
      exact Finset.sum_nonneg (fun i _ => defect_nonneg (c'.entries_pos i))
  · -- No local update: both entries change (2 → 1 and 1/2 → 1)
    intro ⟨lu, _⟩
    have h0 : next.entries ⟨0, by norm_num⟩ ≠ c.entries ⟨0, by norm_num⟩ := by
      show (1 : ℝ) ≠ 2
      norm_num
    have h1 : next.entries ⟨1, by norm_num⟩ ≠ c.entries ⟨1, by norm_num⟩ := by
      show (1 : ℝ) ≠ 1 / 2
      norm_num
    cases lu with
    | mk idx hfixed =>
      fin_cases idx
      · have := hfixed ⟨1, by norm_num⟩ (by decide)
        exact h1 this
      · have := hfixed ⟨0, by norm_num⟩ (by decide)
        exact h0 this

/-- **Theorem (Variational Step Reduces Defect)**:
    The total defect of the successor is at most the total defect
    of the current state.

    This follows immediately: the current state is feasible for itself,
    and the successor minimizes over the feasible set, so the successor's
    cost is at most the current state's cost. -/
theorem variational_step_reduces_defect {N : ℕ}
    (c next : Configuration N)
    (h : IsVariationalSuccessor c next) :
    total_defect next ≤ total_defect c :=
  h.2 c (self_feasible c)

/-- **Theorem**: The unity configuration is an equilibrium when log-charge = 0. -/
theorem unity_is_equilibrium {N : ℕ} (hN : 0 < N) :
    IsEquilibrium (unity_config N hN) := by
  constructor
  · exact self_feasible _
  · intro c' hc'
    rw [unity_defect_zero hN]
    exact total_defect_nonneg c'