A.4 Architecture of the proof
On this page · Permalink · Source line 76
The proof crosses two representations. First, rational coordinates support exact finite calculations. Second, a semantics map transfers those calculations to ordinary complex matrices and vectors.
| Layer | Role |
|---|---|
| Rational tables | Signal, projector entries, filtering, and energies. |
| Exact coordinates | Algebra in the basis \(1,\sqrt3,i,i\sqrt3\). |
| Finite matrices | All entries indexed by \(\operatorname{Fin}(12)\), with exact finite sums. |
| Complex semantics | Preservation of multiplication, adjoint, matrix action, and squared norm. |
| Conventions | Identification of roots and normalization with standard exponentials and square roots. |
| Publication theorem | Bundling of the actual complex identities and reconstruction obstructions. |
The active import chain is QuantumArithmeticBridge into FiniteFourier, then SemanticBridge, then Conventions, then Publication. Supporting Mathlib imports enter at the layer that uses them. There is no circular theorem dependency.