QuantumArithmeticBridge.lean

1 import Mathlib.Tactic.NormNum
2 
3 /-!
4 # Komorebi quantum arithmetic bridge
5 
6 Exact finite formalization of the q = 12 example used in
7 "Mathematics Between Minds".
8 
9 The file has two layers.
10 
11 1. A rational projector layer proving exact filter, idempotence, symmetry,
12    energy, and normalization claims.
13 2. An exact cyclotomic arithmetic layer for the 12th root of unity.  The
14    cyclotomic values are represented in the basis 1, sqrt(3), i, i*sqrt(3)
15    over Q, so no floating point approximation enters the Fourier claims.
16 
17 This file is designed for a recent Mathlib environment.
18 -/
19 
20 set_option autoImplicit false
21 set_option maxRecDepth 100000
22 set_option maxHeartbeats 8000000
23 
24 namespace Komorebi.QuantumArithmetic
25 
26 /-! ## 1. Exact rational signal and projector -/
27 
28 abbrev QVector := List ℚ
29 abbrev QMatrix := List (List ℚ)
30 
31 def dot (x y : QVector) : ℚ :=
32   (List.zipWith (fun a b => a * b) x y).sum
33 
34 def transposeN (n : Nat) (M : QMatrix) : QMatrix :=
35   (List.range n).map (fun j => M.map (fun row => row.getD j 0))
36 
37 def matMulN (n : Nat) (A B : QMatrix) : QMatrix :=
38   A.map (fun row => (transposeN n B).map (fun col => dot row col))
39 
40 def matVec (M : QMatrix) (v : QVector) : QVector :=
41   M.map (fun row => dot row v)
42 
43 def vecAdd (x y : QVector) : QVector :=
44   List.zipWith (fun a b => a + b) x y
45 
46 def vecSub (x y : QVector) : QVector :=
47   List.zipWith (fun a b => a - b) x y
48 
49 def sqEnergy (x : QVector) : ℚ := dot x x
50 
51 /-- Ramanujan sum c_12(n), n = 0,...,11. -/
52 def ramanujan12 : QVector :=
53   [4, 0, 2, 0, -2, 0, -4, 0, -2, 0, 2, 0]
54 
55 /-- A deliberately off-band perturbation: 3 cos(pi n/2) + 2. -/
56 def noise12 : QVector :=
57   [5, 2, -1, 2, 5, 2, -1, 2, 5, 2, -1, 2]
58 
59 /-- Signal used in the essay's filter demonstration. -/
60 def testSignal12 : QVector :=
61   [9, 2, 1, 2, 3, 2, -5, 2, 3, 2, 1, 2]
62 
63 /-- P_nm = c_12(n-m)/12, written exactly over Q. -/
64 def projector12 : QMatrix :=
65 [
66   [(1 / 3 : ℚ), 0, (1 / 6 : ℚ), 0, (-1 / 6 : ℚ), 0, (-1 / 3 : ℚ), 0, (-1 / 6 : ℚ), 0, (1 / 6 : ℚ), 0],
67   [0, (1 / 3 : ℚ), 0, (1 / 6 : ℚ), 0, (-1 / 6 : ℚ), 0, (-1 / 3 : ℚ), 0, (-1 / 6 : ℚ), 0, (1 / 6 : ℚ)],
68   [(1 / 6 : ℚ), 0, (1 / 3 : ℚ), 0, (1 / 6 : ℚ), 0, (-1 / 6 : ℚ), 0, (-1 / 3 : ℚ), 0, (-1 / 6 : ℚ), 0],
69   [0, (1 / 6 : ℚ), 0, (1 / 3 : ℚ), 0, (1 / 6 : ℚ), 0, (-1 / 6 : ℚ), 0, (-1 / 3 : ℚ), 0, (-1 / 6 : ℚ)],
70   [(-1 / 6 : ℚ), 0, (1 / 6 : ℚ), 0, (1 / 3 : ℚ), 0, (1 / 6 : ℚ), 0, (-1 / 6 : ℚ), 0, (-1 / 3 : ℚ), 0],
71   [0, (-1 / 6 : ℚ), 0, (1 / 6 : ℚ), 0, (1 / 3 : ℚ), 0, (1 / 6 : ℚ), 0, (-1 / 6 : ℚ), 0, (-1 / 3 : ℚ)],
72   [(-1 / 3 : ℚ), 0, (-1 / 6 : ℚ), 0, (1 / 6 : ℚ), 0, (1 / 3 : ℚ), 0, (1 / 6 : ℚ), 0, (-1 / 6 : ℚ), 0],
73   [0, (-1 / 3 : ℚ), 0, (-1 / 6 : ℚ), 0, (1 / 6 : ℚ), 0, (1 / 3 : ℚ), 0, (1 / 6 : ℚ), 0, (-1 / 6 : ℚ)],
74   [(-1 / 6 : ℚ), 0, (-1 / 3 : ℚ), 0, (-1 / 6 : ℚ), 0, (1 / 6 : ℚ), 0, (1 / 3 : ℚ), 0, (1 / 6 : ℚ), 0],
75   [0, (-1 / 6 : ℚ), 0, (-1 / 3 : ℚ), 0, (-1 / 6 : ℚ), 0, (1 / 6 : ℚ), 0, (1 / 3 : ℚ), 0, (1 / 6 : ℚ)],
76   [(1 / 6 : ℚ), 0, (-1 / 6 : ℚ), 0, (-1 / 3 : ℚ), 0, (-1 / 6 : ℚ), 0, (1 / 6 : ℚ), 0, (1 / 3 : ℚ), 0],
77   [0, (1 / 6 : ℚ), 0, (-1 / 6 : ℚ), 0, (-1 / 3 : ℚ), 0, (-1 / 6 : ℚ), 0, (1 / 6 : ℚ), 0, (1 / 3 : ℚ)]
78 ]
79 
80 theorem ramanujan12_length : ramanujan12.length = 12 := by decide +kernel
81 
82 theorem projector12_shape :
83     projector12.length = 12 ∧
84     projector12.map List.length = List.replicate 12 12 := by
85   decide +kernel
86 
87 /-- The cyclic Ramanujan kernel is symmetric. -/
88 theorem projector12_symmetric : transposeN 12 projector12 = projector12 := by
89   decide +kernel
90 
91 /-- Exact finite projector identity P^2 = P. -/
92 theorem projector12_idempotent :
93     matMulN 12 projector12 projector12 = projector12 := by
94   decide +kernel
95 
96 /-- The arithmetic signal lies in the selected subspace. -/
97 theorem projector12_fixes_ramanujan :
98     matVec projector12 ramanujan12 = ramanujan12 := by
99   decide +kernel
100 
101 /-- The chosen constant-plus-frequency-3 perturbation lies in the complementary subspace. -/
102 theorem projector12_kills_noise :
103     matVec projector12 noise12 = List.replicate 12 0 := by
104   decide +kernel
105 
106 /-- Therefore the exact filter recovers the arithmetic component. -/
107 theorem projector12_recovers_test_signal :
108     matVec projector12 testSignal12 = ramanujan12 := by
109   decide +kernel
110 
111 /-- The arithmetic amplitude vector has squared norm 48. -/
112 theorem ramanujan12_energy : sqEnergy ramanujan12 = 48 := by
113   decide +kernel
114 
115 /-- The perturbation has squared norm 102. -/
116 theorem noise12_energy : sqEnergy noise12 = 102 := by
117   decide +kernel
118 
119 /-- The full signal has squared norm 150. -/
120 theorem testSignal12_energy : sqEnergy testSignal12 = 150 := by
121   decide +kernel
122 
123 /-- Exact orthogonal energy decomposition 150 = 48 + 102. -/
124 theorem energy_decomposition :
125     sqEnergy testSignal12 = sqEnergy ramanujan12 + sqEnergy noise12 := by
126   decide +kernel
127 
128 /-! ## 2. Exact cyclotomic arithmetic for zeta_12 -/
129 
130 /--
131 An exact coordinate model for Q(sqrt(3), i).  The tuple (a,b,c,d) denotes
132   a + b*sqrt(3) + i*(c + d*sqrt(3)).
133 Only the concrete arithmetic needed for the q=12 certificate is used below;
134 we do not install a global field instance.
135 -/
136 structure Cyclo12 where
137   a : ℚ
138   b : ℚ
139   c : ℚ
140   d : ℚ
141   deriving DecidableEq, Repr
142 
143 def cZero : Cyclo12 := ⟨0, 0, 0, 0⟩
144 def cOne  : Cyclo12 := ⟨1, 0, 0, 0⟩
145 def cRat (r : ℚ) : Cyclo12 := ⟨r, 0, 0, 0⟩
146 
147 def cAdd (x y : Cyclo12) : Cyclo12 :=
148   ⟨x.a + y.a, x.b + y.b, x.c + y.c, x.d + y.d⟩
149 
150 def cNeg (x : Cyclo12) : Cyclo12 :=
151   ⟨-x.a, -x.b, -x.c, -x.d⟩
152 
153 def cSub (x y : Cyclo12) : Cyclo12 := cAdd x (cNeg y)
154 
155 /-- Multiplication in Q(sqrt(3), i). -/
156 def cMul (x y : Cyclo12) : Cyclo12 :=
157   ⟨x.a*y.a + 3*x.b*y.b - x.c*y.c - 3*x.d*y.d,
158    x.a*y.b + x.b*y.a - x.c*y.d - x.d*y.c,
159    x.a*y.c + 3*x.b*y.d + x.c*y.a + 3*x.d*y.b,
160    x.a*y.d + x.b*y.c + x.c*y.b + x.d*y.a⟩
161 
162 def cConj (x : Cyclo12) : Cyclo12 := ⟨x.a, x.b, -x.c, -x.d⟩
163 
164 def cPow (x : Cyclo12) : Nat → Cyclo12
165   | 0 => cOne
166   | n + 1 => cMul (cPow x n) x
167 
168 def cSum : List Cyclo12 → Cyclo12
169   | [] => cZero
170   | x :: xs => cAdd x (cSum xs)
171 
172 /-- zeta = exp(2*pi*i/12) = sqrt(3)/2 + i/2. -/
173 def zeta12 : Cyclo12 := ⟨0, (1/2 : ℚ), (1/2 : ℚ), 0⟩
174 
175 def zeta12Inv : Cyclo12 := cConj zeta12
176 
177 theorem zeta12_order_certificate : cPow zeta12 12 = cOne := by
178   decide +kernel
179 
180 theorem zeta12_inverse_certificate : cMul zeta12 zeta12Inv = cOne := by
181   decide +kernel
182 
183 /-- The four coprime residues modulo 12. -/
184 def unitResidues12 : List Nat := [1, 5, 7, 11]
185 
186 def ramanujanC12 (n : Nat) : Cyclo12 :=
187   cSum (unitResidues12.map (fun a => cPow zeta12 (a*n)))
188 
189 /-- Exact Ramanujan-sum table obtained from the four primitive phases. -/
190 theorem ramanujanC12_table :
191     (List.range 12).map ramanujanC12 =
192       [cRat 4, cRat 0, cRat 2, cRat 0, cRat (-2), cRat 0,
193        cRat (-4), cRat 0, cRat (-2), cRat 0, cRat 2, cRat 0] := by
194   decide +kernel
195 
196 /-- Minus-sign DFT over one period, using zeta^(-k*n). -/
197 def dft12 (x : List Cyclo12) (k : Nat) : Cyclo12 :=
198   cSum ((List.range 12).map (fun n =>
199     cMul (x.getD n cZero) (cPow zeta12Inv (k*n))))
200 
201 def ramanujanCVector : List Cyclo12 :=
202   (List.range 12).map ramanujanC12
203 
204 /-- The DFT is supported exactly on 1,5,7,11, with value 12 there. -/
205 theorem ramanujan_dft_table :
206     (List.range 12).map (dft12 ramanujanCVector) =
207       [cRat 0, cRat 12, cRat 0, cRat 0, cRat 0, cRat 12,
208        cRat 0, cRat 12, cRat 0, cRat 0, cRat 0, cRat 12] := by
209   decide +kernel
210 
211 /-- Absolute-value version of the Ramanujan signal. -/
212 def absRamanujanCVector : List Cyclo12 :=
213   [cRat 4, cRat 0, cRat 2, cRat 0, cRat 2, cRat 0,
214    cRat 4, cRat 0, cRat 2, cRat 0, cRat 2, cRat 0]
215 
216 /-- Removing the signs destroys every coprime Fourier mode. -/
217 theorem abs_ramanujan_dft_table :
218     (List.range 12).map (dft12 absRamanujanCVector) =
219       [cRat 16, cRat 0, cRat 4, cRat 0, cRat 4, cRat 0,
220        cRat 16, cRat 0, cRat 4, cRat 0, cRat 4, cRat 0] := by
221   decide +kernel
222 
223 /-! ## 3. Quantum probability consequences -/
224 
225 /-- Squared amplitudes are unchanged by stripping the signs of c_12(n). -/
226 def absRamanujan12 : QVector :=
227   [4, 0, 2, 0, 2, 0, 4, 0, 2, 0, 2, 0]
228 
229 def sqEntries (x : QVector) : QVector := x.map (fun t => t*t)
230 
231 theorem same_computational_basis_probabilities :
232     sqEntries ramanujan12 = sqEntries absRamanujan12 := by
233   decide +kernel
234 
235 theorem abs_ramanujan12_energy : sqEnergy absRamanujan12 = 48 := by
236   decide +kernel
237 
238 /--
239 For |psi> = (1/sqrt(48)) sum_n c_12(n)|n>, the unitary inverse DFT contributes
240 an additional factor 1/sqrt(12).  A recovered Fourier coefficient 12 therefore
241 has probability 12^2/(48*12) = 1/4.
242 -/
243 theorem recovered_mode_probability :
244     ((12 : ℚ)^2) / (48 * 12) = 1/4 := by
245   norm_num
246 
247 /-- Four recovered coprime modes exhaust total probability. -/
248 theorem recovered_total_probability :
249     4 * (((12 : ℚ)^2) / (48 * 12)) = 1 := by
250   norm_num
251 
252 /-- The absolute-value state has zero probability on each of the four coprime modes. -/
253 theorem phase_stripping_coprime_probability :
254     4 * (((0 : ℚ)^2) / (48 * 12)) = 0 := by
255   norm_num
256 
257 /-- The publication's central finite bridge, bundled as one exact proposition. -/
258 theorem arithmetic_signal_quantum_bridge :
259     matMulN 12 projector12 projector12 = projector12 ∧
260     matVec projector12 testSignal12 = ramanujan12 ∧
261     (List.range 12).map (dft12 ramanujanCVector) =
262       [cRat 0, cRat 12, cRat 0, cRat 0, cRat 0, cRat 12,
263        cRat 0, cRat 12, cRat 0, cRat 0, cRat 0, cRat 12] ∧
264     sqEntries ramanujan12 = sqEntries absRamanujan12 := by
265   exact ⟨projector12_idempotent, projector12_recovers_test_signal,
266     ramanujan_dft_table, same_computational_basis_probabilities⟩
267 
268 end Komorebi.QuantumArithmetic

Back to source controls