The full algebra gl(2ⁿ) as a dynamical Lie algebra: an exponential barren plateau

This module constructs the explicit Hermitian Hilbert–Schmidt orthonormal basis of the full matrix algebra gl(N, ℂ) (the Hermitized matrix units: diagonal Eₖₖ, symmetric (Eᵢⱼ+Eⱼᵢ)/√2, antisymmetric i(Eᵢⱼ−Eⱼᵢ)/√2). For N = 2ⁿ this is a DLAHermBasis of the fully controllable circuit (dynamical Lie algebra = gl(2ⁿ), dimension 4ⁿ), which — fed into ragone_hasBarrenPlateau — exhibits a concrete family with an exponentially vanishing loss variance: a genuine barren plateau, witnessing that the capstone is not vacuous on the canonical physical case.

noncomputable def QuantumAlg.rt2inv : ℂ

The real constant 1/√2, as a complex scalar (the off-diagonal normalization).

Equations

• QuantumAlg.rt2inv = ↑(√2)⁻¹

theorem QuantumAlg.rt2inv_mul_self : rt2inv * rt2inv = 1 / 2

theorem QuantumAlg.rt2inv_conj : star rt2inv = rt2inv

noncomputable def QuantumAlg.hermUnit {N : ℕ} (p : Fin N × Fin N) : Matrix (Fin N) (Fin N) ℂ

The Hermitized matrix units: a complete Hermitian basis of gl(N, ℂ), indexed by Fin N × Fin N (diagonal / symmetric-off-diagonal / antisymmetric-off-diagonal).

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumAlg.hermUnit_isHermitian {N : ℕ} (p : Fin N × Fin N) : (hermUnit p).conjTranspose = hermUnit p

Every Hermitized matrix unit is Hermitian.

theorem QuantumAlg.hermUnit_diag {N : ℕ} (i : Fin N) : hermUnit (i, i) = Matrix.single i i 1

theorem QuantumAlg.hermUnit_lt {N : ℕ} {i j : Fin N} (h : i < j) : hermUnit (i, j) = rt2inv • (Matrix.single i j 1 + Matrix.single j i 1)

theorem QuantumAlg.hermUnit_gt {N : ℕ} {i j : Fin N} (h : j < i) : hermUnit (i, j) = rt2inv • Complex.I • (Matrix.single i j 1 - Matrix.single j i 1)

theorem QuantumAlg.rt2inv_sq : rt2inv ^ 2 = 1 / 2

theorem QuantumAlg.star_I_eq : star Complex.I = -Complex.I

theorem QuantumAlg.hermUnit_orthonormal {N : ℕ} (p q : Fin N × Fin N) : hsInner (hermUnit p) (hermUnit q) = if p = q then 1 else 0

The Hermitized matrix units form a Hilbert–Schmidt orthonormal family.

theorem QuantumAlg.hermUnit_linearIndependent {N : ℕ} : LinearIndependent ℂ hermUnit

The Hermitized matrix units are linearly independent.

theorem QuantumAlg.hermUnit_span_top {N : ℕ} : Submodule.span ℂ (Set.range hermUnit) = ⊤

The Hermitized matrix units span all of gl(N, ℂ).

noncomputable def QuantumAlg.fullHermBasis (N : ℕ) : DLAHermBasis Set.univ

The full algebra gl(N, ℂ) as a DLAHermBasis — the dynamical Lie algebra of a fully controllable circuit (generators span everything), with the Hermitized matrix units as its Hermitian orthonormal basis. Its dimension is N².

Equations

• QuantumAlg.fullHermBasis N = { dim := N * N, B := fun (a : Fin (N * N)) => QuantumAlg.hermUnit (finProdFinEquiv.symm a), herm := ⋯, ortho := ⋯, span_eq := ⋯ }

noncomputable def QuantumAlg.fullCtrlSM (n : ℕ) : RagoneSecondMoment (fullHermBasis (2 ^ n)) ((fullHermBasis (2 ^ n)).B ⟨0, ⋯⟩) ((fullHermBasis (2 ^ n)).B ⟨0, ⋯⟩)

The Ragone second-moment bundle for the fully controllable n-qubit family, with observable and state both equal to the first (Hermitian, normalized) basis element.

Equations

• QuantumAlg.fullCtrlSM n = QuantumAlg.RagoneSecondMoment.ofHermitian ⋯ ⋯ ⋯

theorem QuantumAlg.fullControllability_hasBarrenPlateau : HasBarrenPlateau fun (n : ℕ) => (fullCtrlSM n).variance

Concrete exponential barren plateau (full controllability). The qubit-indexed family of fully controllable circuits — dynamical Lie algebra gl(2ⁿ), dimension 4ⁿ — has an exponentially vanishing loss variance: a genuine barren plateau. This instantiates ragone_hasBarrenPlateau on the canonical physical case, witnessing it is not vacuous.