theorem
proved
tactic proof
noether_not_necessarily_quantized
show as:
view Lean formalization →
formal statement (Lean)
185theorem noether_not_necessarily_quantized :
186 ∃ (N : ℕ) (Q : NoetherCharge N) (c : Configuration N),
187 ¬∃ n : ℤ, Q.value c = (n : ℝ) := by
proof body
Tactic-mode proof.
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. -/