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 (Clock phase powers are cyclic characters).

$$\forall M\in \mathbb{N}[\mathrm{NeZero}M],\forall r,k\in \mathbb{Z}/M\mathbb{Z},(\mathrm{windowRoot}{\left(M\right)}^{\mathrm{val}\left(r\right)}{)}^{\mathrm{val}\left(k\right)}=\left({\mathrm{character}}_M\right)\left(k,r\right)$$

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

Source. Repository-derived.

Commentary.

For every nonzero window cardinality M and cyclic indices r and k, raising the rth clock phase to the representative of k gives the standard cyclic character with frequency k evaluated at r.

Theorem 1.2 (Entries of every cyclic shift power).

$$\begin{array}{c}\forall M\in \mathbb{N}[\mathrm{NeZero}M],\\ \forall n\in \mathbb{N},\forall r,s\in \mathbb{Z}/M\mathbb{Z},\\ (\mathrm{shiftMatrix}(M{)}^n{)}_{rs}=\{\begin{array}{ll}(1:\mathbb{C}),& r-s=(n:\mathbb{Z}/M\mathbb{Z})\\ (0:\mathbb{C}),& \mathrm{otherwise}\end{array}\end{array}$$

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

Source. Repository-derived.

Commentary.

For every nonzero natural cardinality M, every natural exponent n, and cyclic indices r and s, the (r,s) entry of the nth power of shiftMatrix M is the complex number one exactly when r-s equals the image of n in Z/MZ, and is zero otherwise.

Theorem 1.3 (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.4 (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.5 (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.clock_phase_pow_eq_character
• 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
• Truth anchor: D5/S3/Observer/MatrixUnitCertificate.shift_matrix_pow_apply
• Dependency: D5/S3/Observer/WindowRegister