charge_to_axis_surjective

formal source

 151theorem charge_to_axis_injective : Function.Injective charge_to_axis := by
 152  intro a b h; cases a <;> cases b <;> simp_all [charge_to_axis]
 153
 154theorem charge_to_axis_surjective : Function.Surjective charge_to_axis := by
 155  intro ⟨n, hn⟩; interval_cases n
 156  · exact ⟨.electric, rfl⟩
 157  · exact ⟨.baryon, rfl⟩
 158  · exact ⟨.lepton, rfl⟩
 159
 160theorem charge_to_axis_bijective : Function.Bijective charge_to_axis :=
 161  ⟨charge_to_axis_injective, charge_to_axis_surjective⟩
 162
 163/-! ## Part 5: Topological vs. Noether Conservation -/
 164
 165/-- A **Noether charge**: real-valued, conserved under dynamics. -/
 166structure NoetherCharge (N : ℕ) where
 167  value : Configuration N → ℝ
 168  conserved : ∀ (c next : Configuration N),
 169    IsVariationalSuccessor c next → value next = value c
 170
 171/-- Log-charge is a Noether charge (conserved, real-valued). -/
 172noncomputable def logChargeAsNoether (N : ℕ) : NoetherCharge N where
 173  value := log_charge
 174  conserved := fun _ _ h => h.1
 175
 176/-- Every topological charge induces a Noether charge by ℤ ↪ ℝ. -/
 177def topological_to_noether {N : ℕ} (Q : TopologicalCharge N) : NoetherCharge N where
 178  value := fun c => (Q.value c : ℝ)
 179  conserved := fun c next h => by simp [Q.conserved c next h]
 180
 181/-- **THEOREM (Noether Charges Need Not Be Quantized)**:
 182    There exist Noether charges that take non-integer values.
 183
 184    Proof: log(2) satisfies 0 < log(2) < 1, so it is not an integer. -/