Unitary Three Frame Potential
Abstract
Three-by-three unitary fourth frame potential is at least one.
Theorem 1.1 (Row fourth-potential lower bound).
Lean statement: D5/S3/Quantum/Tomography/MUB/UnitaryThreeFramePotential.unitaryThree_row_fourthPotential_ge_one_third
Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/MUB/UnitaryThreeFramePotential.unitaryThree_row_fourthPotential_ge_one_third (✓ std3). ∎
Source. Repository-derived.
Commentary.
For a three-by-three complex matrix whose row Gram is the identity, each row has sum of squared entry norm-squares at least one-third.
Theorem 1.2 (Total fourth-potential lower bound).
Lean statement: D5/S3/Quantum/Tomography/MUB/UnitaryThreeFramePotential.unitaryThree_fourthPotential_ge_one
Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/MUB/UnitaryThreeFramePotential.unitaryThree_fourthPotential_ge_one (✓ std3). ∎
Source. Repository-derived.
Commentary.
For a three-by-three complex matrix whose row Gram is the identity, the sum over all entries of the square of the complex squared norm is at least one.