Finite Window Algebra Generation

Abstract

The finite address-reading clock and cyclic address-writing shift generate every observable in their full matrix algebra.

Theorem 1.1 (Window read and write generate the full matrix algebra).

$$\forall M\in {\mathbb{N}}_{>0},{\mathrm{alg}}_{\mathbb{C}}(C_M,S_M)={\mathrm{Mat}}_{\mathbb{Z}/M\mathbb{Z}}(\mathbb{C}).$$

Proof. Machine-checked in Lean as D5/S3/Observer/WindowAlgebra/WindowGeneration.window_generators_adjoin_top (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every nonzero finite cardinality M, the complex subalgebra generated by the frozen address-reading clock and cyclic address-writing shift is the top subalgebra of the full matrix algebra on ZMod M.

The proof first exposes the frozen Fourier construction of each matrix unit through subalgebra closure under powers, scalar multiplication, finite sums, and products. The frozen exact matrix-unit certificate then identifies those generated elements with standard single-entry matrices, and the standard finite matrix-unit expansion supplies every matrix. This is a finite-window statement and does not assert a universal crossed-product identification.

Theorem 1.2 (Generation and prime-power factorization hold together).

$$\forall M\in {\mathbb{N}}_{>0},A_M={\mathrm{Mat}}_{\mathbb{Z}/M\mathbb{Z}}(\mathbb{C})\wedge \mathrm{bijective}(F_M).$$

Proof. Machine-checked in Lean as D5/S3/Observer/WindowAlgebra/WindowGeneration.window_generated_full_matrix_and_prime_power_factors (✓ std3). ∎

Source. Repository-derived.

Commentary.

The generated-algebra equality is paired with the existing canonical prime-power tensor factorization. The conjunction closes both clauses for the same nonzero window cardinality without reproving or weakening the frozen factorization equivalence.

Theorem 1.3 (The two-address window generates a nonzero off-diagonal observable).

$$E_{0,1}\in {\mathrm{alg}}_{\mathbb{C}}(C_2,S_2)\wedge E_{0,1}\ne 0.$$

Proof. Machine-checked in Lean as D5/S3/Observer/WindowAlgebra/WindowGeneration.window_two_off_diagonal_generated_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

At window cardinality two, the standard single-entry matrix in row zero and column one belongs to the generated algebra and is nonzero. This explicitly exhibits an off-diagonal generated observable, so the result is not witnessed by scalars, diagonal matrices, or an empty generator family.

References

• Truth anchor: D5/S3/Observer/WindowAlgebra/WindowGeneration.window_generated_full_matrix_and_prime_power_factors
• Truth anchor: D5/S3/Observer/WindowAlgebra/WindowGeneration.window_generators_adjoin_top
• Truth anchor: D5/S3/Observer/WindowAlgebra/WindowGeneration.window_two_off_diagonal_generated_witness
• Dependency: D5/S3/Observer/MatrixUnitCertificate
• Dependency: D5/S3/ObserverMemory/PrimePowerTensorTower