GenericLieLengthFiltration

Abstract

Right-nested words, their length filtration and dimension estimates.

Definition 1.1 (suSet).

$$\forall (n:\mathbb{N})(X:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),X\in \mathrm{suSet}n⟺(\mathrm{Matrix}.\mathrm{conjTranspose}\left(X\right)=-X\wedge \mathrm{Matrix}.\mathrm{trace}X=0)$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.suSet (✓ 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.

The real submodule consists of skew-Hermitian matrices with zero trace.

Definition 1.2 (suLie).

$$\forall (n:\mathbb{N})(X:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),X\in \mathrm{suLie}n⟺X\in \mathrm{suSet}n$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.suLie (✓ std3).

Source. Repository-derived.

Commentary.

The same carrier is a real Lie subalgebra with the matrix commutator.

Definition 1.3 (layer).

$$\begin{array}{r}\forall (n:\mathbb{N})(S:\mathrm{Finset}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{layer}S0=\mathrm{Bot}.\mathrm{bot}\\ \forall (n:\mathbb{N})(S:\mathrm{Finset}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{layer}S1=\mathrm{Submodule}.\mathrm{span}\mathbb{R}(S:\mathrm{Set}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))\\ \forall (nk:\mathbb{N})(S:\mathrm{Finset}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{layer}S(k+2)=\mathrm{Submodule}.\mathrm{span}\mathbb{R}\{Z:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}\mid \exists (X:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),X\in S\wedge \exists (Y:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),Y\in \mathrm{layer}S(k+1)\wedge Z=[X,Y]\}\end{array}$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.layer (✓ 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.

Definition 3 (arXiv:2301.08241v3, p. 17) defines the layers by “U₁ = span{U}; Uₙ = span[U,Uₙ₋₁], n ≥ 2.” The zero layer is bottom, and the positive layers have exactly the source recurrence.

Definition 1.4 (lieLength).

$$\forall (n:\mathbb{N})(S:\mathrm{Finset}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{lieLength}nS=\mathrm{sInf}\{l:\mathbb{N}\mid 1\le l\wedge ({\mathrm{iSup}}_{k:\mathbb{N}\in \mathrm{Finset}.\mathrm{Icc}1l}\mathrm{layer}Sk)=\mathrm{suSet}n\}$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.lieLength (✓ 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.

Definition 3 (arXiv:2301.08241v3, p. 17): “The Lie-length of a Lie-generating system U of a finite-dimensional Lie-algebra A is the minimal length of the (right-nested) brackets such that the brackets span the whole Lie-algebra, namely Lieℓ(U)=min{ℓ | A=span{Uₙ, n≤ℓ}}, where Uₙ is defined as: U₁=span{U}; Uₙ=span[U,Uₙ₋₁], n≥2.” Natural sInf returns zero for an empty set; the asserted bounds apply to samples for which the layers span suSet.

Definition 1.5 (suCoordinateMap).

$$\forall (gn:\mathbb{N})(x:\mathrm{Fin}g\to \mathrm{Fin}(\mathrm{Module}.\mathrm{finrank}\mathbb{R}(\mathrm{suSet}n))\to \mathbb{R})(j:\mathrm{Fin}g),\mathrm{suCoordinateMap}gnxj=\mathrm{Subtype}.\mathrm{val}((\mathrm{Module}.\mathrm{finBasis}\mathbb{R}(\mathrm{suSet}n)).\mathrm{equivFun}.\mathrm{symm}(xj))$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.suCoordinateMap (✓ std3).

Source. Repository-derived.

Commentary.

Module.finBasis supplies real coordinates for the traceless skew-Hermitian submodule. The map sends each generator coordinate vector through the inverse basis equivalence.

Definition 1.6 (suPairMeasure).

$$\forall (gn:\mathbb{N}),\mathrm{suPairMeasure}gn=\mathrm{MeasureTheory}.\mathrm{Measure}.\mathrm{map}(\mathrm{suCoordinateMap}gn)\mathrm{volume}$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.suPairMeasure (✓ 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.

The measure is the pushforward of real coordinate Lebesgue measure. Matrices use their entries as functions Fin n → Fin n → ℂ. Almost everywhere therefore means outside a Lebesgue null set of generator coordinates.

Definition 1.7 (RightWord).

$$\begin{array}{r}\forall (I:\mathrm{Type}\ast ),\mathrm{RightWord}.\mathrm{single}:I\to \mathrm{RightWord}I\\ \forall (I:\mathrm{Type}\ast ),\mathrm{RightWord}.\mathrm{cons}:I\to \mathrm{RightWord}I\to \mathrm{RightWord}I\end{array}$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.RightWord (✓ std3).

Source. Repository-derived.

Commentary.

RightWord is the inductive type with precisely the single and cons constructors. It represents nonempty right-nested brackets.

Definition 1.8 (rightWordLength).

$$\begin{array}{r}\forall (I:\mathrm{Type}\ast )(i:I),\mathrm{rightWordLength}(\mathrm{RightWord}.\mathrm{single}i)=1\\ \forall (I:\mathrm{Type}\ast )(i:I)(w:\mathrm{RightWord}I),\mathrm{rightWordLength}(\mathrm{RightWord}.\mathrm{cons}iw)=\mathrm{rightWordLength}w+1\end{array}$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightWordLength (✓ std3).

Source. Repository-derived.

Commentary.

Length counts generator letters.

Definition 1.9 (rightWordEval).

$$\begin{array}{r}\forall (IM:\mathrm{Type}\ast )[\mathrm{LieRing}M](S:I\to M)(i:I),\mathrm{rightWordEval}S(\mathrm{RightWord}.\mathrm{single}i)=Si\\ \forall (IM:\mathrm{Type}\ast )[\mathrm{LieRing}M](S:I\to M)(i:I)(w:\mathrm{RightWord}I),\mathrm{rightWordEval}S(\mathrm{RightWord}.\mathrm{cons}iw)=[Si,\mathrm{rightWordEval}Sw]\end{array}$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightWordEval (✓ std3).

Source. Repository-derived.

Commentary.

Evaluation uses the right-nested Lie bracket.

Definition 1.10 (rightSpan).

$$\forall (IKM:\mathrm{Type}\ast )[\mathrm{CommRing}K][\mathrm{LieRing}M][\mathrm{LieAlgebra}KM](S:I\to M)(L:\mathbb{N}),\mathrm{rightSpan}(K:=K)SL=\mathrm{Submodule}.\mathrm{span}K\{x:M\mid \exists (w:\mathrm{RightWord}I),w.\mathrm{rightWordLength}\le L\wedge \mathrm{rightWordEval}Sw=x\}$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightSpan (✓ std3).

Source. Repository-derived.

Commentary.

The submodule is spanned by evaluations of words of length at most L.

Theorem 1.11 (word_mem).

$$\forall (IKM:\mathrm{Type}\ast )[\mathrm{CommRing}K][\mathrm{LieRing}M][\mathrm{LieAlgebra}KM](S:I\to M)(w:\mathrm{RightWord}I)(L:\mathbb{N}),w.\mathrm{rightWordLength}\le L\to \mathrm{rightWordEval}Sw\in \mathrm{rightSpan}(K:=K)SL$$

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

Source. Repository-derived.

Commentary.

Each sufficiently short word belongs to the defining span.

Theorem 1.12 (rightSpan_mono).

$$\forall (IKM:\mathrm{Type}\ast )[\mathrm{CommRing}K][\mathrm{LieRing}M][\mathrm{LieAlgebra}KM](S:I\to M)(ab:\mathbb{N}),a\le b\to \mathrm{rightSpan}(K:=K)Sa\le \mathrm{rightSpan}(K:=K)Sb$$

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

Source. Repository-derived.

Commentary.

Increasing the length cutoff enlarges the span.

Theorem 1.13 (word_bracket_mem).

$$\forall (IKM:\mathrm{Type}\ast )[\mathrm{CommRing}K][\mathrm{LieRing}M][\mathrm{LieAlgebra}KM](S:I\to M)(uv:\mathrm{RightWord}I),[\mathrm{rightWordEval}Su,\mathrm{rightWordEval}Sv]\in \mathrm{rightSpan}(K:=K)S(u.\mathrm{rightWordLength}+v.\mathrm{rightWordLength})$$

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

Source. Repository-derived.

Commentary.

Jacobi induction moves brackets into the right-nested filtration and adds the two lengths.

Theorem 1.14 (rightSpan_bracket_mem).

$$\forall (IKM:\mathrm{Type}\ast )[\mathrm{CommRing}K][\mathrm{LieRing}M][\mathrm{LieAlgebra}KM](S:I\to M)(rt:\mathbb{N})(xy:M),x\in \mathrm{rightSpan}(K:=K)Sr\to y\in \mathrm{rightSpan}(K:=K)St\to [x,y]\in \mathrm{rightSpan}(K:=K)S(r+t)$$

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

Source. Repository-derived.

Commentary.

Bilinearity extends the word estimate to both spans.

Theorem 1.15 (polynomial_ad_mem).

$$\forall (IKM:\mathrm{Type}\ast )[\mathrm{CommRing}K][\mathrm{LieRing}M][\mathrm{LieAlgebra}KM](S:I\to M)(i:I)(L:\mathbb{N})(x:M)(p:\mathrm{Polynomial}K),x\in \mathrm{rightSpan}(K:=K)SL\to \mathrm{Polynomial}.\mathrm{aeval}(\mathrm{LieAlgebra}.\mathrm{ad}KM(Si))px\in \mathrm{rightSpan}(K:=K)S(L+p.\mathrm{natDegree})$$

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

Source. Repository-derived.

Commentary.

A polynomial in the generator adjoint increases the length by at most its natural degree.

Theorem 1.16 (rightSpan_real_le_su).

$$\forall (I:\mathrm{Type}\ast )(n:\mathbb{N})(S:I\to \mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})(L:\mathbb{N}),(\forall (i:I),Si\in \mathrm{suSet}n)\to \mathrm{rightSpan}(K:=\mathbb{R})SL\le \mathrm{suSet}n$$

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

Source. Repository-derived.

Commentary.

Skew-Hermitian trace-zero generators stay in the same submodule under real linear combinations and brackets.

Theorem 1.17 (rightSpan_complex_to_real).

$$\forall (I:\mathrm{Type}\ast )(n:\mathbb{N})(S:I\to \mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})(L:\mathbb{N})(X:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),(\forall (i:I),Si\in \mathrm{suSet}n)\to X\in \mathrm{suSet}n\to X\in \mathrm{rightSpan}(K:=\mathbb{C})SL\to X\in \mathrm{rightSpan}(K:=\mathbb{R})SL$$

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

Source. Repository-derived.

Commentary.

The skew-adjoint projection replaces every complex coefficient by its real part on a skew-Hermitian word. Complex spanning therefore transfers to the real form.

Theorem 1.18 (rightSpan_reindex_le).

$$\forall (IJKM:\mathrm{Type}\ast )[\mathrm{CommRing}K][\mathrm{LieRing}M][\mathrm{LieAlgebra}KM](f:I\to J)(S:I\to M)(T:J\to M)(L:\mathbb{N}),(\forall (i:I),T(fi)=Si)\to \mathrm{rightSpan}(K:=K)SL\le \mathrm{rightSpan}(K:=K)TL$$

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

Source. Repository-derived.

Commentary.

Relabeling generator indices preserves evaluations and word lengths.

Theorem 1.19 (lieLength_le_of_span).

$$\forall (gnL:\mathbb{N})(S:\mathrm{Fin}g\to \mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),1\le L\to \mathrm{rightSpan}(K:=\mathbb{R})SL=\mathrm{suSet}n\to \mathrm{lieLength}n(\mathrm{Finset}.\mathrm{univ}.\mathrm{image}S)\le L$$

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

Source. Repository-derived.

Commentary.

The cumulative source layers equal the bounded-word span, so saturation bounds the source Lie-length.

Definition 1.20 (words).

$$\begin{array}{r}\forall (g:\mathbb{N}),\mathrm{words}g0=\varnothing \\ \forall (gL:\mathbb{N}),\mathrm{words}g(L+1)=\mathrm{Finset}.\mathrm{univ}.\mathrm{image}\mathrm{RightWord}.\mathrm{single}\cup \mathrm{Finset}.\mathrm{univ}.\mathrm{biUnion}(\mathrm{fun}(i:\mathrm{Fin}g)\mapsto (\mathrm{words}gL).\mathrm{image}(\mathrm{RightWord}.\mathrm{cons}i))\end{array}$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.words (✓ std3).

Source. Repository-derived.

Commentary.

The finite enumeration consists of single letters and words formed by prepending a letter.

Definition 1.21 (wordBudget).

$$\begin{array}{r}\forall (g:\mathbb{N}),\mathrm{wordBudget}g0=0\\ \forall (gL:\mathbb{N}),\mathrm{wordBudget}g(L+1)=g+g\ast \mathrm{wordBudget}gL\end{array}$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthFiltration.wordBudget (✓ std3).

Source. Repository-derived.

Commentary.

The recurrence equals the sum of g to powers 1 through L.

Theorem 1.22 (card_words_le).

$$\forall (gL:\mathbb{N}),(\mathrm{words}gL).\mathrm{card}\le \mathrm{wordBudget}gL$$

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

Source. Repository-derived.

Commentary.

Union and image cardinalities bound the number of enumerated words.

Theorem 1.23 (lower_lieLength_of_saturation).

$$\forall (ngL:\mathbb{N})(S:\mathrm{Fin}g\to \mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),2\le n\to 2\le g\to 1\le L\to \mathrm{rightSpan}(K:=\mathbb{R})SL=\mathrm{suSet}n\to (1/\mathrm{Real}.\log ((g:\mathbb{R})+1))\ast \mathrm{Real}.\log (n:\mathbb{R})\le (\mathrm{lieLength}n(\mathrm{Finset}.\mathrm{univ}.\mathrm{image}S):\mathbb{R})$$

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

Source. Repository-derived.

Commentary.

The real dimension n² − 1 cannot exceed the number of words. Bounding the word budget by (g + 1) to the cutoff yields this logarithmic lower bound.

Theorem 1.24 (upper_log).

$$\forall (n:\mathbb{N}),(16\ast (1+\mathrm{Nat}.\log 2(n+1)):\mathbb{R})\le (32/\mathrm{Real}.\log 2)\ast \mathrm{Real}.\log ((n:\mathbb{R})+2)$$

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

Source. Repository-derived.

Commentary.

Nat.log 2 is the integer base-two logarithm. The cast encloses the natural expression on the left; the right-hand logarithm is real.

References

• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.RightWord
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.card_words_le
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.layer
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.lieLength
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.lieLength_le_of_span
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.lower_lieLength_of_saturation
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.polynomial_ad_mem
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightSpan
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightSpan_bracket_mem
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightSpan_complex_to_real
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightSpan_mono
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightSpan_real_le_su
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightSpan_reindex_le
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightWordEval
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.rightWordLength
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.suCoordinateMap
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.suLie
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.suPairMeasure
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.suSet
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.upper_log
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.wordBudget
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.word_bracket_mem
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.word_mem
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthFiltration.words