Lie-algebraic barren plateaus from the real dynamical Lie algebra

The standard logic of a Lie-algebraic barren-plateau analysis is:

circuit generators ⟹ dynamical Lie algebra g ⟹ decomposition into components g = ⊕ₖ gₖ ⟹ the dimension dim g ⟹ (with the variance law Var ∼ 1 / dim g) the scaling of the variance: exponential or polynomial in the number of qubits.

The earlier LieAlgebraicVariance model (in LeanPool.LeanQuantumAlg.Primitives.Trainability) bundled dim g as an opaque ℕ → ℝ. This module replaces it by the genuine dimension Module.finrank ℂ g of the formalized dynamicalLieAlgebra, and proves:

• dlaDim — the real dimension of the dynamical Lie algebra.
• hasBarrenPlateau_of_exp_dlaDim — if the real dim g grows exponentially in the qubit count then the (Ragone) variance law forces a barren plateau. The variance value numer / dim g (which needs Haar / Weingarten averaging) is the only assumed input; the dimension is real.
• finrank_eq_sum_of_isInternal / dlaDim_eq_sum_of_isInternal — the decomposition step: if g is an internal direct sum of subspaces gₖ then dim g = ∑ₖ dim gₖ.
• Two end-to-end worked examples computing the real dim g and deriving the scaling:
  • dlaDim_univ + barrenPlateau_of_full_dla — the maximal (fully controllable) algebra g = gl(2ⁿ) has dim g = 4ⁿ (exponential) ⟹ barren plateau;
  • dlaDim_singleton + not_barrenPlateau_of_dlaDim_const — a single-generator (commuting) circuit has dim g = 1 (constant) ⟹ no barren plateau (trainable).

The first-principles derivation of the variance law itself (Ragone et al. 2023, Eq. (10), via Weingarten calculus / t-designs) remains a Mathlib gap and is left as an assumed hypothesis throughout; see LeanPool.LeanQuantumAlg.Primitives.Trainability.

Source: Ragone, Bakalov, Sauvage, Kemper, Ortiz Marrero, Larocca, Cerezo (2023), A Lie algebraic theory of barren plateaus (arXiv:2309.09342).

The real dimension of the dynamical Lie algebra

noncomputable def QuantumAlg.dlaDim {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) : ℕ

The dimension of the dynamical Lie algebra of a generator set: the ℂ-finrank of the formalized dynamicalLieAlgebra (a subspace of gl(N, ℂ)). This is the genuine dim g of the Lie-algebraic variance law, not an opaque parameter.

Equations

• QuantumAlg.dlaDim gens = Module.finrank ℂ ↥(QuantumAlg.dynamicalLieAlgebra gens).toSubmodule

Tier 1 — barren plateau from exponential growth of the real dimension

theorem QuantumAlg.hasBarrenPlateau_of_exp_dlaDim {sz : ℕ → ℕ} {gens : (n : ℕ) → Set (Matrix (Fin (sz n)) (Fin (sz n)) ℂ)} {variance : ℕ → ℝ} {numer : ℝ} (hnum : 0 ≤ numer) (hvar : ∀ (n : ℕ), variance n = numer / ↑(dlaDim (gens n))) {b : ℝ} (hb : 1 < b) (hdim : ∀ (n : ℕ), b ^ n ≤ ↑(dlaDim (gens n))) : HasBarrenPlateau variance

Lie-algebraic barren plateau (real dimension). Given the Ragone variance law variance n = numer / dim g_n (the numerator, requiring Haar/Weingarten averaging, is the assumed input), if the real dynamical-Lie-algebra dimension grows at least like bⁿ for some b > 1, then the loss has a barren plateau.

Tier 2 — the decomposition step: dimension is additive over a direct sum

theorem QuantumAlg.finrank_eq_sum_of_isInternal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Type u_2} [AddCommGroup M] [Module ℂ M] [Module.Finite ℂ M] {A : ι → Submodule ℂ M} (h : DirectSum.IsInternal A) : Module.finrank ℂ M = ∑ i : ι, Module.finrank ℂ ↥(A i)

If a finite-dimensional space is the internal direct sum of subspaces A i, its dimension is the sum of theirs. (Linear-algebra core of the Lie-algebra decomposition dim g = ∑ₖ dim gₖ.)

theorem QuantumAlg.dlaDim_eq_sum_of_isInternal {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : ι → Submodule ℂ ↥(dynamicalLieAlgebra gens).toSubmodule} (h : DirectSum.IsInternal A) : dlaDim gens = ∑ i : ι, Module.finrank ℂ ↥(A i)

Decomposition of the dynamical Lie algebra dimension. If the dynamical Lie algebra decomposes as an internal direct sum of subspaces A k (its irreducible / ideal components), then dim g = ∑ₖ dim (A k).

Tier 3a — worked example: full algebra gl(2ⁿ), exponential ⟹ barren plateau

theorem QuantumAlg.dynamicalLieAlgebra_eq_top_of_span_top {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (hspan : Submodule.span ℂ gens = ⊤) : dynamicalLieAlgebra gens = ⊤

A generating set that spans all of gl(N, ℂ) generates the whole algebra: its dynamical Lie algebra is ⊤.

theorem QuantumAlg.dlaDim_univ {N : ℕ} : dlaDim Set.univ = N * N

The dynamical Lie algebra of the full operator set is all of gl(N, ℂ), of dimension N² (maximal / fully controllable case).

theorem QuantumAlg.barrenPlateau_of_full_dla {gens : (n : ℕ) → Set (Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ)} (hfull : ∀ (n : ℕ), Submodule.span ℂ (gens n) = ⊤) {variance : ℕ → ℝ} {numer : ℝ} (hnum : 0 ≤ numer) (hvar : ∀ (n : ℕ), variance n = numer / ↑(dlaDim (gens n))) : HasBarrenPlateau variance

Worked example (exponential ⟹ barren plateau). A fully controllable circuit family on n qubits — whose generators span all of gl(2ⁿ, ℂ), so dim g = 4ⁿ — has a barren plateau under the Ragone variance law.

Tier 3b — worked example: single generator, constant ⟹ no barren plateau

theorem QuantumAlg.dlaDim_singleton {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H ≠ 0) : dlaDim {H} = 1

A single-generator circuit has a one-dimensional dynamical Lie algebra (the generator commutes with itself, so the Lie closure is just its span).

Tier 3c — worked example: commuting family, dimension grows linearly in n

theorem QuantumAlg.dlaDim_diagonalFamily (n : ℕ) : dlaDim (Set.range fun (i : Fin n) => Matrix.diagonal (Pi.single i 1)) = n

The n diagonal unit matrices diag(eᵢ) pairwise commute and are linearly independent, so their dynamical Lie algebra is the n-dimensional diagonal subalgebra: dim g = n. This is a worked example of a dynamical Lie algebra whose dimension grows polynomially (linearly) in the size parameter n — the trainable regime, in contrast to the exponential gl(2ⁿ) case.

theorem QuantumAlg.not_barrenPlateau_of_dlaDim_const {sz : ℕ → ℕ} {H : (n : ℕ) → Matrix (Fin (sz n)) (Fin (sz n)) ℂ} (hH : ∀ (n : ℕ), H n ≠ 0) {variance : ℕ → ℝ} {numer : ℝ} (hnum : 0 < numer) (hvar : ∀ (n : ℕ), variance n = numer / ↑(dlaDim {H n})) : ¬HasBarrenPlateau variance

Worked example (constant ⟹ no barren plateau). A single-generator circuit family — whose dynamical Lie algebra is one-dimensional for every n — is trainable: under the variance law variance = numer / dim g with numer > 0, the variance is the positive constant numer, which does not vanish, so there is no barren plateau.