IsVariationalTrajectory

formal source

 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
 374  | zero => exact h_init
 375  | succ n ih =>
 376    have h1n := h₁ n
 377    have h2n := h₂ n
 378    -- Both traj₁(n+1) and traj₂(n+1) are variational successors of their
 379    -- respective states at time n. Since those states have the same entries
 380    -- (by induction), the feasible sets are the same.
 381    -- Uniqueness of the variational step gives the result.
 382    have h_same_charge : log_charge (traj₁ n) = log_charge (traj₂ n) := by
 383      unfold log_charge
 384      congr 1
 385      funext i
 386      rw [ih]
 387    -- Construct the compatibility: traj₂(n+1) is also a variational successor