AriWordOperations

Abstract

Original rational ari letter actions and word support

H is the existing rational concatenation-word algebra on the whole natural alphabet. N denotes the naturals, including zero. All sums are finite, the empty word is 1, and all coefficients and scalar actions are rational. In supportSpace, p ranges over H and w over Word; the set variables in homogeneous and above range over Word. For a word A, length(A) and get(A,i) mean length and get of A.toList. Sum and prod with a Fin domain run over every coordinate. The source presentation is Proposition 4.19 with individual generator factors; it does not use the naive associative extension of Remark 4.16.

Definition 1.1 (The original infinite-alphabet words).

$$Word=\mathrm{FreeMonoid}\left(N\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.Word (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

The empty word is the multiplicative unit, and multiplication is concatenation.

Definition 1.2 (The existing rational word algebra).

$$H=\mathrm{RationalWordPolynomial}\left(N\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.H (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Coefficients are rational and every polynomial has finite word support.

Definition 1.3 (Ordinary word basis).

$$\forall w:Word,\mathrm{wordBasis}\left(w\right)=\mathrm{single}\left(w,1\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.wordBasis (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

The basis has coefficient one, with no divided powers or factorials.

Definition 1.4 (Original generators including zero).

$$\forall s:N,\mathrm{letter}\left(s\right)=\mathrm{wordBasis}\left(\mathrm{of}\left(s\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.letter (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Every natural index is allowed.

Definition 1.5 (Original letter weight).

$$\forall s:N,\mathrm{gamma}\left(s\right)=\mathrm{ifThenElse}\left(s=0,1,s\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.gamma (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

The zero-index letter has weight one.

Definition 1.6 (Additive original weight).

$$\forall w:Word,\mathrm{weight}\left(w\right)=\mathrm{sum}\left(\mathrm{map}\left(gamma,\mathrm{toList}\left(w\right)\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.weight (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

The sum over an empty list is zero.

Definition 1.7 (The full k-level count).

$$\forall k:N,\forall w:Word,\mathrm{level}\left(k,w\right)=\mathrm{countP}\left(\mathrm{lambda}\left(i,i\ne k\right),\mathrm{toList}\left(w\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.level (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

This counts letters different from k, including k equal to zero.

Definition 1.8 (Coordinate support submodule).

$$\forall S:\mathrm{Set}\left(Word\right),\mathrm{supportSpace}\left(S\right)=\mathrm{set}\left(p,\forall w:Word,(\mathrm{coeff}\left(p,w\right)\ne 0)⟹w\in S\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.supportSpace (✓ std3).

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Finite sums and rational cancellation preserve this support restriction.

Definition 1.9 (Homogeneous support submodule).

$$\forall n:N,\mathrm{homogeneous}\left(n\right)=\mathrm{supportSpace}\left(\mathrm{set}\left(w,\mathrm{weight}\left(w\right)=n\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.homogeneous (✓ std3).

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

The zero polynomial belongs to every degree.

Definition 1.10 (Lower level support submodule).

$$\forall k:N,\forall n:N,\mathrm{above}\left(k,n\right)=\mathrm{supportSpace}\left(\mathrm{set}\left(w,n\le \mathrm{level}\left(k,w\right)\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.above (✓ std3).

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Every supported word has level at least n.

Definition 1.11 (Extended source binomial).

$$\forall a:N,\forall l:N,(\mathrm{beta}\left(0,0\right)=1)\wedge ((\mathrm{beta}\left(0,l+1\right)=0)\wedge ((\mathrm{beta}\left(a+1,0\right)=0)\wedge (\mathrm{beta}\left(a+1,l+1\right)=\mathrm{choose}\left(a,l\right))))$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.beta (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Mixed zero pairs vanish. Positive-positive indices use the ordinary binomial coefficient.

Definition 1.12 (All bounded index tuples).

$$\forall A:Word,\mathrm{lowerIndices}\left(A\right)=\mathrm{piFinset}\left(\mathrm{lambda}\left(i,\mathrm{range}\left(\mathrm{get}\left(A,i\right)+1\right)\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.lowerIndices (✓ std3).

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

The tuple domain is Fin(length(A)); piFinset enumerates every bounded function once.

Definition 1.13 (Signed original multiplicity).

$$\forall A:Word,\forall l:\mathrm{Fin}\left(\mathrm{length}\left(A\right)\right)\to N,\mathrm{multiplicity}\left(A,l\right)=(-1{)}^{\mathrm{sum}\left(\mathrm{Fin}\left(\mathrm{length}\left(A\right)\right),\mathrm{lambda}\left(i,\mathrm{get}\left(A,i\right)\right)\right)+\mathrm{sum}\left(\mathrm{Fin}\left(\mathrm{length}\left(A\right)\right),\mathrm{lambda}\left(i,\mathrm{apply}\left(l,i\right)\right)\right)}\cdot \mathrm{prod}\left(\mathrm{Fin}\left(\mathrm{length}\left(A\right)\right),\mathrm{lambda}\left(i,\mathrm{castQ}\left(\mathrm{beta}\left(\mathrm{get}\left(A,i\right),\mathrm{apply}\left(l,i\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.multiplicity (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

For each l:Fin(length(A))->N, the sign exponent is the sum of the original and lower indices, and the beta factors are cast to Q.

Definition 1.14 (Ordinary rational commutator).

$$\forall p:H,\forall q:H,\mathrm{commutator}\left(p,q\right)=p\cdot q-q\cdot p$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.commutator (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Both products are original concatenation products.

Definition 1.15 (Left-nested ordinary brackets).

$$\forall p:H,\forall l:N,\forall ls:\mathrm{List}\left(N\right),(\mathrm{nestedBracket}\left(p,empty\right)=p)\wedge (\mathrm{nestedBracket}\left(p,\mathrm{cons}\left(l,ls\right)\right)=\mathrm{nestedBracket}\left(\mathrm{commutator}\left(p,\mathrm{letter}\left(l\right)\right),ls\right))$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.nestedBracket (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

The first list entry brackets the initial polynomial first, and the following entries continue on the left-nested result.

Definition 1.16 (Finite original generator action).

$$\forall A:Word,\forall s:N,\mathrm{letterAction}\left(A,s\right)=\mathrm{ifThenElse}\left(A=1,\mathrm{letter}\left(s\right),\mathrm{ifThenElse}\left(s=0,0,\mathrm{sum}\left(\mathrm{lowerIndices}\left(A\right),\mathrm{lambda}\left(l,\mathrm{smulQ}\left(\mathrm{multiplicity}\left(A,l\right),\mathrm{nestedBracket}\left(\mathrm{letter}\left(s+\mathrm{sum}\left(\mathrm{Fin}\left(\mathrm{length}\left(A\right)\right),\mathrm{lambda}\left(i,\mathrm{get}\left(A,i\right)-\mathrm{apply}\left(l,i\right)\right)\right)\right),\mathrm{ofFn}\left(l\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.letterAction (✓ std3).

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

This is the nested-bracket equality in the proof of Proposition 4.19, obtained from Lemma 4.10 and Definitions 4.8 and 1.9. It is the original enveloping action. The empty tuple has multiplicity one.

Definition 1.17 (The concatenation algebra projection).

$$\forall k:N,\forall s:N,\mathrm{pureProjection}\left(k,\mathrm{letter}\left(s\right)\right)=\mathrm{ifThenElse}\left(s=k,X,0\right)$$

Formalization. D5/S1/Words/PostLie/AriWordOperations.pureProjection (✓ std3).

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

This is the Q-algebra homomorphism to Polynomial Q induced by the specified images of every generator, and sends the unit to one.

Theorem 1.18 (weight one).

$$\mathrm{weight}\left(1\right)=0$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.weight_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

The empty word has weight zero.

Theorem 1.19 (weight mul).

$$\forall u:Word,\forall v:Word,\mathrm{weight}\left(u\cdot v\right)=\mathrm{weight}\left(u\right)+\mathrm{weight}\left(v\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.weight_mul (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Concatenation adds weights.

Theorem 1.20 (weight of).

$$\forall s:N,\mathrm{weight}\left(\mathrm{of}\left(s\right)\right)=\mathrm{gamma}\left(s\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.weight_of (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

A generator has its original weight.

Theorem 1.21 (level one).

$$\forall k:N,\mathrm{level}\left(k,1\right)=0$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.level_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

The empty word has level zero for every k.

Theorem 1.22 (level mul).

$$\forall k:N,\forall u:Word,\forall v:Word,\mathrm{level}\left(k,u\cdot v\right)=\mathrm{level}\left(k,u\right)+\mathrm{level}\left(k,v\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.level_mul (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Concatenation adds levels.

Theorem 1.23 (level of).

$$\forall k:N,\forall s:N,\mathrm{level}\left(k,\mathrm{of}\left(s\right)\right)=\mathrm{ifThenElse}\left(s=k,0,1\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.level_of (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

This includes the zero-index generator.

Theorem 1.24 (homogeneous basis).

$$\forall w:Word,\mathrm{wordBasis}\left(w\right)\in \mathrm{homogeneous}\left(\mathrm{weight}\left(w\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.homogeneous_basis (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

A basis monomial is homogeneous.

Theorem 1.25 (above basis).

$$\forall k:N,\forall w:Word,\mathrm{wordBasis}\left(w\right)\in \mathrm{above}\left(k,\mathrm{level}\left(k,w\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.above_basis (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

A basis monomial has its exact level.

Theorem 1.26 (homogeneous mul).

$$\forall p:H,\forall q:H,\forall a:N,\forall b:N,((p\in \mathrm{homogeneous}\left(a\right))\wedge (q\in \mathrm{homogeneous}\left(b\right)))⟹p\cdot q\in \mathrm{homogeneous}\left(a+b\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.homogeneous_mul (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Homogeneous supports multiply in the sum degree.

Theorem 1.27 (above mul).

$$\forall k:N,\forall p:H,\forall q:H,\forall a:N,\forall b:N,((p\in \mathrm{above}\left(k,a\right))\wedge (q\in \mathrm{above}\left(k,b\right)))⟹p\cdot q\in \mathrm{above}\left(k,a+b\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.above_mul (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Lower level bounds add under concatenation.

Theorem 1.28 (letterAction homogeneous).

$$\forall A:Word,\forall s:N,\mathrm{letterAction}\left(A,s\right)\in \mathrm{homogeneous}\left(\mathrm{weight}\left(A\right)+\mathrm{gamma}\left(s\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordOperations.letterAction_homogeneous (✓ std3). ∎

Citation. Annika Burmester; Ulf Kühn (2025). On post-Lie structures for free Lie algebras. DOI: 10.48550/arXiv.2504.19661. URL: https://arxiv.org/html/2504.19661v1.

Commentary.

Nonzero beta factors preserve zero positions; the shifted index is positive in the nonzero branch, so the total original weight is preserved.

References

• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.H
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.Word
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.above
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.above_basis
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.above_mul
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.beta
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.commutator
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.gamma
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.homogeneous
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.homogeneous_basis
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.homogeneous_mul
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.letter
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.letterAction
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.letterAction_homogeneous
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.level
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.level_mul
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.level_of
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.level_one
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.lowerIndices
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.multiplicity
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.nestedBracket
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.pureProjection
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.supportSpace
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.weight
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.weight_mul
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.weight_of
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.weight_one
• Truth anchor: D5/S1/Words/PostLie/AriWordOperations.wordBasis
• Dependency: D5/S1/Words/Complexity/PositivePairs/Coefficients/CutoffCoefficientAlgebra