Map One Cycle and Both Marked Orders Together
Abstract
Map One Cycle and Both Marked Orders Together.
Theorem 1.1 (Transport the Complete Simultaneous State).
Lean statement: D5/S3/Combinatorics/Graph/Walks/ActualTwoOrderStateTransport.actual_two_order_state_map
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/ActualTwoOrderStateTransport.actual_two_order_state_map (✓ std3). ∎
Source. Repository-derived.
Commentary.
An injective graph map carries all three literal partitions of one supplied actual cycle, both marked cut groups and their disjointness to the same mapped cycle. Every resulting piece is the actual image of its source piece, including for a proper graph inclusion.