Primitivity of the truncated log-signature

A series b is primitive for the shuffle coproduct when b([]) = 0 and Σ_{x ∈ u ⧢ v} b(x) = 0 for all nonempty u, v (the boundary sums against [] are automatic, so this is Δ_⧢ b = b ⊗ 1 + 1 ⊗ b in coefficient form). Main theorem: the truncated logarithm of a group-like series is primitive up to the truncation degree — the first-order shadow of "the log-signature lies in the free Lie algebra".

Proof: shuffle sums of (a-1)^{⊗k} expand via the shuffle–deconcatenation compatibility Word.shuffle_splits_perm as Σ_{i,j} N(k,i,j)·(a-1)^{⊗i}(u)·(a-1)^{⊗j}(v), where N(k,i,j) is the coefficient of xⁱyʲ in (x+y+xy)^k, realised in ℤ[y][x]. The required vanishing Σ_k (-1)^k/(k+1)·N(k+1,i,j) = 0 for i,j ≥ 1 is the coefficient identity of log((1+x)(1+y)) = log(1+x) + log(1+y): after d/dx the sum becomes geometric, (1+x+y+xy)·W = (1-(-x-y-xy)^n)(1+y) pins down the low-degree coefficients of W by a bidegree recursion.

Primitive series

def RoughPaths.Word.IsPrimitive {α : Type u} {R : Type v} [Semiring R] (b : List α → R) : Prop

A series is primitive for the shuffle coproduct: the empty coefficient vanishes and all mixed shuffle sums over nonempty word pairs vanish.

Equations

• RoughPaths.Word.IsPrimitive b = (RoughPaths.Word.coeff b [] = 0 ∧ ∀ (u v : List α), u ≠ [] → v ≠ [] → RoughPaths.Word.shuffleCoeff b u v = 0)

def RoughPaths.Word.IsPrimitiveUpToDegree {α : Type u} {R : Type v} [Semiring R] (b : List α → R) (n : ℕ) : Prop

Primitivity up to a degree: mixed shuffle sums vanish whenever the total length is at most n.

Equations

• RoughPaths.Word.IsPrimitiveUpToDegree b n = (RoughPaths.Word.coeff b [] = 0 ∧ ∀ (u v : List α), u ≠ [] → v ≠ [] → u.length + v.length ≤ n → RoughPaths.Word.shuffleCoeff b u v = 0)

theorem RoughPaths.Word.isPrimitive_iff_forall_isPrimitiveUpToDegree {α : Type u} {R : Type v} [Semiring R] (b : List α → R) : IsPrimitive b ↔ ∀ (n : ℕ), IsPrimitiveUpToDegree b n

theorem RoughPaths.Word.zero_isPrimitive {α : Type u} {R : Type v} [Semiring R] : IsPrimitive (zero α R)

theorem RoughPaths.Word.IsPrimitive.add {α : Type u} {R : Type v} [Semiring R] {b c : List α → R} (hb : IsPrimitive b) (hc : IsPrimitive c) : IsPrimitive (b + c)

theorem RoughPaths.Word.IsPrimitive.smul {α : Type u} {R : Type v} [Semiring R] (r : R) {b : List α → R} (hb : IsPrimitive b) : IsPrimitive (r • b)

The bilinear pairing form of shuffle–deconcatenation

compatibility

theorem RoughPaths.Word.shuffleCoeff_tensorProduct {α : Type u} {R : Type v} [CommSemiring R] (f g : List α → R) (u v : List α) : shuffleCoeff (tensorProduct f g) u v = (List.map (fun (p : List α × List α) => (List.map (fun (q : List α × List α) => shuffleCoeff f p.1 q.1 * shuffleCoeff g p.2 q.2) (HopfAlgebras.Word.splits v)).sum) (HopfAlgebras.Word.splits u)).sum

Shuffle sums of a tensor product expand over the splittings of both words — the pairing form of Word.shuffle_splits_perm.

List-sum utilities

Splitting sums against the unit, and short-word vanishing

Bidegree coefficients of (x + y + xy)^k in ℤ[y][x]

The shuffle expansion of tensor powers of the augmentation part

The main theorem

theorem RoughPaths.Word.isPrimitiveUpToDegree_logSignatureTruncated {α : Type u} {R : Type v} [Field R] [CharZero R] {a : List α → R} (ha : IsGroupLike a) (n : ℕ) : IsPrimitiveUpToDegree (logSignatureTruncated a n) n

The truncated log-signature of a group-like series is primitive up to the truncation degree. This is the coefficient-level statement that the logarithm of a shuffle character is an infinitesimal character — the first-order form of "log-signatures are Lie elements".

theorem RoughPaths.Word.Signature.isPrimitiveUpToDegree_logTruncated {α : Type u} {R : Type v} [Field R] [CharZero R] (σ : Signature α R) (n : ℕ) : IsPrimitiveUpToDegree (σ.logTruncated n) n

The truncated log-signature of a bundled group-like signature is primitive up to the truncation degree.