variational_dynamics_deterministic

formal source

 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
 388    -- of traj₁(n) (since feasible sets match).
 389    have h2n_compat : IsVariationalSuccessor (traj₁ n) (traj₂ (n + 1)) := by
 390      constructor
 391      · show log_charge (traj₂ (n + 1)) = log_charge (traj₁ n)
 392        have := h2n.1
 393        exact this.trans h_same_charge.symm
 394      · intro c' hc'
 395        have hc'_feas2 : c' ∈ Feasible (traj₂ n) := by
 396          show log_charge c' = log_charge (traj₂ n)