HeisenbergPrime.lean

1 import PaperXI.SchrodingerOperator
2 import Mathlib.FieldTheory.Finite.Basic
3 
4 /-! The odd-prime specialization uses exactly the manuscript's exponential
5 additive character, with nontriviality and invertibility of two proved. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.HeisenbergPrime
9 
10 variable {p : ℕ} [Fact p.Prime]
11 
12 theorem two_ne_zero (hp : p ≠ 2) : (2 : ZMod p) ≠ 0 := by
13   intro h
14   have hd : p ∣ 2 := (ZMod.natCast_eq_zero_iff 2 p).mp h
15   exact hp ((Nat.prime_dvd_prime_iff_eq (Fact.out : p.Prime) Nat.prime_two).mp hd)
16 
17 theorem character_nontrivial : (ZMod.stdAddChar (N := p)) ≠ 1 := by
18   intro h
19   have he : ZMod.stdAddChar (1 : ZMod p) = ZMod.stdAddChar (0 : ZMod p) := by
20     rw [h]
21     rfl
22   exact one_ne_zero (ZMod.injective_stdAddChar he)
23 
24 theorem character_formula (j : ℤ) :
25     ZMod.stdAddChar (j : ZMod p) =
26       Complex.exp (2 * Real.pi * Complex.I * j / p) :=
27   ZMod.stdAddChar_coe j
28 
29 end PaperXI.HeisenbergPrime

Back to source controls