A.10 The exponential sign and square-root normalization
On this page · Permalink · Source line 440
The usual Fourier matrix is not left as an informal interpretation. The convention module proves that the coordinate root equals the positive exponential root, including the selected square-root branch.
Literal source. Conventions.lean, physical lines 10–24.
/-- The coordinate root is exactly the usual exponential twelfth root. -/
theorem root_is_exponential :
interpret zeta12 = Complex.exp (((Real.pi / 6 : ℝ) : ℂ) * Complex.I) := by
rw [Complex.exp_mul_I]
rw [← Complex.ofReal_cos, ← Complex.ofReal_sin, Real.cos_pi_div_six, Real.sin_pi_div_six]
apply Complex.ext <;> simp [interpret, zeta12]
ring
theorem root_power_twelve : interpret zeta12 ^ 12 = 1 := by
simpa using congrArg interpret zeta12_order_certificate
theorem rootPower_interpret (n : Nat) :
interpret (rootPower n) = interpret zeta12 ^ n := by
simp only [rootPower, interpret_pow]
exact (pow_eq_pow_mod n root_power_twelve).symmIts normalization lemmas prove \(\sqrt{12}=2\sqrt3\) and \(\sqrt{48}=4\sqrt3\), then identify the exact scales with their ordinary reciprocals. The matrix entry formula and state formula below are therefore literal equalities in \(\mathbb C\).
Literal source. Conventions.lean, physical lines 42–54.
theorem fourierScale_interpret :
interpret fourierScale = ((1 / Real.sqrt 12 : ℝ) : ℂ) := by
apply Complex.ext <;> simp [interpret, fourierScale, sqrt_twelve]
have h : Real.sqrt 3 ≠ 0 := by positivity
field_simp
nlinarith [Real.sq_sqrt (show (0 : ℝ) ≤ 3 by norm_num)]
theorem stateScale_interpret :
interpret stateScale = ((1 / Real.sqrt 48 : ℝ) : ℂ) := by
apply Complex.ext <;> simp [interpret, stateScale, sqrt_fortyeight]
have h : Real.sqrt 3 ≠ 0 := by positivity
field_simp
nlinarith [Real.sq_sqrt (show (0 : ℝ) ≤ 3 by norm_num)]Literal source. Conventions.lean, physical lines 56–65.
/-- The matrix checked in the certificate is the standard positive sign Fourier matrix. -/
theorem fourier_entry_formula (i j : Index) :
F i j = ((1 / Real.sqrt 12 : ℝ) : ℂ) *
Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (i.val : ℂ) * (j.val : ℂ) / 12) := by
simp only [F, complexMatrix, exactFourier, interpret_mul, fourierScale_interpret,
rootPower_interpret, root_is_exponential]
rw [← Complex.exp_nat_mul]
congr 2
push_cast
ringLiteral source. Conventions.lean, physical lines 67–82.
theorem psi_entry_formula (i : Index) :
psi i = ((1 / Real.sqrt 48 : ℝ) : ℂ) * (ramanujan12.getD i.val 0 : ℂ) := by
simp [psi, complexVector, exactPsi, stateScale_interpret]
theorem chi_entry_formula (i : Index) :
chi i = ((1 / Real.sqrt 48 : ℝ) : ℂ) * (absRamanujan12.getD i.val 0 : ℂ) := by
simp [chi, complexVector, exactChi, stateScale_interpret]
theorem unitState_entry_formula (i : Index) :
unitState i = if Nat.gcd i.val 12 = 1 then (1/2 : ℂ) else 0 := by
by_cases h : Nat.gcd i.val 12 = 1 <;>
simp [unitState, complexVector, exactUnitState, h]
theorem projector_entry_formula (i j : Index) :
P i j = (ramanujan12.getD ((i.val + 12 - j.val) % 12) 0 : ℂ) / 12 := by
simp [P, complexMatrix, exactProjector]The convention is positive sign for \(F\) and negative sign for \(F^*\). The earlier unnormalized dft12 uses the negative sign. The normalization and adjoint are the precise link between those notations.