Exact Matrix Units from a Finite Weyl Pair

Abstract

Finite Fourier combinations of the cyclic window clock and shift form exact matrix units.

Theorem 1.1 (Fourier matrix units are single-entry matrices).

$$E_{ij}=\mathrm{single}(i,j,1)$$

Proof. Machine-checked in Lean as D5/S3/Observer/MatrixUnitCertificate.matrix_unit_eq_single (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every positive window cardinality M and indices i and j in Z/MZ, the Fourier construction E_ij defined below equals the matrix with entry one at (i,j) and zero elsewhere. Character orthogonality gives the diagonal projector, and the shift places its nonzero entry at (i,j).

Theorem 1.2 (Weyl Fourier matrix units multiply exactly).

$$\begin{array}{c}\forall M\in {\mathbb{N}}_{>0},\\ \forall i,j,k,l\in \mathbb{Z}/M\mathbb{Z},\\ E_{ij}:=(\frac{1}{M}\sum _{a\in \mathbb{Z}/M\mathbb{Z}}{\omega }_M^{-ia}{V}_M^a)U_M^{i-j},\\ E_{ij}{E}_{kl}=\{\begin{array}{ll}1,& j=k\\ 0,& j\ne k\end{array}{E}_{il}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/MatrixUnitCertificate.matrix_unit_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

For each positive window cardinality M, Fourier projection of the frozen clock V_M onto address i, followed by the frozen shift U_M^(i-j), defines E_ij. The exponent i-j is forced by the existing entry convention U_M(r,s) = 1 exactly when r-s = 1.

The standard Z/MZ characters enumerate the full finite character group. Exact character orthogonality makes the Fourier projector the single-entry matrix at (i,i), and the shift moves its nonzero column to j. Thus E_ij is exactly the standard single-entry matrix at (i,j).

Consequently E_ij E_kl equals E_il when j=k and is the zero matrix otherwise. This is an identity of complex matrices for every four window indices; it has no residual, norm bound, tolerance, or numerical approximation.

Theorem 1.3 (Diagonal matrix units resolve the identity).

$$\forall M\in {\mathbb{N}}_{>0},\sum _{i\in \mathbb{Z}/M\mathbb{Z}}{E}_{ii}=I_M.$$

Proof. Machine-checked in Lean as D5/S3/Observer/MatrixUnitCertificate.matrix_units_sum_diagonal (✓ std3). ∎

Source. Repository-derived.

Commentary.

Summing the diagonal Fourier matrix units over every cyclic address gives the identity matrix exactly. This is the finite-window completeness relation for the same Weyl-generated family.

References

• Truth anchor: D5/S3/Observer/MatrixUnitCertificate.matrix_unit_eq_single
• Truth anchor: D5/S3/Observer/MatrixUnitCertificate.matrix_unit_mul
• Truth anchor: D5/S3/Observer/MatrixUnitCertificate.matrix_units_sum_diagonal
• Dependency: D5/S3/Observer/WindowRegister