GenericLieLength

Abstract

Generic Lie-length in the traceless skew-Hermitian matrix Lie algebra grows logarithmically for every fixed generator count at least two.

Theorem 1.1 (ae_mvPolynomial_ne_zero).

$$\forall (n:\mathbb{N})(p:\mathrm{MvPolynomial}(\mathrm{Fin}n)\mathbb{R}),p\ne 0\to {\forall }^m(x:\mathrm{Fin}n\to \mathbb{R}),\mathrm{MvPolynomial}.\mathrm{eval}xp\ne 0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/GenericLieLength.ae_mvPolynomial_ne_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

A nonzero real multivariate polynomial vanishes only on a Lebesgue null set. AnalyticOnNhd.eval_mvPolynomial gives analyticity, MvPolynomial.funext supplies a nonzero value, and AnalyticZeroSetNull.ae_ne_zero_of_analytic gives nonvanishing almost everywhere.

Theorem 1.2 (ae_span_top_of_witness).

$$\forall (M:\mathrm{Type}\ast )[\mathrm{LieRing}M][\mathrm{LieAlgebra}\mathbb{R}M][\mathrm{FiniteDimensional}\mathbb{R}M](gdL:\mathbb{N})(b:\mathrm{Module}.\mathrm{Basis}(\mathrm{Fin}d)\mathbb{R}M)(S0:\mathrm{Fin}g\to M),\mathrm{rightSpan}(K:=\mathbb{R})S0L=\mathrm{Top}.\mathrm{top}\to {\forall }^m(x:\mathrm{Fin}g\to \mathrm{Fin}d\to \mathbb{R}),\mathrm{rightSpan}(K:=\mathbb{R})(\mathrm{fun}(i:\mathrm{Fin}g)\mapsto b.\mathrm{equivFun}.\mathrm{symm}(xi))L=\mathrm{Top}.\mathrm{top}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/GenericLieLength.ae_span_top_of_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

One spanning tuple supplies coefficients for a determinant polynomial which evaluates to one. Its nonzero evaluations give full span for almost all tuples of real basis coordinates.

Definition 1.3 (claim).

$$\mathrm{claim}⟺(\forall (g:\mathbb{N}),2\le g\to \exists (cC:\mathbb{R}),0<c\wedge 0<C\wedge \forall (n:\mathbb{N}),2\le n\to \mathrm{Filter}.\mathrm{Eventually}(\mathrm{fun}(S:\mathrm{Fin}g\to \mathrm{Fin}n\to \mathrm{Fin}n\to \mathbb{C})\mapsto (c\ast \mathrm{Real}.\log (n:\mathbb{R})\le (\mathrm{lieLength}n(\mathrm{Finset}.\mathrm{univ}.\mathrm{image}S):\mathbb{R})\wedge (\mathrm{lieLength}n(\mathrm{Finset}.\mathrm{univ}.\mathrm{image}S):\mathbb{R})\le C\ast \mathrm{Real}.\log (n:\mathbb{R})))(\mathrm{MeasureTheory}.\mathrm{ae}(\mathrm{suPairMeasure}gn)))$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLength.claim (✓ std3).

Citation. Yifan Jia; Angela Capel (2024). A generic quantum Wielandt’s inequality. DOI: 10.22331/q-2024-05-02-1331. URL: https://arxiv.org/abs/2301.08241.

Commentary.

Conjecture 6 (arXiv:2301.08241v3, p. 19): “Let S be a random Lie-generating set of su(n), then Lieℓ(S) = Θ(log n) almost surely.” The number g of generators is fixed, with g ≥ 2, and the positive real constants depend on g but not on n ≥ 2. Lie-length counts generator letters in right-nested brackets and cumulative layers. Filter.Eventually under suPairMeasure gives the source almost-sure qualifier.

Theorem 1.4 (result).

$$\mathrm{claim}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/GenericLieLength.result (✓ std3). ∎

Resolves. Problems/jia-capel-2023-generic-lie-length (proved) by D5/S3/Quantum/Algebra/GenericLieLength.result.

Source. Repository-derived.

Acknowledgement. Yifan Jia; Angela Capel (2024). A generic quantum Wielandt’s inequality. DOI: 10.22331/q-2024-05-02-1331. URL: https://arxiv.org/abs/2301.08241.

Acknowledgement. Seth Lloyd; Reevu Maity (2019). Efficient implementation of unitary transformations. DOI: 10.48550/arXiv.1901.03431. URL: https://arxiv.org/abs/1901.03431.

Commentary.

For each fixed g ≥ 2 the constants c = 1/log(g + 1) and C = 32/log 2 work. The anchored heap produces a spanning pair in 16(1 + Nat.log 2 (n − 1)) letters; the determinant argument gives the same bound almost everywhere. The word-count dimension bound gives the lower estimate. The optimal upper constant and Lloyd–Maity Conjecture III remain open.

References

• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLength.ae_mvPolynomial_ne_zero
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLength.ae_span_top_of_witness
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLength.claim
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLength.result
• Dependency: D5/S3/Analytic/NullSets/AnalyticZeroSetNull
• Dependency: D5/S3/Quantum/Algebra/GenericLieLengthConstruction