FiniteFourier.lean

1 import QuantumArithmeticBridge
2 
3 set_option autoImplicit false
4 set_option maxRecDepth 100000
5 set_option maxHeartbeats 8000000
6 
7 namespace Komorebi.QuantumArithmetic
8 
9 abbrev Index := Fin 12
10 abbrev KVector := Index → Cyclo12
11 abbrev KMatrix := Index → Index → Cyclo12
12 
13 def kSum (f : Index → Cyclo12) : Cyclo12 := cSum (List.ofFn f)
14 
15 def kIdentity : KMatrix := fun i j => if i = j then cOne else cZero
16 
17 def kAdjoint (A : KMatrix) : KMatrix := fun i j => cConj (A j i)
18 
19 def kMatMul (A B : KMatrix) : KMatrix := fun i j =>
20   kSum (fun k => cMul (A i k) (B k j))
21 
22 def kMatVec (A : KMatrix) (v : KVector) : KVector := fun i =>
23   kSum (fun j => cMul (A i j) (v j))
24 
25 /-- sqrt(3)/6 = 1/sqrt(12). Its interpretation is proved separately. -/
26 def fourierScale : Cyclo12 := ⟨0, (1/6 : ℚ), 0, 0⟩
27 
28 /-- sqrt(3)/12 = 1/sqrt(48). -/
29 def stateScale : Cyclo12 := ⟨0, (1/12 : ℚ), 0, 0⟩
30 
31 def rootPower (n : Nat) : Cyclo12 := cPow zeta12 (n % 12)
32 
33 def exactFourier : KMatrix := fun i j =>
34   cMul fourierScale (rootPower (i.val * j.val))
35 
36 def exactSelector : KMatrix := fun i j =>
37   if i = j ∧ Nat.gcd i.val 12 = 1 then cOne else cZero
38 
39 def exactProjector : KMatrix := fun i j =>
40   cRat ((ramanujan12.getD ((i.val + 12 - j.val) % 12) 0) / 12)
41 
42 def exactUnitState : KVector := fun i =>
43   if Nat.gcd i.val 12 = 1 then cRat (1/2) else cZero
44 
45 def exactPsi : KVector := fun i =>
46   cMul stateScale (cRat (ramanujan12.getD i.val 0))
47 
48 def exactChi : KVector := fun i =>
49   cMul stateScale (cRat (absRamanujan12.getD i.val 0))
50 
51 def kNormSq (z : Cyclo12) : Cyclo12 := cMul (cConj z) z
52 
53 def kMass (v : KVector) : Cyclo12 := kSum (fun i => kNormSq (v i))
54 
55 def kCoprimeMass (v : KVector) : Cyclo12 :=
56   kSum (fun i => if Nat.gcd i.val 12 = 1 then kNormSq (v i) else cZero)
57 
58 /-- The stored arithmetic selector is exactly the coprimality predicate. -/
59 theorem coprime_residues_exact :
60     (List.range 12).filter (fun a => Nat.gcd a 12 == 1) = unitResidues12 := by
61   decide +kernel
62 
63 theorem root_exact_order :
64     ∀ n : Fin 12, 0 < n.val → cPow zeta12 n.val ≠ cOne := by
65   decide +kernel
66 
67 theorem normalized_fourier_left :
68     ∀ i j, kMatMul (kAdjoint exactFourier) exactFourier i j = kIdentity i j := by
69   decide +kernel
70 
71 theorem normalized_fourier_right :
72     ∀ i j, kMatMul exactFourier (kAdjoint exactFourier) i j = kIdentity i j := by
73   decide +kernel
74 
75 def selectedKernel : KMatrix := fun i j =>
76   kSum (fun k => if Nat.gcd k.val 12 = 1 then
77     cMul (exactFourier i k) (cConj (exactFourier j k)) else cZero)
78 
79 theorem exact_projector_transport :
80     ∀ i j, selectedKernel i j = exactProjector i j := by
81   decide +kernel
82 
83 theorem exact_projector_matches_rational_table :
84     ∀ i j, exactProjector i j = cRat ((projector12.getD i.val []).getD j.val 0) := by
85   decide +kernel
86 
87 theorem exact_state_preparation :
88     ∀ i, kMatVec exactFourier exactUnitState i = exactPsi i := by
89   decide +kernel
90 
91 theorem exact_state_recovery :
92     ∀ i, kMatVec (kAdjoint exactFourier) exactPsi i = exactUnitState i := by
93   decide +kernel
94 
95 theorem exact_unit_normalized : kMass exactUnitState = cOne := by
96   decide +kernel
97 
98 theorem exact_psi_normalized : kMass exactPsi = cOne := by
99   decide +kernel
100 
101 theorem exact_chi_normalized : kMass exactChi = cOne := by
102   decide +kernel
103 
104 theorem exact_same_initial_probabilities :
105     ∀ i, kNormSq (exactPsi i) = kNormSq (exactChi i) := by
106   decide +kernel
107 
108 theorem exact_orthogonal_states :
109     kSum (fun i => cMul (cConj (exactPsi i)) (exactChi i)) = cZero := by
110   decide +kernel
111 
112 theorem exact_coprime_mass_psi :
113     kCoprimeMass (kMatVec (kAdjoint exactFourier) exactPsi) = cOne := by
114   decide +kernel
115 
116 theorem exact_coprime_mass_chi :
117     kCoprimeMass (kMatVec (kAdjoint exactFourier) exactChi) = cZero := by
118   decide +kernel
119 
120 theorem exact_projector_fixes_psi :
121     ∀ i, kMatVec exactProjector exactPsi i = exactPsi i := by
122   decide +kernel
123 
124 theorem exact_projector_kills_chi :
125     ∀ i, kMatVec exactProjector exactChi i = cZero := by
126   decide +kernel
127 
128 end Komorebi.QuantumArithmetic

Back to source controls