A.7 Finite indices and normalized Fourier certificates
On this page · Permalink · Source line 238
The finite layer uses Index := Fin 12. Its normalized Fourier scale is represented exactly as \(\sqrt3/6=1/\sqrt{12}\), and its state scale as \(\sqrt3/12=1/\sqrt{48}\). The use of a finite index type makes every row and column well defined without list-length side conditions.
Literal source. FiniteFourier.lean, physical lines 58–93.
/-- The stored arithmetic selector is exactly the coprimality predicate. -/
theorem coprime_residues_exact :
(List.range 12).filter (fun a => Nat.gcd a 12 == 1) = unitResidues12 := by
decide +kernel
theorem root_exact_order :
∀ n : Fin 12, 0 < n.val → cPow zeta12 n.val ≠ cOne := by
decide +kernel
theorem normalized_fourier_left :
∀ i j, kMatMul (kAdjoint exactFourier) exactFourier i j = kIdentity i j := by
decide +kernel
theorem normalized_fourier_right :
∀ i j, kMatMul exactFourier (kAdjoint exactFourier) i j = kIdentity i j := by
decide +kernel
def selectedKernel : KMatrix := fun i j =>
kSum (fun k => if Nat.gcd k.val 12 = 1 then
cMul (exactFourier i k) (cConj (exactFourier j k)) else cZero)
theorem exact_projector_transport :
∀ i j, selectedKernel i j = exactProjector i j := by
decide +kernel
theorem exact_projector_matches_rational_table :
∀ i j, exactProjector i j = cRat ((projector12.getD i.val []).getD j.val 0) := by
decide +kernel
theorem exact_state_preparation :
∀ i, kMatVec exactFourier exactUnitState i = exactPsi i := by
decide +kernel
theorem exact_state_recovery :
∀ i, kMatVec (kAdjoint exactFourier) exactPsi i = exactUnitState i := by
decide +kernelThe two Fourier identities above quantify over all \(12\times12\) entries. Kernel reduction proves these concrete universal statements over a finite type. The selected-kernel equality and state actions are also complete finite certificates, rather than floating-point matrix comparisons.