q_lean.tex
Quantum and Circuits
q_lean.tex
This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.
Read this chapter with formatted equations
1 \section{What this guide certifies}
2 The completed fixed example is a bridge between exact arithmetic and ordinary
3 complex linear algebra. It certifies a twelve-dimensional Fourier matrix, a
4 Ramanujan projector, two normalized states with the same initial probabilities,
5 and their opposite outcomes after a basis change. This guide maps those claims to
6 actual Lean declarations rather than treating numerical agreement as a proof.
7
8 The five-module formal package contains \textbf{96 named mathematical theorems}. Its current verification rebuilt the source, inspected the axiom dependencies of every named theorem, and replayed all five modules. Historical proof records remain separate from this fresh execution.
9
10 \begin{center}
11 \begin{tabular}{lr}
12 \toprule
13 Production module & Named theorems\\
14 \midrule
15 \texttt{QuantumArithmeticBridge} & 22\\
16 \texttt{FiniteFourier} & 17\\
17 \texttt{SemanticBridge} & 30\\
18 \texttt{Conventions} & 17\\
19 \texttt{Publication} & 10\\
20 \midrule
21 Total & 96\\
22 \bottomrule
23 \end{tabular}
24 \end{center}
25
26 These counts include supporting lemmas. They count named source declarations,
27 not new discoveries, compiler jobs, or declarations generated internally by Lean.
28 The namespace is \texttt{Komorebi.QuantumArithmetic} throughout.
29
30 \section{The typed mathematical target}
31 The complex matrices act on vectors indexed by \(\operatorname{Fin}(12)\).
32 The Fourier convention is
33 \[
34 F_{nk}=\frac{1}{\sqrt{12}}\exp\!\left(\frac{2\pi i nk}{12}\right),
35 \qquad n,k\in\{0,\ldots,11\}.
36 \]
37 The adjoint \(F^*\) therefore carries the negative exponential sign. The
38 selector \(D\) is diagonal with value one precisely at the residues
39 \(U=\{1,5,7,11\}\). The transported operator is \(P=FDF^*\).
40
41 Write
42 \[
43 c=(4,0,2,0,-2,0,-4,0,-2,0,2,0),\qquad
44 \psi=\frac{c}{\sqrt{48}},\qquad \chi=\frac{|c|}{\sqrt{48}}.
45 \]
46 Both vectors have norm one. Their initial probability histograms are identical,
47 but their inner product is zero. The vector \(u\) has entry \(1/2\) on \(U\)
48 and zero elsewhere. Lean proves the actual complex identities \(Fu=\psi\) and
49 \(F^*\psi=u\), as well as transformed coprime probability one for \(\psi\)
50 and zero for \(\chi\).
51
52 The statements are finite and exact. No parameterized arbitrary-modulus theorem,
53 general circuit construction, physical phase-removal process, or quantum speedup
54 is included in these formal claims.
55
56 \section{Revision reconciliation}
57 Two retrieved archives carry version \texttt{0.2.0}, but they do not have the same
58 active source. The earlier four-module checkpoint has 59 mathematical theorems
59 and four separately checked refutation controls. The later five-module checkpoint
60 has 96 mathematical theorems and three rejected control files. Its proof receipt
61 is the later \texttt{verification/final/REPORT.json}.
62
63 The original 22 finite-table statements are retained inside both checkpoints.
64 They are not counted a second time. Likewise, \(59+96\) is not a meaningful
65 theorem total: these are overlapping revisions of one formal development.
66
67 The earlier proof boundary disclosed that explicit projector transport and
68 normalized-state matrix actions had not yet been supplied. The later source
69 supplies both, connects the Fourier matrix to the usual complex exponential, and
70 proves a histogram nonreconstruction theorem. The earlier boundary remains a
71 record of its own revision, rather than a gap list for the current publication.
72
73 The entire later checkpoint is preserved under \texttt{lean/checked\_checkpoint}.
74 The source files are not edited to match this guide.
75
76 \section{Architecture of the proof}
77 The proof crosses two representations. First, rational coordinates support exact
78 finite calculations. Second, a semantics map transfers those calculations to
79 ordinary complex matrices and vectors.
80
81 \begin{center}
82 \begin{tabular}{p{0.27\linewidth}p{0.64\linewidth}}
83 \toprule
84 Layer & Role\\
85 \midrule
86 Rational tables & Signal, projector entries, filtering, and energies.\\
87 Exact coordinates & Algebra in the basis \(1,\sqrt3,i,i\sqrt3\).\\
88 Finite matrices & All entries indexed by \(\operatorname{Fin}(12)\), with exact finite sums.\\
89 Complex semantics & Preservation of multiplication, adjoint, matrix action, and squared norm.\\
90 Conventions & Identification of roots and normalization with standard exponentials and square roots.\\
91 Publication theorem & Bundling of the actual complex identities and reconstruction obstructions.\\
92 \bottomrule
93 \end{tabular}
94 \end{center}
95
96 The active import chain is \texttt{QuantumArithmeticBridge} into
97 \texttt{FiniteFourier}, then \texttt{SemanticBridge}, then \texttt{Conventions},
98 then \texttt{Publication}. Supporting Mathlib imports enter at the layer that
99 uses them. There is no circular theorem dependency.
100
101 \section{The rational signal and its filter}
102 The first layer uses literal rational lists. The chosen perturbation is
103 \(r_n=3\cos(\pi n/2)+2\), whose displayed rational entries can be certified
104 without numerical trigonometric evaluation. Its sum with \(c\) is the test signal.
105
106 \Needspace{16\baselineskip}
107 \noindent\textbf{Literal source.} \texttt{\detokenize{QuantumArithmeticBridge.lean}}, physical lines 51--61.
108
109 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
110 /-- Ramanujan sum c_12(n), n = 0,...,11. -/
111 def ramanujan12 : QVector :=
112 [4, 0, 2, 0, -2, 0, -4, 0, -2, 0, 2, 0]
113
114 /-- A deliberately off-band perturbation: 3 cos(pi n/2) + 2. -/
115 def noise12 : QVector :=
116 [5, 2, -1, 2, 5, 2, -1, 2, 5, 2, -1, 2]
117
118 /-- Signal used in the essay's filter demonstration. -/
119 def testSignal12 : QVector :=
120 [9, 2, 1, 2, 3, 2, -5, 2, 3, 2, 1, 2]
121 \end{Verbatim}
122
123 The cyclic matrix has entry \(c_{(n-m)\bmod12}/12\). The original layer proves
124 its symmetry, idempotence, preservation of \(c\), rejection of the chosen
125 perturbation, and exact recovery from the displayed contaminated signal.
126 The exact energy contract is \(150=48+102\).
127
128 \Needspace{6\baselineskip}
129 \noindent\textbf{Literal source.} \texttt{\detokenize{QuantumArithmeticBridge.lean}}, physical lines 92--126.
130
131 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize]
132 theorem projector12_idempotent :
133 matMulN 12 projector12 projector12 = projector12 := by
134 decide +kernel
135
136 /-- The arithmetic signal lies in the selected subspace. -/
137 theorem projector12_fixes_ramanujan :
138 matVec projector12 ramanujan12 = ramanujan12 := by
139 decide +kernel
140
141 /-- The chosen constant-plus-frequency-3 perturbation lies in the complementary subspace. -/
142 theorem projector12_kills_noise :
143 matVec projector12 noise12 = List.replicate 12 0 := by
144 decide +kernel
145
146 /-- Therefore the exact filter recovers the arithmetic component. -/
147 theorem projector12_recovers_test_signal :
148 matVec projector12 testSignal12 = ramanujan12 := by
149 decide +kernel
150
151 /-- The arithmetic amplitude vector has squared norm 48. -/
152 theorem ramanujan12_energy : sqEnergy ramanujan12 = 48 := by
153 decide +kernel
154
155 /-- The perturbation has squared norm 102. -/
156 theorem noise12_energy : sqEnergy noise12 = 102 := by
157 decide +kernel
158
159 /-- The full signal has squared norm 150. -/
160 theorem testSignal12_energy : sqEnergy testSignal12 = 150 := by
161 decide +kernel
162
163 /-- Exact orthogonal energy decomposition 150 = 48 + 102. -/
164 theorem energy_decomposition :
165 sqEnergy testSignal12 = sqEnergy ramanujan12 + sqEnergy noise12 := by
166 decide +kernel
167 \end{Verbatim}
168
169 The list operations use finite lists, including zero defaults and zip-based dot
170 products. These facts are therefore claims about the supplied twelve-entry
171 objects. They should not be silently interpreted as universal matrix theorems
172 for arbitrary ragged lists. The later \(\operatorname{Fin}(12)\) layer supplies
173 the typed matrix identities used in the publication.
174
175 \section{The exact phase arithmetic}
176 The structure \texttt{Cyclo12} represents
177 \[
178 (a,b,c,d)\longmapsto a+b\sqrt3+i(c+d\sqrt3),\qquad a,b,c,d\in\mathbb Q.
179 \]
180 Its multiplication explicitly incorporates \((\sqrt3)^2=3\) and \(i^2=-1\).
181 It is a concrete arithmetic representation. The development does not need or
182 install a global field instance to certify the finite example.
183
184 \Needspace{17\baselineskip}
185 \noindent\textbf{Literal source.} \texttt{\detokenize{QuantumArithmeticBridge.lean}}, physical lines 130--141.
186
187 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
188 /--
189 An exact coordinate model for Q(sqrt(3), i). The tuple (a,b,c,d) denotes
190 a + b*sqrt(3) + i*(c + d*sqrt(3)).
191 Only the concrete arithmetic needed for the q=12 certificate is used below;
192 we do not install a global field instance.
193 -/
194 structure Cyclo12 where
195 a : ℚ
196 b : ℚ
197 c : ℚ
198 d : ℚ
199 deriving DecidableEq, Repr
200 \end{Verbatim}
201
202 \Needspace{6\baselineskip}
203 \noindent\textbf{Literal source.} \texttt{\detokenize{QuantumArithmeticBridge.lean}}, physical lines 155--173.
204
205 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize]
206 /-- Multiplication in Q(sqrt(3), i). -/
207 def cMul (x y : Cyclo12) : Cyclo12 :=
208 ⟨x.a*y.a + 3*x.b*y.b - x.c*y.c - 3*x.d*y.d,
209 x.a*y.b + x.b*y.a - x.c*y.d - x.d*y.c,
210 x.a*y.c + 3*x.b*y.d + x.c*y.a + 3*x.d*y.b,
211 x.a*y.d + x.b*y.c + x.c*y.b + x.d*y.a⟩
212
213 def cConj (x : Cyclo12) : Cyclo12 := ⟨x.a, x.b, -x.c, -x.d⟩
214
215 def cPow (x : Cyclo12) : Nat → Cyclo12
216 | 0 => cOne
217 | n + 1 => cMul (cPow x n) x
218
219 def cSum : List Cyclo12 → Cyclo12
220 | [] => cZero
221 | x :: xs => cAdd x (cSum xs)
222
223 /-- zeta = exp(2*pi*i/12) = sqrt(3)/2 + i/2. -/
224 def zeta12 : Cyclo12 := ⟨0, (1/2 : ℚ), (1/2 : ℚ), 0⟩
225 \end{Verbatim}
226
227 The phase \(\zeta=(0,1/2,1/2,0)\) has complex meaning
228 \(\sqrt3/2+i/2\). Exact finite certificates establish its twelfth power, inverse,
229 and absence of a smaller positive power below twelve. Later the convention
230 module identifies it with \(\exp(\pi i/6)\).
231
232 The Ramanujan vector is obtained by summing powers of this phase over
233 \(1,5,7,11\). The negative-sign unnormalized DFT has value 12 at these four
234 frequencies and zero elsewhere. The absolute-value vector has Fourier support
235 on the even frequencies instead. These are exact phase calculations over
236 rational coordinates.
237
238 \section{Finite indices and normalized Fourier certificates}
239 The finite layer uses \texttt{Index := Fin 12}. Its normalized Fourier scale is
240 represented exactly as \(\sqrt3/6=1/\sqrt{12}\), and its state scale as
241 \(\sqrt3/12=1/\sqrt{48}\). The use of a finite index type makes every row and
242 column well defined without list-length side conditions.
243
244 \Needspace{6\baselineskip}
245 \noindent\textbf{Literal source.} \texttt{\detokenize{FiniteFourier.lean}}, physical lines 58--93.
246
247 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize]
248 /-- The stored arithmetic selector is exactly the coprimality predicate. -/
249 theorem coprime_residues_exact :
250 (List.range 12).filter (fun a => Nat.gcd a 12 == 1) = unitResidues12 := by
251 decide +kernel
252
253 theorem root_exact_order :
254 ∀ n : Fin 12, 0 < n.val → cPow zeta12 n.val ≠ cOne := by
255 decide +kernel
256
257 theorem normalized_fourier_left :
258 ∀ i j, kMatMul (kAdjoint exactFourier) exactFourier i j = kIdentity i j := by
259 decide +kernel
260
261 theorem normalized_fourier_right :
262 ∀ i j, kMatMul exactFourier (kAdjoint exactFourier) i j = kIdentity i j := by
263 decide +kernel
264
265 def selectedKernel : KMatrix := fun i j =>
266 kSum (fun k => if Nat.gcd k.val 12 = 1 then
267 cMul (exactFourier i k) (cConj (exactFourier j k)) else cZero)
268
269 theorem exact_projector_transport :
270 ∀ i j, selectedKernel i j = exactProjector i j := by
271 decide +kernel
272
273 theorem exact_projector_matches_rational_table :
274 ∀ i j, exactProjector i j = cRat ((projector12.getD i.val []).getD j.val 0) := by
275 decide +kernel
276
277 theorem exact_state_preparation :
278 ∀ i, kMatVec exactFourier exactUnitState i = exactPsi i := by
279 decide +kernel
280
281 theorem exact_state_recovery :
282 ∀ i, kMatVec (kAdjoint exactFourier) exactPsi i = exactUnitState i := by
283 decide +kernel
284 \end{Verbatim}
285
286 The two Fourier identities above quantify over all \(12\times12\) entries.
287 Kernel reduction proves these concrete universal statements over a finite type.
288 The selected-kernel equality and state actions are also complete finite
289 certificates, rather than floating-point matrix comparisons.
290
291 \section{Why the coordinate certificates mean complex identities}
292 The semantics map is explicitly defined with the positive real square root.
293 Soundness for addition, multiplication, conjugation, powers, and finite sums
294 prevents the exact coordinate layer from being a detached calculation with an
295 unproved interpretation.
296
297 \Needspace{6\baselineskip}
298 \noindent\textbf{Literal source.} \texttt{\detokenize{SemanticBridge.lean}}, physical lines 14--56.
299
300 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize]
301 /-- The exact coordinate arithmetic is interpreted in the ordinary complex numbers. -/
302 noncomputable def interpret (x : Cyclo12) : ℂ :=
303 ⟨(x.a : ℝ) + (x.b : ℝ) * Real.sqrt 3,
304 (x.c : ℝ) + (x.d : ℝ) * Real.sqrt 3⟩
305
306 @[simp] theorem interpret_zero : interpret cZero = 0 := by
307 apply Complex.ext <;> simp [interpret, cZero]
308
309 @[simp] theorem interpret_one : interpret cOne = 1 := by
310 apply Complex.ext <;> simp [interpret, cOne]
311
312 @[simp] theorem interpret_rat (r : ℚ) : interpret (cRat r) = (r : ℂ) := by
313 apply Complex.ext <;> simp [interpret, cRat]
314
315 @[simp] theorem interpret_add (x y : Cyclo12) :
316 interpret (cAdd x y) = interpret x + interpret y := by
317 apply Complex.ext <;> simp [interpret, cAdd] <;> ring
318
319 @[simp] theorem interpret_mul (x y : Cyclo12) :
320 interpret (cMul x y) = interpret x * interpret y := by
321 apply Complex.ext <;> simp [interpret, cMul, Complex.mul_re, Complex.mul_im] <;>
322 ring_nf <;> norm_num [Real.sq_sqrt]
323
324 @[simp] theorem interpret_conj (x : Cyclo12) :
325 interpret (cConj x) = star (interpret x) := by
326 apply Complex.ext <;> simp [interpret, cConj]
327 ring
328
329 @[simp] theorem interpret_pow (x : Cyclo12) (n : Nat) :
330 interpret (cPow x n) = interpret x ^ n := by
331 induction n with
332 | zero => simp [cPow]
333 | succ n ih => simp [cPow, ih, pow_succ]
334
335 @[simp] theorem interpret_sum (xs : List Cyclo12) :
336 interpret (cSum xs) = (xs.map interpret).sum := by
337 induction xs with
338 | nil => simp [cSum]
339 | cons x xs ih => simp [cSum, ih]
340
341 @[simp] theorem interpret_kSum (f : Index → Cyclo12) :
342 interpret (kSum f) = ∑ i, interpret (f i) := by
343 simp only [kSum, interpret_sum, List.map_ofFn, List.sum_ofFn]
344 \end{Verbatim}
345
346 The multiplication proof uses complex extensionality, real polynomial
347 normalization, and the square-root identity. It proves preservation for arbitrary
348 coordinates, not merely for the handful of roots that occur in the example.
349 The power and finite-sum proofs use induction.
350
351 Injectivity of this interpretation is not needed to transfer an equality: if
352 two coordinate expressions are proved equal, applying the interpretation gives
353 equal complex expressions. No claim of a globally packaged field equivalence is
354 required by the theorem chain.
355
356 \section{Matrix transport and actual unitarity}
357 The semantics layer proves that coordinate matrix multiplication, adjoint,
358 identity, and matrix-vector action have their ordinary complex meanings.
359 The matrices \(F,P,D\) and the normalized states are then defined directly
360 in that complex representation.
361
362 \Needspace{6\baselineskip}
363 \noindent\textbf{Literal source.} \texttt{\detokenize{SemanticBridge.lean}}, physical lines 65--91.
364
365 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize]
366 @[simp] theorem complexMatrix_mul (A B : KMatrix) :
367 complexMatrix (kMatMul A B) = complexMatrix A * complexMatrix B := by
368 ext i j
369 simp [complexMatrix, kMatMul, Matrix.mul_apply]
370
371 @[simp] theorem complexMatrix_adjoint (A : KMatrix) :
372 complexMatrix (kAdjoint A) = (complexMatrix A)ᴴ := by
373 ext i j
374 simp [complexMatrix, kAdjoint, Matrix.conjTranspose_apply]
375
376 @[simp] theorem complexMatrix_identity :
377 complexMatrix kIdentity = 1 := by
378 ext i j
379 by_cases h : i = j <;> simp [complexMatrix, kIdentity, h, Matrix.one_apply]
380
381 @[simp] theorem complexVector_mul (A : KMatrix) (v : KVector) :
382 complexVector (kMatVec A v) = (complexMatrix A).mulVec (complexVector v) := by
383 ext i
384 simp [complexVector, complexMatrix, kMatVec, Matrix.mulVec, dotProduct]
385
386 noncomputable def F : Matrix Index Index ℂ := complexMatrix exactFourier
387 noncomputable def P : Matrix Index Index ℂ := complexMatrix exactProjector
388 noncomputable def D : Matrix Index Index ℂ :=
389 Matrix.diagonal (fun i => if Nat.gcd i.val 12 = 1 then 1 else 0)
390 noncomputable def psi : Index → ℂ := complexVector exactPsi
391 noncomputable def chi : Index → ℂ := complexVector exactChi
392 noncomputable def unitState : Index → ℂ := complexVector exactUnitState
393 \end{Verbatim}
394
395 Consequently, the finite certificates produce actual complex unitarity and
396 projector transport. The following excerpt contains the full proofs of both
397 unitary identities, the cross-representation projector identity, and the two
398 state-action identities.
399
400 \Needspace{6\baselineskip}
401 \noindent\textbf{Literal source.} \texttt{\detokenize{SemanticBridge.lean}}, physical lines 93--120.
402
403 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize]
404 /-- Actual complex unitarity, not an assertion only about the coordinate checker. -/
405 theorem fourier_unitary_left : Fᴴ * F = 1 := by
406 have h : kMatMul (kAdjoint exactFourier) exactFourier = kIdentity :=
407 funext (fun i => funext (normalized_fourier_left i))
408 simpa [F] using congrArg complexMatrix h
409
410 theorem fourier_unitary_right : F * Fᴴ = 1 := by
411 have h : kMatMul exactFourier (kAdjoint exactFourier) = kIdentity :=
412 funext (fun i => funext (normalized_fourier_right i))
413 simpa [F] using congrArg complexMatrix h
414
415 theorem projector_transport : F * D * Fᴴ = P := by
416 ext i j
417 have h := congrArg interpret (exact_projector_transport i j)
418 simp only [selectedKernel, interpret_kSum] at h
419 rw [Matrix.mul_apply]
420 simpa [D, P, F, complexMatrix, Matrix.mul_diagonal, Matrix.conjTranspose_apply,
421 apply_ite interpret, mul_ite] using h
422
423 theorem state_preparation : F.mulVec unitState = psi := by
424 have h : kMatVec exactFourier exactUnitState = exactPsi :=
425 funext exact_state_preparation
426 simpa [F, unitState, psi] using congrArg complexVector h
427
428 theorem state_recovery : Fᴴ.mulVec psi = unitState := by
429 have h : kMatVec (kAdjoint exactFourier) exactPsi = exactUnitState :=
430 funext exact_state_recovery
431 simpa [F, unitState, psi] using congrArg complexVector h
432 \end{Verbatim}
433
434 This is the key strengthening over the earlier checkpoint. The rational matrix,
435 the exact coordinate kernel, and the complex matrix \(FDF^*\) are explicitly
436 connected. State preparation and recovery are equalities of actual complex
437 vectors. The theorem name \texttt{state\_preparation} describes a matrix identity,
438 not an efficient hardware preparation algorithm.
439
440 \section{The exponential sign and square-root normalization}
441 The usual Fourier matrix is not left as an informal interpretation. The
442 convention module proves that the coordinate root equals the positive
443 exponential root, including the selected square-root branch.
444
445 \Needspace{20\baselineskip}
446 \noindent\textbf{Literal source.} \texttt{\detokenize{Conventions.lean}}, physical lines 10--24.
447
448 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
449 /-- The coordinate root is exactly the usual exponential twelfth root. -/
450 theorem root_is_exponential :
451 interpret zeta12 = Complex.exp (((Real.pi / 6 : ℝ) : ℂ) * Complex.I) := by
452 rw [Complex.exp_mul_I]
453 rw [← Complex.ofReal_cos, ← Complex.ofReal_sin, Real.cos_pi_div_six, Real.sin_pi_div_six]
454 apply Complex.ext <;> simp [interpret, zeta12]
455 ring
456
457 theorem root_power_twelve : interpret zeta12 ^ 12 = 1 := by
458 simpa using congrArg interpret zeta12_order_certificate
459
460 theorem rootPower_interpret (n : Nat) :
461 interpret (rootPower n) = interpret zeta12 ^ n := by
462 simp only [rootPower, interpret_pow]
463 exact (pow_eq_pow_mod n root_power_twelve).symm
464 \end{Verbatim}
465
466 Its normalization lemmas prove \(\sqrt{12}=2\sqrt3\) and
467 \(\sqrt{48}=4\sqrt3\), then identify the exact scales with their ordinary
468 reciprocals. The matrix entry formula and state formula below are therefore
469 literal equalities in \(\mathbb C\).
470
471 \Needspace{18\baselineskip}
472 \noindent\textbf{Literal source.} \texttt{\detokenize{Conventions.lean}}, physical lines 42--54.
473
474 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
475 theorem fourierScale_interpret :
476 interpret fourierScale = ((1 / Real.sqrt 12 : ℝ) : ℂ) := by
477 apply Complex.ext <;> simp [interpret, fourierScale, sqrt_twelve]
478 have h : Real.sqrt 3 ≠ 0 := by positivity
479 field_simp
480 nlinarith [Real.sq_sqrt (show (0 : ℝ) ≤ 3 by norm_num)]
481
482 theorem stateScale_interpret :
483 interpret stateScale = ((1 / Real.sqrt 48 : ℝ) : ℂ) := by
484 apply Complex.ext <;> simp [interpret, stateScale, sqrt_fortyeight]
485 have h : Real.sqrt 3 ≠ 0 := by positivity
486 field_simp
487 nlinarith [Real.sq_sqrt (show (0 : ℝ) ≤ 3 by norm_num)]
488 \end{Verbatim}
489
490 \Needspace{15\baselineskip}
491 \noindent\textbf{Literal source.} \texttt{\detokenize{Conventions.lean}}, physical lines 56--65.
492
493 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
494 /-- The matrix checked in the certificate is the standard positive sign Fourier matrix. -/
495 theorem fourier_entry_formula (i j : Index) :
496 F i j = ((1 / Real.sqrt 12 : ℝ) : ℂ) *
497 Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (i.val : ℂ) * (j.val : ℂ) / 12) := by
498 simp only [F, complexMatrix, exactFourier, interpret_mul, fourierScale_interpret,
499 rootPower_interpret, root_is_exponential]
500 rw [← Complex.exp_nat_mul]
501 congr 2
502 push_cast
503 ring
504 \end{Verbatim}
505
506 \Needspace{21\baselineskip}
507 \noindent\textbf{Literal source.} \texttt{\detokenize{Conventions.lean}}, physical lines 67--82.
508
509 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
510 theorem psi_entry_formula (i : Index) :
511 psi i = ((1 / Real.sqrt 48 : ℝ) : ℂ) * (ramanujan12.getD i.val 0 : ℂ) := by
512 simp [psi, complexVector, exactPsi, stateScale_interpret]
513
514 theorem chi_entry_formula (i : Index) :
515 chi i = ((1 / Real.sqrt 48 : ℝ) : ℂ) * (absRamanujan12.getD i.val 0 : ℂ) := by
516 simp [chi, complexVector, exactChi, stateScale_interpret]
517
518 theorem unitState_entry_formula (i : Index) :
519 unitState i = if Nat.gcd i.val 12 = 1 then (1/2 : ℂ) else 0 := by
520 by_cases h : Nat.gcd i.val 12 = 1 <;>
521 simp [unitState, complexVector, exactUnitState, h]
522
523 theorem projector_entry_formula (i j : Index) :
524 P i j = (ramanujan12.getD ((i.val + 12 - j.val) % 12) 0 : ℂ) / 12 := by
525 simp [P, complexMatrix, exactProjector]
526 \end{Verbatim}
527
528 The convention is positive sign for \(F\) and negative sign for \(F^*\). The
529 earlier unnormalized \texttt{dft12} uses the negative sign. The normalization
530 and adjoint are the precise link between those notations.
531
532 \section{Hermitian projection and phase-sensitive states}
533 The selector is Hermitian and idempotent. Transport through a unitary matrix
534 then proves the corresponding facts for \(P\). They are ordinary matrix
535 identities, not claims that every rational list operation is an orthogonal
536 projection.
537
538 \Needspace{6\baselineskip}
539 \noindent\textbf{Literal source.} \texttt{\detokenize{Conventions.lean}}, physical lines 84--108.
540
541 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize]
542 theorem selector_idempotent : D * D = D := by
543 unfold D
544 rw [Matrix.diagonal_mul_diagonal]
545 congr 1
546 funext i
547 by_cases h : Nat.gcd i.val 12 = 1 <;> simp [h]
548
549 theorem selector_selfAdjoint : Dᴴ = D := by
550 ext i j
551 by_cases h : i = j
552 · subst j
553 simp [D, Matrix.conjTranspose_apply, apply_ite star]
554 · simp [D, Matrix.conjTranspose_apply, h, Ne.symm h]
555
556 theorem projector_idempotent_complex : P * P = P := by
557 rw [← projector_transport]
558 calc
559 (F * D * Fᴴ) * (F * D * Fᴴ) = F * D * (Fᴴ * F) * D * Fᴴ := by
560 simp only [Matrix.mul_assoc]
561 _ = F * D * Fᴴ := by rw [fourier_unitary_left, Matrix.mul_one, Matrix.mul_assoc F D D,
562 selector_idempotent]
563
564 theorem projector_selfAdjoint_complex : Pᴴ = P := by
565 rw [← projector_transport]
566 simp [Matrix.conjTranspose_mul, selector_selfAdjoint, Matrix.mul_assoc]
567 \end{Verbatim}
568
569 The vectors \(\psi\) and \(\chi\) are separately defined states. One is the
570 signed arithmetic amplitude vector and the other its entrywise absolute value.
571 They have the same squared amplitudes at each initial index but retain different
572 relative phase. The development neither claims nor requires a universal quantum
573 operation implementing the nonlinear map \(v\mapsto |v|\).
574
575 \Needspace{6\baselineskip}
576 \noindent\textbf{Literal source.} \texttt{\detokenize{SemanticBridge.lean}}, physical lines 145--174.
577
578 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize]
579 theorem psi_normalized : totalProbability psi = 1 := by
580 have h := congrArg interpret exact_psi_normalized
581 simpa [psi] using congrArg Complex.re h
582
583 theorem chi_normalized : totalProbability chi = 1 := by
584 have h := congrArg interpret exact_chi_normalized
585 simpa [chi] using congrArg Complex.re h
586
587 theorem unitState_normalized : totalProbability unitState = 1 := by
588 have h := congrArg interpret exact_unit_normalized
589 simpa [unitState] using congrArg Complex.re h
590
591 theorem same_initial_probabilities (i : Index) :
592 Complex.normSq (psi i) = Complex.normSq (chi i) := by
593 have h := congrArg interpret (exact_same_initial_probabilities i)
594 simpa [psi, chi, complexVector] using congrArg Complex.re h
595
596 theorem states_orthogonal : ∑ i, star (psi i) * chi i = 0 := by
597 have h := congrArg interpret exact_orthogonal_states
598 simpa [psi, chi, complexVector] using h
599
600 theorem signed_state_recovers_arithmetic :
601 coprimeProbability (Fᴴ.mulVec psi) = 1 := by
602 have h := congrArg interpret exact_coprime_mass_psi
603 simpa [F, psi] using congrArg Complex.re h
604
605 theorem unsigned_state_erases_arithmetic :
606 coprimeProbability (Fᴴ.mulVec chi) = 0 := by
607 have h := congrArg interpret exact_coprime_mass_chi
608 simpa [F, chi] using congrArg Complex.re h
609 \end{Verbatim}
610
611 The transformed probability statement is exact. The measurement event is the
612 coprime-frequency subset. After applying \(F^*\), its probability is one for
613 \(\psi\) and zero for \(\chi\). This basis change reveals information that their
614 shared initial histogram does not contain.
615
616 \section{Two exact information-loss statements}
617 The formal development isolates distinct obstructions. First, the initial
618 histogram cannot be inverted on both states by any reconstruction function.
619 Second, the projector itself is noninjective because it annihilates the nonzero
620 normalized state \(\chi\).
621
622 \Needspace{17\baselineskip}
623 \noindent\textbf{Literal source.} \texttt{\detokenize{Publication.lean}}, physical lines 39--50.
624
625 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
626 /-- No state reconstruction function can invert the initial probability histogram on both states. -/
627 theorem no_reconstruction_from_initial_probabilities :
628 ¬ ∃ R : (Index → ℝ) → (Index → ℂ),
629 R (fun i => Complex.normSq (psi i)) = psi ∧
630 R (fun i => Complex.normSq (chi i)) = chi := by
631 rintro ⟨R, hpsi, hchi⟩
632 have heq : (fun i => Complex.normSq (psi i)) =
633 (fun i => Complex.normSq (chi i)) := funext same_initial_probabilities
634 have hstate : psi = chi := by rw [← hpsi, ← hchi, heq]
635 have h := signed_state_recovers_arithmetic
636 rw [hstate, unsigned_state_erases_arithmetic] at h
637 norm_num at h
638 \end{Verbatim}
639
640 \Needspace{11\baselineskip}
641 \noindent\textbf{Literal source.} \texttt{\detokenize{Publication.lean}}, physical lines 52--57.
642
643 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
644 /-- Exact probabilities in the recovered basis, connected to the normalized state. -/
645 theorem recovered_probability_at (i : Index) :
646 Complex.normSq (Fᴴ.mulVec psi i) =
647 if Nat.gcd i.val 12 = 1 then (1/4 : ℝ) else 0 := by
648 rw [state_recovery, unitState_entry_formula]
649 by_cases h : Nat.gcd i.val 12 = 1 <;> norm_num [h, Complex.normSq_apply]
650 \end{Verbatim}
651
652 \Needspace{12\baselineskip}
653 \noindent\textbf{Literal source.} \texttt{\detokenize{Publication.lean}}, physical lines 59--65.
654
655 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
656 /-- The operator is not injective. Its nonzero normalized kernel state is explicit. -/
657 theorem projector_not_injective : ¬ Function.Injective P.mulVec := by
658 intro h
659 have hz : chi = 0 := h (by simp [projector_kills_chi])
660 have hp := chi_normalized
661 rw [hz] at hp
662 norm_num [totalProbability] at hp
663 \end{Verbatim}
664
665 The nonreconstruction theorem quantifies over every function from real-valued
666 histograms to complex-valued vectors. It uses equality of the two histograms and
667 the incompatible transformed probabilities. This is a mathematical obstruction
668 to a specified inverse, not a statistical claim about estimating a state from
669 many measurements in several bases.
670
671 The traditional paper also proves that the two states cannot both be recovered
672 up to an overall phase from this histogram. That strengthening is a prose
673 corollary of their orthogonality and normalization. It is not separately exported
674 as a quotient-by-global-phase Lean theorem.
675
676 Projection becomes reconstructive when its residual is retained. The next
677 identity holds for every twelve-dimensional complex vector, including vectors
678 outside the arithmetic signal subspace.
679
680 \Needspace{10\baselineskip}
681 \noindent\textbf{Literal source.} \texttt{\detokenize{Publication.lean}}, physical lines 33--37.
682
683 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
684 /-- Every signal is reconstructible from the retained and discarded components together. -/
685 theorem projector_residual_reconstructs (v : Index → ℂ) :
686 P.mulVec v + (1 - P).mulVec v = v := by
687 rw [Matrix.sub_mulVec, Matrix.one_mulVec]
688 exact add_sub_cancel _ _
689 \end{Verbatim}
690
691 Its proof is algebraic. The identity \(Pv+(I-P)v=v\) itself does not require
692 idempotence. Hermitian idempotence supplies the stronger interpretation as
693 orthogonal retained and discarded components. This separates the reconstruction
694 identity from the additional geometric structure.
695
696 \section{The publication theorem in full}
697 The final declaration bundles the formal core of the worked example. Every
698 conjunct is supported by a previously proved declaration rather than by a new
699 numerical test or an implicit physical assumption.
700
701 \Needspace{19\baselineskip}
702 \noindent\textbf{Literal source.} \texttt{\detokenize{Publication.lean}}, physical lines 67--80.
703
704 \begin{Verbatim}[breaklines=true,breakanywhere=true,fontsize=\footnotesize,samepage=true]
705 /-- Publication theorem gathering the complex identities stated in the worked example. -/
706 theorem publication_bridge :
707 Fᴴ * F = 1 ∧ F * Fᴴ = 1 ∧ F * D * Fᴴ = P ∧
708 P * P = P ∧ Pᴴ = P ∧ F.mulVec unitState = psi ∧
709 Fᴴ.mulVec psi = unitState ∧ totalProbability psi = 1 ∧
710 totalProbability chi = 1 ∧
711 (∀ i, Complex.normSq (psi i) = Complex.normSq (chi i)) ∧
712 (∑ i, star (psi i) * chi i) = 0 ∧
713 coprimeProbability (Fᴴ.mulVec psi) = 1 ∧
714 coprimeProbability (Fᴴ.mulVec chi) = 0 := by
715 exact ⟨fourier_unitary_left, fourier_unitary_right, projector_transport,
716 projector_idempotent_complex, projector_selfAdjoint_complex, state_preparation,
717 state_recovery, psi_normalized, chi_normalized, same_initial_probabilities,
718 states_orthogonal, signed_state_recovers_arithmetic, unsigned_state_erases_arithmetic⟩
719 \end{Verbatim}
720
721 The bundled theorem has a fixed dimension and explicitly named operators and
722 states. It establishes the bridge used in the paper. Broader arbitrary-modulus
723 results remain separate prose theorems, with their own proofs and evidence.
724
725 The manuscript's QA18 additionally includes filtering and energy, normalization
726 of \(u\), the projector actions on both states, and noninjectivity. Those clauses
727 use separately exported declarations, including
728 \texttt{projector12\_recovers\_test\_signal}, \texttt{energy\_decomposition},
729 \texttt{unitState\_normalized}, \texttt{projector\_fixes\_psi},
730 \texttt{projector\_kills\_chi}, and \texttt{projector\_not\_injective}.
731 The complete machine concordance lists these supporting results. The manuscript
732 bundle is not identified with a literal statement that omits its extra clauses.
733
734 \section{Manuscript-to-Lean concordance}
735 The main paper labels its results QA01 through QA20. The table below distinguishes
736 the exact fixed-example formal coverage from the more general mathematical
737 development. ``Not formalized here'' is a scope label, not a claim that the prose
738 result is false.
739
740 \small
741 \begin{longtable}{p{0.08\linewidth}p{0.26\linewidth}p{0.56\linewidth}}
742 \toprule
743 Claim & Subject & Formal coverage\\
744 \midrule
745 \endhead
746 QA01 & Primitive root & Exact order 12 and standard exponential root.\\
747 QA02 & Character orthogonality & Fixed-example content through both exact unitary identities; general theorem not separately exported.\\
748 QA03 & Fourier theory & Both ordinary complex unitary identities and standard entry formula; general Parseval theorem not separately exported.\\
749 QA04 & M\"obius formula & General modulus formula not formalized; exact integer table for 12 certified.\\
750 QA05 & Ramanujan support & Exact signed and unsigned twelve-frequency DFT tables and arithmetic energy 48.\\
751 QA06 & Divisor projectors & Primitive-order projector at 12 certified; the full divisor family not a general Lean family.\\
752 QA07 & Projector geometry & Hermitian idempotence, displayed energies, explicit noninjectivity, and all-vector residual reconstruction.\\
753 QA08 & Residue recombination & No theorem in this checkpoint.\\
754 QA09 & Polyphase aliasing & No theorem in this checkpoint.\\
755 QA10 & Arithmetic example & Phase sum connected to the exact rational sample table.\\
756 QA11 & Exact filtering & Displayed contaminated signal and orthogonal energy decomposition.\\
757 QA12 & State preparation & Ordinary complex normalized vector actions and recovery.\\
758 QA13 & Shared histogram & Entrywise probability equality and state orthogonality.\\
759 QA14 & Phase separation & Actual transformed coprime probabilities 1 versus 0.\\
760 QA15 & Reconstruction barrier & No vector-valued initial-histogram inverse works on both specified states; the global-phase corollary is prose only.\\
761 QA16 & Measurement law & Relevant projector algebra and state probabilities; no general conditional-state-update API.\\
762 QA17 & Arithmetic semantics & Soundness for scalar, matrix, vector, adjoint, and mass operations.\\
763 QA18 & Central bridge & Publication bundle plus separately exported filter, energy, normalization, projector-action, and noninjectivity results.\\
764 QA19 & Relative-phase family & Prose extension \(\sin^2(\theta/2)\); not an inherited Lean theorem.\\
765 QA20 & Dephased probability & Prose density-matrix calculation \(1/3\); not an inherited Lean theorem.\\
766 \bottomrule
767 \end{longtable}
768 \normalsize
769
770 The machine concordance includes all theorem statements verbatim, per-theorem
771 axiom records, source hashes, and exact physical line locators. Its mapping
772 records formal scope; it does not upgrade general manuscript claims merely
773 because a nearby finite special case is checked.
774
775 \section{Trust boundary and current verification}
776 The current replay uses Lean 4.34.0-rc2, compiler commit
777 \texttt{\detokenize{6a10ac8c22beadecabdbb0919c2b50214762f91d}}, and Mathlib revision
778 \texttt{\detokenize{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}}.
779 It built the five source modules with warnings treated as errors, printed axiom
780 dependencies for all 96 named theorems, and replayed each module with
781 \texttt{leanchecker}. The compiler and imported dependency cache were not rebuilt
782 from their source. Kernel replay uses Lean's own kernel, not a second independent
783 proof checker.
784
785 The axiom union is exactly \texttt{propext}, \texttt{Classical.choice}, and
786 \texttt{Quot.sound}. This is the standard foundation used by the audited proof
787 terms, not an axiom-free claim. The active source contains no proof placeholders,
788 custom axiom declarations, native decision proofs, or unsafe declarations.
789 Historical failed or native-decision drafts are excluded from the active build.
790
791 Current source reconciliation checked all five source hashes and all eleven
792 archived check-log hashes against the archived report. All sixteen match.
793 The current inventory contains exactly 96 unique names and 96 archived axiom
794 records. All line numbers agree with the archived source index.
795
796 The pinned portable runtime was restored and verified against its combined archive hash. A fresh build, all 96 theorem axiom inspections, and all five kernel replays passed. The complete receipt and logs accompany the source package. Earlier transfer failures remain historical records.
797
798 \section{Controls, failed attempts, and reproducibility}
799 The latest archive rejected a deliberately false signal sign and a proof using
800 \texttt{sorry} under warnings as errors. Its false Fourier-mode control also
801 failed, but the compiler stopped at opaque \texttt{Decidable} reduction. That
802 failure alone is not a direct mathematical certificate that the proposition is
803 false. The positive \texttt{ramanujan\_dft\_table} theorem separately establishes
804 the correct value 12.
805
806 The control runner's broad diagnostic expression can match the word ``false''
807 in a filename. The guide does not interpret that match as a stronger arithmetic
808 test than the actual log provides. The earlier checkpoint's four explicit
809 refutation proofs are retained as earlier evidence and are not silently counted
810 as current production theorems.
811
812 A supplementary current check closes the diagnostic gap for the false-mode control. It derives the exact mode-one value and its negation from the proved Fourier table, replays the supplementary module through the kernel, and rejects a false rational-coordinate equality with an explicit false-value diagnostic. These two verification lemmas do not increase the monograph count of 96 theorems.
813
814 The supplied verifier creates a fresh source project, checks dependency revisions,
815 builds, prints all theorem axiom dependencies, replays all five modules, and runs
816 the controls. It refuses to overwrite an existing fresh build directory and
817 treats timeouts as failures. It makes no network requests or installations.
818 With the pinned runtime restored, the documented command is:
819
820 \begin{Verbatim}[breaklines=true,fontsize=\footnotesize]
821 python scripts/verify_lean.py \
822 --toolchain /path/to/Komorebi_Portable_Lean_4.34.0-rc2/toolchain \
823 --packages /path/to/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages \
824 --out verification/reproduction_new
825 \end{Verbatim}
826 The runner was exercised under Linux x86-64. It uses POSIX process groups and
827 filesystem symlinks. Native Windows behavior is not tested. WSL2 with the pinned
828 Linux runtime is the documented route for a Windows machine.
829
830 Full proof source, manifests, archived build and replay logs, the static
831 concordance builder, and the current successful replay receipt are
832 included. The runtime itself remains an external dependency.
833
834 \section{Complete active theorem inventory}
835 All names in the following table have prefix
836 \texttt{Komorebi.QuantumArithmetic}. File and physical source line identify the
837 exact declaration. The full literal statements and axiom lists are also available
838 in \texttt{Lean\_Concordance.json} and \texttt{Lean\_Concordance.csv}.
839
840 \Needspace{10\baselineskip}
841 \subsection{\texttt{\detokenize{QuantumArithmeticBridge}}: 22 theorems}
842
843 \small\begin{longtable}{p{0.79\linewidth}r}
844 \toprule Declaration & Line\\\midrule\endhead
845 \texttt{\detokenize{ramanujan12_length}} & 80\\
846 \texttt{\detokenize{projector12_shape}} & 82\\
847 \texttt{\detokenize{projector12_symmetric}} & 88\\
848 \texttt{\detokenize{projector12_idempotent}} & 92\\
849 \texttt{\detokenize{projector12_fixes_ramanujan}} & 97\\
850 \texttt{\detokenize{projector12_kills_noise}} & 102\\
851 \texttt{\detokenize{projector12_recovers_test_signal}} & 107\\
852 \texttt{\detokenize{ramanujan12_energy}} & 112\\
853 \texttt{\detokenize{noise12_energy}} & 116\\
854 \texttt{\detokenize{testSignal12_energy}} & 120\\
855 \texttt{\detokenize{energy_decomposition}} & 124\\
856 \texttt{\detokenize{zeta12_order_certificate}} & 177\\
857 \texttt{\detokenize{zeta12_inverse_certificate}} & 180\\
858 \texttt{\detokenize{ramanujanC12_table}} & 190\\
859 \texttt{\detokenize{ramanujan_dft_table}} & 205\\
860 \texttt{\detokenize{abs_ramanujan_dft_table}} & 217\\
861 \texttt{\detokenize{same_computational_basis_probabilities}} & 231\\
862 \texttt{\detokenize{abs_ramanujan12_energy}} & 235\\
863 \texttt{\detokenize{recovered_mode_probability}} & 243\\
864 \texttt{\detokenize{recovered_total_probability}} & 248\\
865 \texttt{\detokenize{phase_stripping_coprime_probability}} & 253\\
866 \texttt{\detokenize{arithmetic_signal_quantum_bridge}} & 258\\
867 \bottomrule\end{longtable}\normalsize
868
869 \Needspace{10\baselineskip}
870 \subsection{\texttt{\detokenize{FiniteFourier}}: 17 theorems}
871
872 \small\begin{longtable}{p{0.79\linewidth}r}
873 \toprule Declaration & Line\\\midrule\endhead
874 \texttt{\detokenize{coprime_residues_exact}} & 59\\
875 \texttt{\detokenize{root_exact_order}} & 63\\
876 \texttt{\detokenize{normalized_fourier_left}} & 67\\
877 \texttt{\detokenize{normalized_fourier_right}} & 71\\
878 \texttt{\detokenize{exact_projector_transport}} & 79\\
879 \texttt{\detokenize{exact_projector_matches_rational_table}} & 83\\
880 \texttt{\detokenize{exact_state_preparation}} & 87\\
881 \texttt{\detokenize{exact_state_recovery}} & 91\\
882 \texttt{\detokenize{exact_unit_normalized}} & 95\\
883 \texttt{\detokenize{exact_psi_normalized}} & 98\\
884 \texttt{\detokenize{exact_chi_normalized}} & 101\\
885 \texttt{\detokenize{exact_same_initial_probabilities}} & 104\\
886 \texttt{\detokenize{exact_orthogonal_states}} & 108\\
887 \texttt{\detokenize{exact_coprime_mass_psi}} & 112\\
888 \texttt{\detokenize{exact_coprime_mass_chi}} & 116\\
889 \texttt{\detokenize{exact_projector_fixes_psi}} & 120\\
890 \texttt{\detokenize{exact_projector_kills_chi}} & 124\\
891 \bottomrule\end{longtable}\normalsize
892
893 \Needspace{10\baselineskip}
894 \subsection{\texttt{\detokenize{SemanticBridge}}: 30 theorems}
895
896 \small\begin{longtable}{p{0.79\linewidth}r}
897 \toprule Declaration & Line\\\midrule\endhead
898 \texttt{\detokenize{interpret_zero}} & 19\\
899 \texttt{\detokenize{interpret_one}} & 22\\
900 \texttt{\detokenize{interpret_rat}} & 25\\
901 \texttt{\detokenize{interpret_add}} & 28\\
902 \texttt{\detokenize{interpret_mul}} & 32\\
903 \texttt{\detokenize{interpret_conj}} & 37\\
904 \texttt{\detokenize{interpret_pow}} & 42\\
905 \texttt{\detokenize{interpret_sum}} & 48\\
906 \texttt{\detokenize{interpret_kSum}} & 54\\
907 \texttt{\detokenize{complexMatrix_mul}} & 65\\
908 \texttt{\detokenize{complexMatrix_adjoint}} & 70\\
909 \texttt{\detokenize{complexMatrix_identity}} & 75\\
910 \texttt{\detokenize{complexVector_mul}} & 80\\
911 \texttt{\detokenize{fourier_unitary_left}} & 94\\
912 \texttt{\detokenize{fourier_unitary_right}} & 99\\
913 \texttt{\detokenize{projector_transport}} & 104\\
914 \texttt{\detokenize{state_preparation}} & 112\\
915 \texttt{\detokenize{state_recovery}} & 117\\
916 \texttt{\detokenize{interpret_normSq}} & 122\\
917 \texttt{\detokenize{interpret_mass}} & 133\\
918 \texttt{\detokenize{interpret_coprimeMass}} & 137\\
919 \texttt{\detokenize{psi_normalized}} & 145\\
920 \texttt{\detokenize{chi_normalized}} & 149\\
921 \texttt{\detokenize{unitState_normalized}} & 153\\
922 \texttt{\detokenize{same_initial_probabilities}} & 157\\
923 \texttt{\detokenize{states_orthogonal}} & 162\\
924 \texttt{\detokenize{signed_state_recovers_arithmetic}} & 166\\
925 \texttt{\detokenize{unsigned_state_erases_arithmetic}} & 171\\
926 \texttt{\detokenize{projector_fixes_psi}} & 176\\
927 \texttt{\detokenize{projector_kills_chi}} & 181\\
928 \bottomrule\end{longtable}\normalsize
929
930 \Needspace{10\baselineskip}
931 \subsection{\texttt{\detokenize{Conventions}}: 17 theorems}
932
933 \small\begin{longtable}{p{0.79\linewidth}r}
934 \toprule Declaration & Line\\\midrule\endhead
935 \texttt{\detokenize{root_is_exponential}} & 11\\
936 \texttt{\detokenize{root_power_twelve}} & 18\\
937 \texttt{\detokenize{rootPower_interpret}} & 21\\
938 \texttt{\detokenize{sqrt_twelve}} & 26\\
939 \texttt{\detokenize{sqrt_fortyeight}} & 34\\
940 \texttt{\detokenize{fourierScale_interpret}} & 42\\
941 \texttt{\detokenize{stateScale_interpret}} & 49\\
942 \texttt{\detokenize{fourier_entry_formula}} & 57\\
943 \texttt{\detokenize{psi_entry_formula}} & 67\\
944 \texttt{\detokenize{chi_entry_formula}} & 71\\
945 \texttt{\detokenize{unitState_entry_formula}} & 75\\
946 \texttt{\detokenize{projector_entry_formula}} & 80\\
947 \texttt{\detokenize{selector_idempotent}} & 84\\
948 \texttt{\detokenize{selector_selfAdjoint}} & 91\\
949 \texttt{\detokenize{projector_idempotent_complex}} & 98\\
950 \texttt{\detokenize{projector_selfAdjoint_complex}} & 106\\
951 \texttt{\detokenize{complete_phase_separation}} & 111\\
952 \bottomrule\end{longtable}\normalsize
953
954 \Needspace{10\baselineskip}
955 \subsection{\texttt{\detokenize{Publication}}: 10 theorems}
956
957 \small\begin{longtable}{p{0.79\linewidth}r}
958 \toprule Declaration & Line\\\midrule\endhead
959 \texttt{\detokenize{exact_phase_signal_lookup}} & 9\\
960 \texttt{\detokenize{complex_ramanujan_signal}} & 14\\
961 \texttt{\detokenize{absolute_signal_lookup}} & 22\\
962 \texttt{\detokenize{retained_discarded_orthogonal}} & 27\\
963 \texttt{\detokenize{signal_decomposition}} & 30\\
964 \texttt{\detokenize{projector_residual_reconstructs}} & 34\\
965 \texttt{\detokenize{no_reconstruction_from_initial_probabilities}} & 40\\
966 \texttt{\detokenize{recovered_probability_at}} & 53\\
967 \texttt{\detokenize{projector_not_injective}} & 60\\
968 \texttt{\detokenize{publication_bridge}} & 68\\
969 \bottomrule\end{longtable}\normalsize
970
971 \section{What completion means here}
972 The fixed twelve-dimensional bridge is formally covered in the preserved later
973 checkpoint. This guide and machine concordance expose its proof and trust
974 boundaries.
975
976 General-modulus M\"obius and divisor-projector theory, polyphase identities, and a
977 general measurement API remain outside this Lean package. The traditional paper
978 supplies separate proofs. The current pinned replay passed for the fixed formal package.
979
980
981 \section{The original finite bridge and its extension}
982 \hypertarget{q:formal-coverage-lineage-and-reproducibility}{%
983 \section{Formal coverage, lineage, and
984 reproducibility}\label{q:formal-coverage-lineage-and-reproducibility}}
985
986 \hypertarget{q:two-inherited-checkpoints-and-the-expanded-boundary}{%
987 \subsection{Two inherited checkpoints and the expanded
988 boundary}\label{q:two-inherited-checkpoints-and-the-expanded-boundary}}
989
990 The earlier checked package has four mathematical production modules and
991 fifty-nine named theorem declarations. Its first module preserves
992 twenty-two original statements. Its proof-boundary document correctly
993 says that explicit matrix transport between independently defined
994 representations and normalized state-action identities are not supplied
995 as additional theorems in that package. Those limitations must not be
996 erased when describing the earlier evidence.
997
998 \Needspace{16\baselineskip}
999 The later checked package has five production modules and ninety-six
1000 named theorem declarations:
1001
1002 {\small\begin{longtable}[]{@{}
1003 >{\raggedright\arraybackslash}p{\dimexpr 0.3333\columnwidth - 1.3332\tabcolsep\relax}
1004 >{\raggedleft\arraybackslash}p{\dimexpr 0.3333\columnwidth - 1.3332\tabcolsep\relax}
1005 >{\raggedright\arraybackslash}p{\dimexpr 0.3333\columnwidth - 1.3332\tabcolsep\relax}@{}}
1006 \toprule\noalign{}
1007 \begin{minipage}[b]{\linewidth}\raggedright
1008 Module
1009 \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft
1010 Named theorems
1011 \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
1012 Principal role
1013 \end{minipage} \\
1014 \midrule\noalign{}
1015 \endhead
1016 \bottomrule\noalign{}
1017 \endlastfoot
1018 \texttt{QuantumArithmeticBridge} & 22 & Literal rational projector and
1019 cyclotomic tables \\
1020 \texttt{FiniteFourier} & 17 & Indexed exact Fourier and normalized state
1021 identities \\
1022 \texttt{SemanticBridge} & 30 & Sound complex interpretation and
1023 transported identities \\
1024 \texttt{Conventions} & 17 & Exponential entries, scales, and complex
1025 projector laws \\
1026 \texttt{Publication} & 10 & Phase lookup, residual reconstruction,
1027 nonreconstruction, and central bundle \\
1028 Total & 96 & Finite modulus-twelve proof chain, including helpers \\
1029 \end{longtable}}
1030
1031 The later source explicitly supplies \(FDF^\dagger=P\), both normalized
1032 state-action identities, the conventional exponential formula for \(F\),
1033 identical initial probabilities, orthogonality, exact selected
1034 probability one versus zero, histogram nonreconstruction, and projector
1035 noninjectivity. It therefore closes the representation-transport
1036 obligations that the earlier package leaves outside its formal boundary.
1037
1038 The ninety-six count includes helper lemmas and bundled propositions. It
1039 is not a count of ninety-six independent discoveries. Nor should the
1040 earlier fifty-nine and later ninety-six counts be added as if their
1041 shared declarations were disjoint.
1042
1043 \hypertarget{q:current-and-inherited-checks}{%
1044 \subsection{Current and inherited
1045 checks}\label{q:current-and-inherited-checks}}
1046
1047 This edition preserves the source, theorem index, verification records,
1048 and compiled-artifact lineage of the checked checkpoints. The archived
1049 records provide the earlier compiler and kernel-checking evidence.
1050 Current static audits and independent Python replay provide current
1051 bounded evidence about the downloaded files and the example
1052 implementation. These are disclosed separately in the release records.
1053
1054 The pinned runtime was restored for this completion pass. Fresh source compilation, axiom inspection, and replay of all five modules passed. The separate historical failures are preserved in the source records.
1055
1056 The exact source uses kernel-reduction decision proofs for finite
1057 identities and ordinary proof terms for the transport lemmas. The
1058 declaration audit rejects admitted proofs and unapproved
1059 project-specific axioms. Standard foundational dependencies are reported
1060 in the formal guide. Compiled artifact checking reuses Lean's kernel; it
1061 is not an independently implemented proof assistant.
1062
1063 The later checkpoint preserves three negative controls with distinct
1064 meanings. The false-sign claim is a directly false finite statement. The
1065 false-mode case is an operational rejection whose failure mechanism must
1066 be read alongside its diagnostic and the positive checked transform
1067 table. The admitted-proof case tests the verification policy for
1068 incomplete proof evidence. These controls are not combined with the four
1069 controls of the earlier checkpoint into an artificial total.
1070
1071 \hypertarget{q:independent-arithmetic-evidence}{%
1072 \subsection{Independent arithmetic
1073 evidence}\label{q:independent-arithmetic-evidence}}
1074
1075 The original reproducibility package records 3,003 exact Python
1076 assertions, separately from floating-point checks. Its exact verifier
1077 represents the twelfth root in a cyclotomic quotient, checks the signal
1078 and transform tables, the rational projector identities, the test-signal
1079 decomposition, divisor-shell completeness, and the phase-sensitive
1080 example. Its arithmetic regression range is bounded to moduli two
1081 through sixty-four.
1082
1083 The release also includes the current replay and any added finite checks
1084 with their own records. Exact rational or cyclotomic arithmetic and
1085 numerical residuals are reported separately. A small floating-point
1086 residual verifies the implementation at its declared tolerance; it does
1087 not replace the exact proof of the general formula. Likewise, a finite
1088 modulus sweep does not prove the arbitrary-modulus theorem. QA01 through
1089 QA09 provide the general proofs needed here.
1090
1091 \hypertarget{q:the-twenty-two-preserved-original-statements}{%
1092 \subsection{The twenty-two preserved original
1093 statements}\label{q:the-twenty-two-preserved-original-statements}}
1094
1095 The original bridge module's statements remain available under their
1096 original names. The following list records their substantive content
1097 rather than treating each source helper as a separate main theorem.
1098
1099 {\small\begin{longtable}[]{@{}
1100 >{\raggedright\arraybackslash}p{\dimexpr 0.5000\columnwidth - 1.0000\tabcolsep\relax}
1101 >{\raggedright\arraybackslash}p{\dimexpr 0.5000\columnwidth - 1.0000\tabcolsep\relax}@{}}
1102 \toprule\noalign{}
1103 \begin{minipage}[b]{\linewidth}\raggedright
1104 Original declaration
1105 \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
1106 Preserved statement
1107 \end{minipage} \\
1108 \midrule\noalign{}
1109 \endhead
1110 \bottomrule\noalign{}
1111 \endlastfoot
1112 \texttt{ramanujan12\_length} & The rational signal list has length
1113 twelve \\
1114 \texttt{projector12\_shape} & The literal matrix has twelve rows and
1115 twelve columns \\
1116 \texttt{projector12\_symmetric} & The rational matrix equals its
1117 transpose \\
1118 \texttt{projector12\_idempotent} & Exact rational multiplication gives
1119 \(P^2=P\) \\
1120 \texttt{projector12\_fixes\_ramanujan} & The matrix fixes the signal
1121 \(c\) \\
1122 \texttt{projector12\_kills\_noise} & The matrix sends the displayed
1123 perturbation \(b\) to zero \\
1124 \texttt{projector12\_recovers\_test\_signal} & Applying it to \(x\)
1125 returns \(c\) \\
1126 \texttt{ramanujan12\_energy} & \(\|c\|^2=48\) \\
1127 \texttt{noise12\_energy} & \(\|b\|^2=102\) \\
1128 \texttt{testSignal12\_energy} & \(\|x\|^2=150\) \\
1129 \texttt{energy\_decomposition} & The exact energy balance is
1130 \(150=48+102\) \\
1131 \texttt{zeta12\_order\_certificate} & The coordinate root raised to the
1132 twelfth power is one \\
1133 \texttt{zeta12\_inverse\_certificate} & The coordinate root times its
1134 conjugate is one \\
1135 \texttt{ramanujanC12\_table} & Four primitive phase sums give the exact
1136 twelve-entry signal table \\
1137 \texttt{ramanujan\_dft\_table} & The negative-sign DFT gives twelve
1138 exactly at \(1,5,7,11\) \\
1139 \texttt{abs\_ramanujan\_dft\_table} & The unsigned DFT gives the exact
1140 even-support table \\
1141 \texttt{same\_computational\_basis\_probabilities} & Signed and unsigned
1142 rational entries have the same squares \\
1143 \texttt{abs\_ramanujan12\_energy} & The unsigned signal also has squared
1144 energy forty-eight \\
1145 \texttt{recovered\_mode\_probability} & The scalar normalization gives
1146 \(12^2/(48\cdot12)=1/4\) \\
1147 \texttt{recovered\_total\_probability} & Four recovered mode
1148 probabilities sum to one \\
1149 \texttt{phase\_stripping\_coprime\_probability} & Zero transformed
1150 coefficients give zero selected mass \\
1151 \texttt{arithmetic\_signal\_quantum\_bridge} & The original finite
1152 projector, recovery, DFT, and equal-square claims are bundled \\
1153 \end{longtable}}
1154
1155 The later source strengthens the specification around these statements.
1156 It proves that the four labels are exactly the coprime residues, that
1157 the coordinate root has no smaller positive order, that the literal
1158 rational and indexed matrices agree, and that the probability
1159 consequences belong to the actual normalized complex state vectors.
1160
1161 The list operations in the original module use explicit finite literal
1162 lists. Their generic helper definitions are not an assertion of
1163 arbitrary-dimensional linear algebra for unsized lists, where zip
1164 operations could truncate. General vector identities in this chapter use
1165 fixed finite index sets, and the later matrix source uses
1166 \texttt{Fin\ 12} for exactly that reason.
1167
Other PDFs for this work
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: dfa61baf4014e2f4ecd8488a7beed31183bbc682fe66825008194f0cf46a3f66