Chow's theorem at level two

Group-like series are exactly the signatures of piecewise-linear paths, to second order: over a finite alphabet, every character of the word shuffle Hopf algebra agrees up to degree two with the signature of an explicit piecewise-linear path (exists_piecewiseLinear_eq_of_isGroupLike_levelTwo); conversely every such signature is group-like (isGroupLike_piecewiseLinearSignature).

The construction is the classical one: a straight segment matches the level-one data, and one rectangle loop per coordinate plane corrects the antisymmetric part of the level-two data — the shuffle identity forces the symmetric part, and loops contribute pure area. Degree two is the order at which the library's rough path analysis operates; the full-depth identification (Chow–Rashevskii) needs the free Lie algebra and remains on the roadmap.

Low-degree expansion of the tensor product

Rectangle loops

def RoughPaths.Word.rectLoop {α : Type u} {R : Type v} [DecidableEq α] [Field R] (i j : α) (c : R) : List (α → R)

The rectangle loop in the (i,j)-coordinate plane with area parameter c: out, up, back, down.

Equations

• RoughPaths.Word.rectLoop i j c = [Pi.single i c, Pi.single j 1, -Pi.single i c, -Pi.single j 1]

Appending area loops

Chow's theorem at level two

theorem RoughPaths.Word.exists_piecewiseLinear_eq_of_isGroupLike_levelTwo {R : Type v} {d : ℕ} [Field R] [CharZero R] {a : List (Fin d) → R} (ha : IsGroupLike a) : ∃ (segs : List (Fin d → R)), ∀ (w : List (Fin d)), w.length ≤ 2 → coeff (piecewiseLinearSignature segs) w = coeff a w

Chow's theorem at level two: over a finite alphabet, every group-like series — every character of the word shuffle Hopf algebra — agrees up to degree two with the signature of an explicit piecewise-linear path: a straight segment for the first level, plus one rectangle loop per coordinate plane for the antisymmetric second-level part (the symmetric part is forced by the shuffle identity). Together with isGroupLike_piecewiseLinearSignature, the group-like elements are exactly the piecewise-linear signatures to second order.