Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Complex Hadamard Relative Gram Cocycle

Abstract

Relative Grams of finite complex Hadamards form a scaled transition cocycle.

Theorem 1.1 (Relative Gram reflexivity).

Lean statement: D5/S3/Quantum/Tomography/MUB/ComplexHadamardRelativeGramCocycle.relativeGram_refl

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/MUB/ComplexHadamardRelativeGramCocycle.relativeGram_refl (✓ std3). ∎

Source. Repository-derived.

Commentary.

The relative Gram of a complex Hadamard with itself is cardinality times the identity.

Theorem 1.2 (Relative Gram reversal).

Lean statement: D5/S3/Quantum/Tomography/MUB/ComplexHadamardRelativeGramCocycle.relativeGram_reverse

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/MUB/ComplexHadamardRelativeGramCocycle.relativeGram_reverse (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reversing a relative transition gives its conjugate transpose.

Theorem 1.3 (Relative Gram cocycle).

Lean statement: D5/S3/Quantum/Tomography/MUB/ComplexHadamardRelativeGramCocycle.relativeGram_cocycle

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/MUB/ComplexHadamardRelativeGramCocycle.relativeGram_cocycle (✓ std3). ∎

Source. Repository-derived.

Commentary.

Relative Grams compose with the finite cardinality scaling law.

Theorem 1.4 (Hadamard triangle composition).

Lean statement: D5/S3/Quantum/Tomography/MUB/ComplexHadamardRelativeGramCocycle.relativeGram_triangle

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/MUB/ComplexHadamardRelativeGramCocycle.relativeGram_triangle (✓ std3). ∎

Source. Repository-derived.

Commentary.

Three pairwise relative Grams satisfy every cyclic composition law.

Theorem 1.5 (Four-MUB relative Gram edges).

Lean statement: D5/S3/Quantum/Tomography/MUB/ComplexHadamardRelativeGramCocycle.fourMUBWitness_relativeGram_edges

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/MUB/ComplexHadamardRelativeGramCocycle.fourMUBWitness_relativeGram_edges (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every off-diagonal edge of a normalized four-MUB witness is a scaled complex Hadamard and obeys the cocycle law.

References