Chronological Signature Group-Like Hopf Laws

Abstract

Step-two chronological signatures satisfy the group-like coproduct and antipode laws, and the antipode reverses event order with negated values.

Definition 1.1 (Group-like diagonal).

Lean statement: D5/S3/Observer/Chronology/ChronologicalSignatureHopf.groupLikeCoproduct

Formalization. D5/S3/Observer/Chronology/ChronologicalSignatureHopf.groupLikeCoproduct (✓ std3).

Source. Repository-derived.

Commentary.

The finite group-like coproduct sends a signature to two identical copies.

Theorem 1.2 (Multiplicative diagonal).

$$\forall a,b,\mathrm{groupLikeCoproduct}(a\cdot b)=(\mathrm{fst}(\mathrm{groupLikeCoproduct}(a))\cdot \mathrm{fst}(\mathrm{groupLikeCoproduct}(b)),\mathrm{snd}(\mathrm{groupLikeCoproduct}(a))\cdot \mathrm{snd}(\mathrm{groupLikeCoproduct}(b))).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Chronology/ChronologicalSignatureHopf.group_like_coproduct_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

The diagonal preserves chronological multiplication componentwise.

Theorem 1.3 (Coassociative group-like diagonal).

$$\begin{array}{c}\forall a:\\ (\mathrm{fst}(\mathrm{groupLikeCoproduct}(a)),\mathrm{fst}(\mathrm{groupLikeCoproduct}(\mathrm{snd}(\mathrm{groupLikeCoproduct}(a)))),\mathrm{snd}(\mathrm{groupLikeCoproduct}(\mathrm{snd}(\mathrm{groupLikeCoproduct}(a)))))\\ =(\mathrm{fst}(\mathrm{groupLikeCoproduct}(\mathrm{fst}(\mathrm{groupLikeCoproduct}(a)))),\mathrm{snd}(\mathrm{groupLikeCoproduct}(\mathrm{fst}(\mathrm{groupLikeCoproduct}(a)))),\mathrm{snd}(\mathrm{groupLikeCoproduct}(a))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Chronology/ChronologicalSignatureHopf.group_like_coproduct_coassociative (✓ std3). ∎

Source. Repository-derived.

Commentary.

Either order of iterating the diagonal produces three identical signature components.

Theorem 1.4 (Left antipode cancellation).

$$\forall a,\mathrm{signatureAntipode}(\mathrm{fst}(\mathrm{groupLikeCoproduct}(a)))\cdot \mathrm{snd}(\mathrm{groupLikeCoproduct}(a))=1.$$

Proof. Machine-checked in Lean as D5/S3/Observer/Chronology/ChronologicalSignatureHopf.antipode_left_convolution (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplying the antipode leg by the identity leg yields the empty signature.

Theorem 1.5 (Right antipode cancellation).

$$\forall a,\mathrm{fst}(\mathrm{groupLikeCoproduct}(a))\cdot \mathrm{signatureAntipode}(\mathrm{snd}(\mathrm{groupLikeCoproduct}(a)))=1.$$

Proof. Machine-checked in Lean as D5/S3/Observer/Chronology/ChronologicalSignatureHopf.antipode_right_convolution (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplying the identity leg by the antipode leg yields the empty signature.

Theorem 1.6 (Reverse-and-negate realizes the antipode).

$$\forall f,L,\mathrm{chronologicalSignature}(x\mapsto -f(x),\mathrm{reverse}(L))=\mathrm{signatureAntipode}(\mathrm{chronologicalSignature}(f,L)).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Chronology/ChronologicalSignatureHopf.chronological_signature_reverse_neg (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reversing an event word and negating every observed value gives exactly the antipode of its chronological signature.

Theorem 1.7 (Reverse-and-negate in logarithmic coordinates).

$$\forall f,L,\mathrm{chronologicalLog}(\mathrm{chronologicalSignature}(x\mapsto -f(x),\mathrm{reverse}(L)))=\mathrm{inverse}(\mathrm{chronologicalLog}(\mathrm{chronologicalSignature}(f,L))).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Chronology/ChronologicalSignatureHopf.chronological_log_reverse_neg (✓ std3). ∎

Source. Repository-derived.

Commentary.

After applying the logarithm, reverse-and-negate becomes coordinatewise negation.

Theorem 1.8 (Involutive chronology reversal).

$$\forall f,L,\mathrm{signatureAntipode}(\mathrm{chronologicalSignature}(x\mapsto -f(x),\mathrm{reverse}(L)))=\mathrm{chronologicalSignature}(f,L).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Chronology/ChronologicalSignatureHopf.chronological_signature_reverse_neg_involutive (✓ std3). ∎

Source. Repository-derived.

Commentary.

Applying the finite antipode after reverse-and-negate recovers the original signature.

Theorem 1.9 (Reversal of concatenation).

$$\begin{array}{c}\forall f,P,S:\\ \mathrm{chronologicalSignature}(x\mapsto -f(x),\mathrm{reverse}(\mathrm{append}(P,S)))\\ =\mathrm{signatureAntipode}(\mathrm{chronologicalSignature}(f,S))\cdot \mathrm{signatureAntipode}(\mathrm{chronologicalSignature}(f,P)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Chronology/ChronologicalSignatureHopf.chronological_signature_reverse_neg_append (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reverse-and-negate sends concatenation to the reversed product of the two antipodes.

References

• Truth anchor: D5/S3/Observer/Chronology/ChronologicalSignatureHopf.antipode_left_convolution
• Truth anchor: D5/S3/Observer/Chronology/ChronologicalSignatureHopf.antipode_right_convolution
• Truth anchor: D5/S3/Observer/Chronology/ChronologicalSignatureHopf.chronological_log_reverse_neg
• Truth anchor: D5/S3/Observer/Chronology/ChronologicalSignatureHopf.chronological_signature_reverse_neg
• Truth anchor: D5/S3/Observer/Chronology/ChronologicalSignatureHopf.chronological_signature_reverse_neg_append
• Truth anchor: D5/S3/Observer/Chronology/ChronologicalSignatureHopf.chronological_signature_reverse_neg_involutive
• Truth anchor: D5/S3/Observer/Chronology/ChronologicalSignatureHopf.groupLikeCoproduct
• Truth anchor: D5/S3/Observer/Chronology/ChronologicalSignatureHopf.group_like_coproduct_coassociative
• Truth anchor: D5/S3/Observer/Chronology/ChronologicalSignatureHopf.group_like_coproduct_mul
• Dependency: D5/S3/Observer/Chronology/StepTwoChronologicalLogarithm