Actual Joint and Route Fragments
Abstract
The retained joint prefix and two actual route cuts yield the literal fragments used by graph surgery.
The vertex type and simple graph are arbitrary. All paths and cycle inventories refer to the literal supplied walks. These statements provide actual graph-surgery steps; an all-order recursive Hamilton construction is a separate consumer.
Theorem 1.1 (Recover the Actual P and Q Fragments).
Lean statement: D5/S3/Combinatorics/Graph/Walks/ActualJointRouteSlicing.actual_joint_and_route_three_fragments
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/ActualJointRouteSlicing.actual_joint_and_route_three_fragments (✓ std3). ∎
Source. Repository-derived.
Commentary.
The old actual vertex partition and retained supplier edges force the distinguished joint path prefix. Two cuts in distinct supplied route pieces have earned strict order on the same joined route. The output records the original joint tail and three actual simple route fragments with exact support and edge decompositions.