MUB Completion Single Relative Gram

Abstract

A fixed-edge mutually unbiased double completion yields one relative Gram system.

Theorem 1.1 (Single relative Gram system).

Lean statement: D5/S3/Quantum/Tomography/MUB/MUBCompletionSingleRelativeGram.doubleCompletion_yields_singleRelativeGramSystem

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

Source. Repository-derived.

Commentary.

A fixed-edge mutually unbiased double completion yields a scaled-Hadamard relative Gram that recovers both second factors.

Theorem 1.2 (Dimension-six relative Gram system).

Lean statement: D5/S3/Quantum/Tomography/MUB/MUBCompletionSingleRelativeGram.doubleCompletion_yields_singleRelativeGramSystem_six

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

Source. Repository-derived.

Commentary.

The necessary relative-Gram equations specialize to the dimension-six carrier.

References