Two Circulant X Seed
Abstract
Unit-phase triples with opposite sums yield an order-six Hadamard seed.
Definition 1.1 (Circulant block seed).
Lean statement: D5/S3/Quantum/Tomography/MUB/TwoCirculantXSeed.twoCirculantSeed
Formalization. D5/S3/Quantum/Tomography/MUB/TwoCirculantXSeed.twoCirculantSeed (✓ std3).
Source. Repository-derived.
Commentary.
For complex a,b,c,d, let A be the circulant matrix generated by (a,1,b) and B the one generated by (c,1,d). The order-six seed has block rows (A,B) and (B-adjoint,-A-adjoint).
Theorem 1.2 (Hadamard seed from opposite phase triples).
Lean statement: D5/S3/Quantum/Tomography/MUB/TwoCirculantXSeed.twoCirculantSeed_hadamard_of_opposite_phase_triples
Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/MUB/TwoCirculantXSeed.twoCirculantSeed_hadamard_of_opposite_phase_triples (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let r and s be triples of complex numbers whose entries all have squared norm one. If each triple has product one and their sums add to zero, then twoCirculantSeed evaluated at (r0 r1,r1,s0 s1,s1) is complex Hadamard.