A.1 What this guide certifies
On this page · Permalink · Source line 1
The completed fixed example is a bridge between exact arithmetic and ordinary complex linear algebra. It certifies a twelve-dimensional Fourier matrix, a Ramanujan projector, two normalized states with the same initial probabilities, and their opposite outcomes after a basis change. This guide maps those claims to actual Lean declarations rather than treating numerical agreement as a proof.
The five-module formal package contains 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.
| Production module | Named theorems |
|---|---|
QuantumArithmeticBridge | 22 |
FiniteFourier | 17 |
SemanticBridge | 30 |
Conventions | 17 |
Publication | 10 |
| Total | 96 |
These counts include supporting lemmas. They count named source declarations, not new discoveries, compiler jobs, or declarations generated internally by Lean. The namespace is Komorebi.QuantumArithmetic throughout.