A scaled unitary matrix is flat if its leading codimension-one block is flat

Proved

Matrix.normSq_eq_of_scaled_unitary_core

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

complex-hadamard-matriceslinear-algebramutually-unbiased-basesunitary-matrices

Let $d\geq1$ be an integer, let $a>0$ be real, and let $M$ be a complex square matrix of order $d$ . Suppose that its column Gram matrix is a scalar identity and that every entry of its leading block of order $d-1$ has squared modulus $a$ :

M^\dagger M=daI_d, \qquad |M_{ij}|^2=a\quad(0\leq i,j<d-1).

Then every entry of the entire matrix has squared modulus $a$ :

|M_{ij}|^2=a\quad(0\leq i,j<d).

This is a reusable completion statement for scaled unitary and Hadamard matrices. In the order-six MUB problem it removes the final row and column of entry-modulus equations from both individual matrices and cross-Gram matrices. For $d=1$ the block hypothesis is empty, and the conclusion still holds.

Formalization Note. The Lean parameter is $n=d-1$ . The coefficient $a$ is strictly positive, all entries are arbitrary complex numbers, and only the column Gram identity is assumed. The corresponding row Gram identity is a consequence for square matrices. This border-completion lemma is an algebraic consequence of the cited normalization identities, rather than a verbatim theorem in the source.

Preamble

import Mathlib.LinearAlgebra.Matrix.ConjTranspose
import Mathlib.LinearAlgebra.Matrix.SemiringInverse
import Mathlib.Data.Complex.BigOperators
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum

open Matrix
open scoped BigOperators ComplexConjugate Matrix

Formal statement

theorem Matrix.normSq_eq_of_scaled_unitary_core (n : ℕ) (a : ℝ) (ha : 0 < a)
    (M : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ)
    (hgram : Mᴴ * M = (((n + 1 : ℕ) : ℂ) * (a : ℂ)) •
      (1 : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ))
    (hcore : ∀ i j : Fin n, Complex.normSq (M i.castSucc j.castSucc) = a) :
    ∀ i j, Complex.normSq (M i j) = a := by sorry

Source

Durt, Englert, Bengtsson and Zyczkowski, On mutually unbiased bases, arXiv:1004.3348v2, Section 1.1.1, equations (1.1)-(1.2) and the normalization paragraph immediately after (1.1), https://arxiv.org/html/1004.3348#S1.SS1.SSS1; the scaled Hadamard convention is equation (5.5). The submitted border-completion statement is an explicitly derived algebraic consequence, proved in the accompanying solution, not a theorem quoted verbatim from the review.

View graph