Truncated Tensor Hopf Balance
Abstract
Degree-two tensor signatures satisfy the truncated group-like balance.
Definition 1.1 (Canonical tensor flip).
Lean statement: D5/S3/Observer/Chronology/TruncatedTensorHopf.tensorFlip
Formalization. D5/S3/Observer/Chronology/TruncatedTensorHopf.tensorFlip (✓ std3).
Source. Repository-derived.
Commentary.
The two degree-one tensor factors are interchanged by Mathlib’s canonical tensor symmetry.
Definition 1.2 (Step-two group-like equation).
Lean statement: D5/S3/Observer/Chronology/TruncatedTensorHopf.IsStepTwoGroupLike
Formalization. D5/S3/Observer/Chronology/TruncatedTensorHopf.IsStepTwoGroupLike (✓ std3).
Source. Repository-derived.
Commentary.
A doubled degree-two coordinate is group-like when its symmetric part is twice the tensor square of degree one.
Theorem 1.3 (Every finite word is group-like).
Proof. Machine-checked in Lean as D5/S3/Observer/Chronology/TruncatedTensorHopf.chronological_tensor_signature_is_step_two_group_like (✓ std3). ∎
Source. Repository-derived.
Commentary.
The zero degree-one and degree-two coordinates satisfy the balance, and a pure tensor square is fixed by the tensor flip, so the empty and single-event signatures are group-like.
The symmetric cross terms generated by chronological composition complete the tensor square of the summed degree-one coordinate, so group-likeness is closed under Chen multiplication; induction over the event list extends it to every finite chronological word.
References
- Truth anchor:
D5/S3/Observer/Chronology/TruncatedTensorHopf.IsStepTwoGroupLike - Truth anchor:
D5/S3/Observer/Chronology/TruncatedTensorHopf.chronological_tensor_signature_is_step_two_group_like - Truth anchor:
D5/S3/Observer/Chronology/TruncatedTensorHopf.tensorFlip - Dependency: D5/S3/Observer/Chronology/TruncatedTensorSignature