Scaled orthogonal columns extend to a square scaled unitary matrix

Proved

Matrix.exists_scaled_orthogonal_completion

by puno · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

linear-algebramutually-unbiased-basesorthonormal-basesunitary-matrices

Let $n\geq0$ be an integer, let $a>0$ be real, and let $A$ be a complex matrix with $n+1$ rows and $n$ columns. If the columns of $A$ are orthogonal and have common squared length $a$ , then they extend to a square matrix with the same column Gram scale:

A^\dagger A=aI_n \quad\Longrightarrow\quad \exists H\in\mathbb C^{(n+1)\times(n+1)}: \quad H^\dagger H=aI_{n+1},\qquad H_{ij}=A_{ij}\quad(0\leq i<n+1,\ 0\leq j<n).

Every prescribed column is preserved at its original index. The new column has squared length $a$ and is orthogonal to all prescribed columns. The statement asserts existence; it does not assert uniqueness or specify the phase of the new column. For $n=0$ there are no prescribed columns, and the conclusion is the existence of a one-by-one matrix with squared column length $a$ .

This completion lemma converts partial orthogonal bases into full bases. With $n=5$ and $a=6$ , it reconstructs a sixth column for each rectangular matrix used in the dimension-six MUB frontier.

Formalization Note. The first $n$ columns of the completion are indexed by Fin.castSucc. This is the positive-scale matrix version of the orthonormal-basis completion discussed in the source; the source's normalized convention corresponds to $a=1$ .

Preamble

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.LinearAlgebra.Matrix.ConjTranspose
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.NormNum

open Matrix
open scoped ComplexConjugate Matrix

Formal statement

theorem Matrix.exists_scaled_orthogonal_completion (n : ℕ) (a : ℝ) (ha : 0 < a)
    (A : Matrix (Fin (n + 1)) (Fin n) ℂ)
    (hA : Aᴴ * A = (a : ℂ) • (1 : Matrix (Fin n) (Fin n) ℂ)) :
    ∃ H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ,
      Hᴴ * H = (a : ℂ) • (1 : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) ∧
      ∀ i j, H i j.castSucc = A i j := by sorry

Source

Brierley and Weigert, Maximal Sets of Mutually Unbiased Quantum States in Dimension Six, arXiv:0808.1614v1, Section 2.1, paragraph immediately before equation (3), https://arxiv.org/html/0808.1614#S2.SS1; published as Phys. Rev. A 78, 042312 (2008), Section II.A, https://doi.org/10.1103/PhysRevA.78.042312. The stated lemma is the positive-scale matrix version of orthonormal-basis completion; it does not include a uniqueness assertion. Mathlib formal tool: Orthonormal.exists_orthonormalBasis_extension_of_card_eq in Analysis/InnerProductSpace/PiL2.lean at revision c5ea00351c28e24afc9f0f84379aa41082b1188f.

View graph