theorem
proved
tactic proof
variational_dynamics_deterministic
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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)
397 exact hc'.trans h_same_charge
398 exact h2n.2 c' hc'_feas2
399 exact variational_step_unique hN (traj₁ n) (traj₁ (n + 1)) (traj₂ (n + 1)) h1n h2n_compat
400
401/-- **Theorem (Monotone Defect Along Trajectories)**:
402 Total defect is non-increasing along any variational trajectory. -/