The Lie-algebraic loss-variance formula (Ragone et al. 2023): foundations

This module builds, in staged milestones, toward a genuine formalization of the loss-gradient variance law of Ragone et al. (2023), A Lie algebraic theory of barren plateaus (arXiv:2309.09342): Var_θ[ℓ] = P_g(ρ) · P_g(O) / dim(g) for a simple dynamical Lie algebra g (and the per-component sum for the reductive case). The deep analytic / representation- theoretic inputs that are genuine Mathlib gaps (a normalized Haar measure on the dynamical Lie group; the twirl-is-a-projector property; Schur's lemma for Lie modules / (g⊗g)^G one-dimensional) are isolated as named hypotheses, while everything downstream of them — the entire algebraic / Hilbert–Schmidt derivation of the closed form — is machine-checked.

Phase 1 (this file, growing):

• *-closedness — when the circuit generators are skew-Hermitian (star A = -A, i.e. A = i H), the dynamical Lie algebra is closed under the adjoint star = (·)ᴴ. This is what makes the Hilbert–Schmidt orthogonal complement / Hermitian basis behave, and underlies the reductive (g ⊆ u(N)) structure of the DLA.
• (next) the Hermitian Hilbert–Schmidt orthonormal basis of the DLA, the quadratic Casimir, the g-purity, and the contraction identities (⟪C,C⟫ = dim g, ⟪C, H⊗H⟫ = P_g(H)).

theorem QuantumAlg.dynamicalLieAlgebra_star_mem {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (hskew : ∀ A ∈ gens, star A = -A) {x : Matrix (Fin N) (Fin N) ℂ} (hx : x ∈ dynamicalLieAlgebra gens) : star x ∈ dynamicalLieAlgebra gens

The dynamical Lie algebra of skew-Hermitian generators is *-closed. If every generator A is skew-Hermitian (star A = -A, the physical case A = i H with H Hermitian), then the adjoint star x = xᴴ of any element of the dynamical Lie algebra is again in it. Hence the DLA is the complexification of a real Lie algebra inside u(N), and admits a Hilbert–Schmidt orthonormal basis of Hermitian matrices.

theorem QuantumAlg.dynamicalLieAlgebra_conjTranspose_mem {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (hskew : ∀ A ∈ gens, A.conjTranspose = -A) {x : Matrix (Fin N) (Fin N) ℂ} (hx : x ∈ dynamicalLieAlgebra gens) : x.conjTranspose ∈ dynamicalLieAlgebra gens

Restated with the conjugate-transpose notation: the DLA of skew-Hermitian generators is closed under (·)ᴴ.

A Hermitian orthonormal basis of the DLA; the Casimir and the g-purity

structure QuantumAlg.DLAHermBasis {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) : Type

A Hermitian Hilbert–Schmidt orthonormal basis of the dynamical Lie algebra: the data underlying the quadratic Casimir and the g-purity in Ragone et al. (2023). Such a basis exists whenever the generators are skew-Hermitian (the DLA is then *-closed, see dynamicalLieAlgebra_star_mem); existence is established separately.

• dim : ℕ

  The number of basis elements (= dim g).

• B : Fin self.dim → Matrix (Fin N) (Fin N) ℂ

  The basis vectors.

• herm (j : Fin self.dim) : (self.B j).conjTranspose = self.B j

  Each basis vector is Hermitian (lies in ig).

• ortho (i j : Fin self.dim) : hsInner (self.B i) (self.B j) = if i = j then 1 else 0

  The basis is Hilbert–Schmidt orthonormal.

• span_eq : Submodule.span ℂ (Set.range self.B) = (dynamicalLieAlgebra gens).toSubmodule

  The basis spans the dynamical Lie algebra.

theorem QuantumAlg.DLAHermBasis.trace_mul {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) (i k : Fin b.dim) : (b.B i * b.B k).trace = if i = k then 1 else 0

For a Hermitian orthonormal basis, Tr[Bᵢ Bₖ] = δᵢₖ.

theorem QuantumAlg.DLAHermBasis.linearIndependent_B {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) : LinearIndependent ℂ b.B

An orthonormal family is linearly independent.

theorem QuantumAlg.DLAHermBasis.dlaDim_eq {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) : dlaDim gens = b.dim

The basis cardinality is the dimension of the dynamical Lie algebra.

noncomputable def QuantumAlg.DLAHermBasis.casimir {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) : Matrix (Fin N × Fin N) (Fin N × Fin N) ℂ

The quadratic Casimir C = Σⱼ Bⱼ ⊗ Bⱼ (as a Kronecker product).

Equations

• b.casimir = ∑ j : Fin b.dim, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (b.B j) (b.B j)

noncomputable def QuantumAlg.DLAHermBasis.gProj {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) (H : Matrix (Fin N) (Fin N) ℂ) : Matrix (Fin N) (Fin N) ℂ

The orthogonal projection of H onto the dynamical Lie algebra, H_g = Σⱼ ⟪Bⱼ,H⟫ Bⱼ.

Equations

• b.gProj H = ∑ j : Fin b.dim, QuantumAlg.hsInner (b.B j) H • b.B j

noncomputable def QuantumAlg.DLAHermBasis.gPurity {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) (H : Matrix (Fin N) (Fin N) ℂ) : ℂ

The g-purity P_g(H) = Σⱼ ⟪Bⱼ,H⟫² (Ragone et al. 2023, Eq. (6); equal to Tr[H_g²], see gPurity_eq_trace).

Equations

• b.gPurity H = ∑ i : Fin b.dim, QuantumAlg.hsInner (b.B i) H ^ 2

theorem QuantumAlg.DLAHermBasis.casimir_hsInner_self {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) : hsInner b.casimir b.casimir = ↑b.dim

Step 9a (normalization). ⟪C, C⟫ = dim g — the 1/dim(g) factor.

theorem QuantumAlg.DLAHermBasis.casimir_hsInner_kron {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) (H : Matrix (Fin N) (Fin N) ℂ) : hsInner b.casimir (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) H H) = b.gPurity H

Step 9b (contraction). ⟪C, H ⊗ H⟫ = P_g(H) — the Casimir contracts to the g-purity.

theorem QuantumAlg.DLAHermBasis.gPurity_eq_trace {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) (H : Matrix (Fin N) (Fin N) ℂ) : b.gPurity H = (b.gProj H * b.gProj H).trace

The g-purity coincides with Ragone's Tr[H_g²] (H_g = gProj H).

theorem QuantumAlg.DLAHermBasis.casimir_isHermitian {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) : b.casimir.conjTranspose = b.casimir

The quadratic Casimir is Hermitian.

theorem QuantumAlg.DLAHermBasis.gPurity_conj {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.conjTranspose = H) : (starRingEnd ℂ) (b.gPurity H) = b.gPurity H

The g-purity of a Hermitian matrix is real.

theorem QuantumAlg.DLAHermBasis.gPurity_basis_elem {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) (i : Fin b.dim) : b.gPurity (b.B i) = 1

The g-purity of a basis element is 1 (it is normalized).

The variance formula (simple-DLA case) from the Haar second-moment hypotheses

The deep analytic / representation-theoretic facts that are genuine Mathlib gaps — a normalized Haar measure on the dynamical Lie group, the twirl-is-a-projector property (Steps 3–4), the vanishing of the mean for a simple algebra (Step 5), and the one-dimensionality of (g⊗g)^G (Step 7, Schur) — are bundled into the hypothesis structure below. The closed-form value is then genuinely derived from the proved Steps 9a/9b. The existence of the Hermitian orthonormal basis DLAHermBasis (for skew-Hermitian generators the DLA is *-closed by dynamicalLieAlgebra_star_mem, hence the complexification of its Hermitian real form V_h = V ∩ selfAdjoint with V = V_h ⊕ i·V_h; a Frobenius-orthonormal basis of V_h is a Hermitian orthonormal ℂ-basis of V) is a standard finite-dimensional linear-algebra fact, taken here as input — it is not a deep gap like Haar/Schur.

structure QuantumAlg.RagoneSecondMoment {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (b : DLAHermBasis gens) (ρ O : Matrix (Fin N) (Fin N) ℂ) : Type

Bundled Haar / representation-theoretic input (Ragone et al. 2023, Steps 2–7), simple-DLA case: the loss variance is the Hilbert–Schmidt pairing of ρ⊗ρ with the second-moment operator M²(O⊗O), and the latter is the orthogonal projection of O⊗O onto the one-dimensional G-invariant space span{C} (the quadratic Casimir).

• variance : ℝ

  The loss-gradient variance.

• secondMoment : Matrix (Fin N × Fin N) (Fin N × Fin N) ℂ

  The second-moment (twirl) operator evaluated at O ⊗ O.

• var_eq : ↑self.variance = hsInner (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρ ρ) self.secondMoment

  Step 2 (Haar second moment): Var = ⟪ρ⊗ρ, M²(O⊗O)⟫.

• proj_mem : ∃ (κ : ℂ), self.secondMoment = κ • b.casimir

  Steps 4–7: M²(O⊗O) lies in the one-dimensional invariant space span{C}.

• proj_orth : hsInner b.casimir (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) O O) = hsInner b.casimir self.secondMoment

  Step 4 (orthogonal projection): residual ⊥ C, i.e. ⟪C,O⊗O⟫ = ⟪C,M²(O⊗O)⟫.

theorem QuantumAlg.RagoneSecondMoment.variance_eq_gPurity {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} {b : DLAHermBasis gens} {ρ O : Matrix (Fin N) (Fin N) ℂ} (M : RagoneSecondMoment b ρ O) (hρ : ρ.conjTranspose = ρ) (hdim : 0 < b.dim) : ↑M.variance = b.gPurity ρ * b.gPurity O / ↑b.dim

The Lie-algebraic loss-variance formula (simple-DLA case) — Ragone et al. (2023), the k=1 case. Given the bundled Haar/twirl/Schur hypotheses and Hermitian ρ, O, the loss variance is P_g(ρ) · P_g(O) / dim(g). Genuinely derived from the proved Casimir identities (Steps 9a/9b); only the RagoneSecondMoment data is assumed.

noncomputable def QuantumAlg.RagoneSecondMoment.ofHermitian {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} {b : DLAHermBasis gens} {ρ O : Matrix (Fin N) (Fin N) ℂ} (hρ : ρ.conjTranspose = ρ) (hO : O.conjTranspose = O) (hdim : 0 < b.dim) : RagoneSecondMoment b ρ O

Non-vacuity: the bundle is satisfiable. For any Hermitian orthonormal basis b of a (nonzero-dimensional) dynamical Lie algebra and any Hermitian state ρ and observable O, the RagoneSecondMoment hypotheses are simultaneously satisfiable — witnessed by the rank-one second moment (P_g(O)/dim) • C. This shows the assumption bundle is internally consistent, so variance_eq_gPurity is not vacuously true. (It exhibits that the constraints are consistent; it does not construct the physical Haar twirl, which remains the Mathlib gap.)

Equations

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

Reductive case: sum over the simple ideals

structure QuantumAlg.RagoneReductive {N : ℕ} (ρ O : Matrix (Fin N) (Fin N) ℂ) : Type

Reductive-case input (Ragone et al. 2023, Prop. 1 / Step 0): a finite family of simple components, each with its second-moment bundle, plus the independence assumption that the total loss variance is the sum of the per-component variances.

• numComp : ℕ

  Number of simple ideals.

• gens : Fin self.numComp → Set (Matrix (Fin N) (Fin N) ℂ)

  Generators of each simple ideal.

• basis (j : Fin self.numComp) : DLAHermBasis (self.gens j)

  A Hermitian orthonormal basis of each ideal.

• comp (j : Fin self.numComp) : RagoneSecondMoment (self.basis j) ρ O

  The second-moment bundle of each simple component.

• totalVariance : ℝ

  Total loss variance.

• total_eq : ↑self.totalVariance = ∑ j : Fin self.numComp, ↑(self.comp j).variance

  Independence: total variance is the sum of the per-component variances.

theorem QuantumAlg.RagoneReductive.totalVariance_eq {N : ℕ} {ρ O : Matrix (Fin N) (Fin N) ℂ} (R : RagoneReductive ρ O) (hρ : ρ.conjTranspose = ρ) (hdim : ∀ (j : Fin R.numComp), 0 < (R.basis j).dim) : ↑R.totalVariance = ∑ j : Fin R.numComp, (R.basis j).gPurity ρ * (R.basis j).gPurity O / ↑(R.basis j).dim

Reductive-case variance formula. The total loss variance is the sum over the simple ideals of P_{gⱼ}(ρ) · P_{gⱼ}(O) / dim(gⱼ).

Capstone: exponentially large DLA ⟹ barren plateau (genuine variance)

theorem QuantumAlg.ragone_hasBarrenPlateau {sz : ℕ → ℕ} {gens : (n : ℕ) → Set (Matrix (Fin (sz n)) (Fin (sz n)) ℂ)} {ρ O : (n : ℕ) → Matrix (Fin (sz n)) (Fin (sz n)) ℂ} {b : (n : ℕ) → DLAHermBasis (gens n)} (M : (n : ℕ) → RagoneSecondMoment (b n) (ρ n) (O n)) (hρ : ∀ (n : ℕ), (ρ n).conjTranspose = ρ n) (hdimpos : ∀ (n : ℕ), 0 < (b n).dim) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (n : ℕ), ‖(b n).gPurity (ρ n) * (b n).gPurity (O n)‖ ≤ C) {base : ℝ} (hbase : 1 < base) (hexp : ∀ (n : ℕ), base ^ n ≤ ↑(b n).dim) : HasBarrenPlateau fun (n : ℕ) => (M n).variance

Capstone — the full chain circuit ⟹ DLA ⟹ dimension ⟹ variance ⟹ barren plateau. For a qubit-indexed family of simple-DLA circuits whose loss variance is the genuine Ragone value P_g(ρ)·P_g(O)/dim(g) (the RagoneSecondMoment bundle), if the g-purity numerator stays bounded and the dynamical Lie algebra dimension grows exponentially in the qubit count, then the loss has a barren plateau. This consumes the proved variance formula (variance_eq_gPurity) rather than an assumed variance law.

A concrete witness: the hypotheses are inhabited

def QuantumAlg.trivialDLAHermBasis : DLAHermBasis {1}

A concrete one-dimensional DLAHermBasis: the dynamical Lie algebra generated by the identity, with the (already normalized) identity as its single Hermitian orthonormal basis vector. Witnesses that the geometric hypotheses are inhabitable.

Equations

• QuantumAlg.trivialDLAHermBasis = { dim := 1, B := fun (x : Fin 1) => 1, herm := QuantumAlg.trivialDLAHermBasis._proof_3, ortho := ⋯, span_eq := QuantumAlg.trivialDLAHermBasis._proof_2 }

theorem QuantumAlg.ragone_hypotheses_nonempty : ∃ (gens : Set (Matrix (Fin 1) (Fin 1) ℂ)) (b : DLAHermBasis gens) (ρ : Matrix (Fin 1) (Fin 1) ℂ) (O : Matrix (Fin 1) (Fin 1) ℂ), Nonempty (RagoneSecondMoment b ρ O)

The full hypothesis stack is non-vacuous. There is a concrete dynamical Lie algebra with a Hermitian orthonormal basis and a satisfiable second-moment bundle — so the variance formula variance_eq_gPurity and the barren-plateau capstone are not vacuously true.