A.14 Manuscript-to-Lean concordance
On this page · Permalink · Source line 734
The main paper labels its results QA01 through QA20. The table below distinguishes the exact fixed-example formal coverage from the more general mathematical development. “Not formalized here” is a scope label, not a claim that the prose result is false.
| Claim | Subject | Formal coverage |
|---|---|---|
| QA01 | Primitive root | Exact order 12 and standard exponential root. |
| QA02 | Character orthogonality | Fixed-example content through both exact unitary identities; general theorem not separately exported. |
| QA03 | Fourier theory | Both ordinary complex unitary identities and standard entry formula; general Parseval theorem not separately exported. |
| QA04 | Möbius formula | General modulus formula not formalized; exact integer table for 12 certified. |
| QA05 | Ramanujan support | Exact signed and unsigned twelve-frequency DFT tables and arithmetic energy 48. |
| QA06 | Divisor projectors | Primitive-order projector at 12 certified; the full divisor family not a general Lean family. |
| QA07 | Projector geometry | Hermitian idempotence, displayed energies, explicit noninjectivity, and all-vector residual reconstruction. |
| QA08 | Residue recombination | No theorem in this checkpoint. |
| QA09 | Polyphase aliasing | No theorem in this checkpoint. |
| QA10 | Arithmetic example | Phase sum connected to the exact rational sample table. |
| QA11 | Exact filtering | Displayed contaminated signal and orthogonal energy decomposition. |
| QA12 | State preparation | Ordinary complex normalized vector actions and recovery. |
| QA13 | Shared histogram | Entrywise probability equality and state orthogonality. |
| QA14 | Phase separation | Actual transformed coprime probabilities 1 versus 0. |
| QA15 | Reconstruction barrier | No vector-valued initial-histogram inverse works on both specified states; the global-phase corollary is prose only. |
| QA16 | Measurement law | Relevant projector algebra and state probabilities; no general conditional-state-update API. |
| QA17 | Arithmetic semantics | Soundness for scalar, matrix, vector, adjoint, and mass operations. |
| QA18 | Central bridge | Publication bundle plus separately exported filter, energy, normalization, projector-action, and noninjectivity results. |
| QA19 | Relative-phase family | Prose extension \(\sin^2(\theta/2)\); not an inherited Lean theorem. |
| QA20 | Dephased probability | Prose density-matrix calculation \(1/3\); not an inherited Lean theorem. |
The machine concordance includes all theorem statements verbatim, per-theorem axiom records, source hashes, and exact physical line locators. Its mapping records formal scope; it does not upgrade general manuscript claims merely because a nearby finite special case is checked.