topological_charge_quantized

formal source

  68
  69/-- **THEOREM (Quantization Is Automatic)**:
  70    Every topological charge takes integer values. -/
  71theorem topological_charge_quantized {N : ℕ} (Q : TopologicalCharge N)
  72    (c : Configuration N) : ∃ n : ℤ, Q.value c = n :=
  73  ⟨Q.value c, rfl⟩
  74
  75/-- **THEOREM (Exact Conservation Along Trajectories)** -/
  76theorem topological_charge_trajectory_conserved {N : ℕ} (Q : TopologicalCharge N)
  77    (traj : Trajectory N) (h : IsVariationalTrajectory traj) :
  78    ∀ t, Q.value (traj t) = Q.value (traj 0) := by
  79  intro t
  80  induction t with
  81  | zero => rfl
  82  | succ n ih => rw [← ih]; exact Q.conserved (traj n) (traj (n + 1)) (h n)
  83
  84/-- **THEOREM (Charge Is Time-Independent)** -/
  85theorem charge_at_any_tick {N : ℕ} (Q : TopologicalCharge N)
  86    (traj : Trajectory N) (h : IsVariationalTrajectory traj)
  87    (t₁ t₂ : ℕ) : Q.value (traj t₁) = Q.value (traj t₂) := by
  88  rw [topological_charge_trajectory_conserved Q traj h t₁,
  89      topological_charge_trajectory_conserved Q traj h t₂]
  90
  91/-! ## Part 2: Trivial Charges -/
  92
  93/-- The trivial topological charge: always zero. -/
  94def zeroCharge (N : ℕ) : TopologicalCharge N where
  95  value := fun _ => 0
  96  conserved := fun _ _ _ => rfl
  97
  98/-- A constant topological charge. -/
  99def constCharge (N : ℕ) (n : ℤ) : TopologicalCharge N where
 100  value := fun _ => n
 101  conserved := fun _ _ _ => rfl