noether_not_necessarily_quantized

formal source

 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. -/
 185theorem noether_not_necessarily_quantized :
 186    ∃ (N : ℕ) (Q : NoetherCharge N) (c : Configuration N),
 187      ¬∃ n : ℤ, Q.value c = (n : ℝ) := by
 188  use 1, logChargeAsNoether 1
 189  let c : Configuration 1 := {
 190    entries := fun _ => 2
 191    entries_pos := fun _ => by norm_num
 192  }
 193  use c
 194  intro ⟨n, hn⟩
 195  simp only [logChargeAsNoether, log_charge, Fin.sum_univ_one] at hn
 196  have h_pos : 0 < Real.log 2 := Real.log_pos (by norm_num : (1 : ℝ) < 2)
 197  have h_lt : Real.log 2 < 1 := by
 198    have h2_lt_e : (2 : ℝ) < Real.exp 1 := by
 199      exact lt_trans (by norm_num) Real.exp_one_gt_d9
 200    calc Real.log 2 < Real.log (Real.exp 1) :=
 201          Real.log_lt_log (by norm_num) h2_lt_e
 202      _ = 1 := Real.log_exp 1
 203  have h1 : (0 : ℝ) < n := by linarith
 204  have h2 : (n : ℝ) < 1 := by linarith
 205  have h3 : (0 : ℤ) < n := Int.cast_pos.mp h1
 206  have h4 : n < (1 : ℤ) := by exact_mod_cast h2
 207  omega
 208
 209/-! ## Part 6: Charge Algebra -/
 210
 211/-- Sum of two topological charges. -/
 212def addCharges {N : ℕ} (Q₁ Q₂ : TopologicalCharge N) : TopologicalCharge N where
 213  value := fun c => Q₁.value c + Q₂.value c
 214  conserved := fun c next h => by rw [Q₁.conserved c next h, Q₂.conserved c next h]
 215