TopologicalCharge

formal source

  61
  62    Integer-valuedness is the formal content of "charge quantization."
  63    It is structural (the codomain is ℤ), not imposed. -/
  64structure TopologicalCharge (N : ℕ) where
  65  value : Configuration N → ℤ
  66  conserved : ∀ (c next : Configuration N),
  67    IsVariationalSuccessor c next → value next = value c
  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