1.16 What is complete and what remains a separate question
On this page · Permalink · Source line 1419
The finite worked bridge is complete as a mathematical result. Its maps are defined, its identities are proved, its literal coefficients agree across the rational and cyclotomic representations, and its principal modulus-twelve transport and phase claims have formal certificates. The current release provides the traditional paper, visual guide, formal concordance, source, and reproducibility records.
The general prose theorems also establish Fourier unitarity, the Möbius divisor formula, rational divisor-projector completeness, and polyphase aliasing for the declared finite or formal models. Their arbitrary-modulus formulations are not claimed as generic Lean declarations in this package. The continuous phase and dephased-state extensions are proved prose results rather than inherited formal additions. The visual guide illustrates the continuous phase family.
Several broader questions have different proof obligations. Efficient preparation of coprime-support states needs an algorithm and a cost model. Efficient circuit synthesis of the twelve-dimensional transformation or its qubit embedding needs a gate construction and resource bounds. Incomplete-sample recovery needs an observation map that is injective on the declared model, or a stability theorem with stated conditioning. Noisy implementation needs a perturbation analysis. A physical claim needs an experimental protocol and measured data.
These questions can be asked using the same operator language. Their existence does not weaken the exact bridge proved here, and the bridge does not answer them automatically. The present result shows, in one fully specified example, how arithmetic selection becomes rational filtering and phase-sensitive unitary realization while keeping reconstruction, information loss, and measurement distinct.