AriWordProduct

Abstract

Ordered primitive unshuffle and rational ari product

N includes zero. H is the rational concatenation-word algebra and Word its ordinary basis index type. Functions to Fin(n) assign each original position to one slot. Tuple words multiply componentwise by concatenation. Every assignment is summed separately; identical resulting tuples are not deduplicated. List products retain their displayed order. For a word, length and get mean the corresponding operations on its original toList. In orderedTerm, j ranges over Fin(length(B)); successor slots have indices j+1.

Definition 1.1 (Ordered slot subsequences).

$$\forall n:N,(\forall e:\mathrm{Fin}\left(0\right)\to \mathrm{Fin}\left(n\right),\forall j:\mathrm{Fin}\left(n\right),\mathrm{slot}\left(empty,e,j\right)=1)\wedge (\forall a:N,\forall A:\mathrm{List}\left(N\right),\forall f:\mathrm{Fin}\left(\mathrm{length}\left(A\right)+1\right)\to \mathrm{Fin}\left(n\right),\forall j:\mathrm{Fin}\left(n\right),\mathrm{slot}\left(\mathrm{cons}\left(a,A\right),f,j\right)=\mathrm{ifThenElse}\left(\mathrm{apply}\left(f,0\right)=j,\mathrm{of}\left(a\right)\cdot \mathrm{slot}\left(A,\mathrm{tail}\left(f\right),j\right),\mathrm{slot}\left(A,\mathrm{tail}\left(f\right),j\right)\right))$$

Formalization. D5/S1/Words/PostLie/AriWordProduct.slot (✓ 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 and successor cases have their own function domains. For f:Fin(length(A))->Fin(n), slot j is the subsequence of A whose positions map to j. The tail of f sends i to f(succ(i)).

Definition 1.2 (primitiveUnshuffle).

$$\forall n:N,\mathrm{primitiveUnshuffle}\left(n\right)=\mathrm{FreeMonoidLift}\left(\mathrm{lambda}\left(a,\mathrm{sum}\left(\mathrm{Fin}\left(n\right),\mathrm{lambda}\left(j,\mathrm{single}\left(\mathrm{update}\left(\mathrm{constant}\left(1\right),j,\mathrm{of}\left(a\right)\right),1\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordProduct.primitiveUnshuffle (✓ 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 monoid homomorphism is the free-monoid lift of the primitive sum. Its target is MonoidAlgebra Q of the n-tuples of original words; the tuple with a single nonempty slot represents placement in that tensor factor.

Theorem 1.3 (primitiveUnshuffle_assignments).

$$\forall n:N,\forall A:\mathrm{List}\left(N\right),\mathrm{primitiveUnshuffle}\left(n,\mathrm{ofList}\left(A\right)\right)=\mathrm{sum}\left(\mathrm{Fin}\left(\mathrm{length}\left(A\right)\right)\to \mathrm{Fin}\left(n\right),\mathrm{lambda}\left(f,\mathrm{single}\left(\mathrm{lambda}\left(j,\mathrm{slot}\left(A,f,j\right)\right),1\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordProduct.primitiveUnshuffle_assignments (✓ 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 proves the equality of the primitive multiplicative expansion with all ordered position assignments, including empty words and zero slots.

Definition 1.4 (orderedTerm).

$$\forall B:Word,\forall S:\mathrm{Fin}\left(\mathrm{length}\left(B\right)+1\right)\to Word,\mathrm{orderedTerm}\left(B,S\right)=\mathrm{wordBasis}\left(\mathrm{apply}\left(S,0\right)\right)\cdot \mathrm{listProd}\left(\mathrm{ofFn}\left(\mathrm{lambda}\left(j,\mathrm{letterAction}\left(\mathrm{apply}\left(S,\mathrm{succ}\left(j\right)\right),\mathrm{get}\left(B,j\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordProduct.orderedTerm (✓ 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.

S has domain Fin(length(B)+1). Slot zero is concatenated with the list product of the actions of each successor slot on the corresponding original letter of B.

Definition 1.5 (starWord).

$$\forall A:Word,\forall B:Word,\mathrm{starWord}\left(A,B\right)=\mathrm{sum}\left(\mathrm{Fin}\left(\mathrm{length}\left(A\right)\right)\to \mathrm{Fin}\left(\mathrm{length}\left(B\right)+1\right),\mathrm{lambda}\left(f,\mathrm{orderedTerm}\left(B,\mathrm{lambda}\left(j,\mathrm{slot}\left(\mathrm{toList}\left(A\right),f,j\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordProduct.starWord (✓ 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 summation domain is every position assignment, not the set of distinct slot tuples.

Theorem 1.6 (starWord_unshuffle).

$$\forall A:Word,\forall B:Word,\mathrm{starWord}\left(A,B\right)=\mathrm{apply}\left(\mathrm{basisConstrQ}\left(\mathrm{MonoidAlgebraBasis}\left(\mathrm{Fin}\left(\mathrm{length}\left(B\right)+1\right)\to Word\right),\mathrm{orderedTerm}\left(B\right)\right),\mathrm{primitiveUnshuffle}\left(\mathrm{length}\left(B\right)+1,A\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordProduct.starWord_unshuffle (✓ 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 linear extension of orderedTerm is applied to the actual primitive unshuffle. This is the finite source product presentation of Proposition 2.1.

Definition 1.7 (star).

$$\forall P:H,\forall Q:H,\mathrm{star}\left(P,Q\right)=\mathrm{sum}\left(\mathrm{support}\left(P\right),\mathrm{lambda}\left(A,\mathrm{sum}\left(\mathrm{support}\left(Q\right),\mathrm{lambda}\left(B,\mathrm{smulQ}\left(\mathrm{coeff}\left(P,A\right)\cdot \mathrm{coeff}\left(Q,B\right),\mathrm{starWord}\left(A,B\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/PostLie/AriWordProduct.star (✓ 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 rational bilinear extension of the ordered primitive-unshuffle construction. The displayed finite-support formula follows from its basis values.

Theorem 1.8 (star_basis).

$$\forall A:Word,\forall B:Word,\mathrm{star}\left(\mathrm{wordBasis}\left(A\right),\mathrm{wordBasis}\left(B\right)\right)=\mathrm{starWord}\left(A,B\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordProduct.star_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.

The bilinear primitive construction has exactly the assignment-defined basis values.

Theorem 1.9 (starWord_homogeneous).

$$\forall A:Word,\forall B:Word,\mathrm{starWord}\left(A,B\right)\in \mathrm{homogeneous}\left(\mathrm{weight}\left(A\right)+\mathrm{weight}\left(B\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordProduct.starWord_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.

Every nonzero supported term has the sum of the two original input weights. The unshuffle slots partition all input positions.

Theorem 1.10 (starWord_above).

$$\forall k:N,\forall A:Word,\forall B:Word,\mathrm{starWord}\left(A,B\right)\in \mathrm{above}\left(k,\mathrm{level}\left(k,B\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/PostLie/AriWordProduct.starWord_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.

Each non-k letter of B contributes at least one non-k letter in every supported output. Multiplication adds counts; summation and cancellation cannot create smaller-level support.

References

• Truth anchor: D5/S1/Words/PostLie/AriWordProduct.orderedTerm
• Truth anchor: D5/S1/Words/PostLie/AriWordProduct.primitiveUnshuffle
• Truth anchor: D5/S1/Words/PostLie/AriWordProduct.primitiveUnshuffle_assignments
• Truth anchor: D5/S1/Words/PostLie/AriWordProduct.slot
• Truth anchor: D5/S1/Words/PostLie/AriWordProduct.star
• Truth anchor: D5/S1/Words/PostLie/AriWordProduct.starWord
• Truth anchor: D5/S1/Words/PostLie/AriWordProduct.starWord_above
• Truth anchor: D5/S1/Words/PostLie/AriWordProduct.starWord_homogeneous
• Truth anchor: D5/S1/Words/PostLie/AriWordProduct.starWord_unshuffle
• Truth anchor: D5/S1/Words/PostLie/AriWordProduct.star_basis
• Dependency: D5/S1/Words/PostLie/AriProjection