Foundation Variational Dynamics

/-- **Definition (Update Rule)**: The next state is the configuration
    that minimizes total defect subject to conservation of log-charge.

    This is the "equation of motion" for the ledger. -/
def IsVariationalSuccessor {N : ℕ} (current next : Configuration N) : Prop :=
  next ∈ Feasible current ∧
  ∀ c' ∈ Feasible current, total_defect next ≤ total_defect c'

/-- The feasible set: configurations reachable in one tick.
    A configuration c' is feasible from c if:
    1. All entries remain positive
    2. Total log-charge is conserved -/
def Feasible {N : ℕ} (c : Configuration N) : Set (Configuration N) :=
  { c' : Configuration N | log_charge c' = log_charge c }

/-- **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 (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 (Monotone Defect Along Trajectories)**:
    Total defect is non-increasing along any variational trajectory. -/
theorem trajectory_defect_monotone {N : ℕ}
    (traj : Trajectory N)
    (h : IsVariationalTrajectory traj) :
    ∀ t, total_defect (traj (t + 1)) ≤ total_defect (traj t) :=
  fun t => variational_step_reduces_defect (traj t) (traj (t + 1)) (h t)

/-- **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 Implies Recognition Step)**:
    Every variational step produces a valid `RecognitionStep` in the
    `TimeEmergence` framework.

    The variational dynamics generates the defect-reducing steps that
    TimeEmergence postulated but never constructed. -/
theorem variational_implies_recognition_step {N : ℕ}
    (c next : Configuration N)
    (h : IsVariationalSuccessor c next)
    (tick_val : ℕ) :
    ∃ step : RecognitionStep,
      step.input.defect = total_defect c ∧
      step.output.defect = total_defect next := by
  refine ⟨{
    input := {
      tick := ⟨tick_val⟩
      defect := total_defect c
      defect_nonneg := total_defect_nonneg c
    }
    output := {
      tick := ⟨tick_val + 1⟩
      defect := total_defect next
      defect_nonneg := total_defect_nonneg next
    }
    tick_advance := rfl
    defect_reduce := variational_step_reduces_defect c next h
  }, rfl, rfl⟩