IsometricCompression

Abstract

A one-step matrix intertwining extends through every finite operator word.

Theorem 1.1 (word intertwines).

Lean statement: D5/S3/Quantum/Reduction/IsometricCompression.word_intertwines

Proof. Machine-checked in Lean as D5/S3/Quantum/Reduction/IsometricCompression.word_intertwines (✓ std3). ∎

Source. Repository-derived.

Commentary.

A one-step matrix intertwining extends through every finite operator word.