Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Construct the Actual Joint Partition of a Closed Parent Cycle

Abstract

Construct the Actual Joint Partition of a Closed Parent Cycle.

Theorem 1.1 (Three New Paths and Every Unchanged Old Piece).

Lean statement: D5/S3/Combinatorics/Graph/Walks/ActualClosedParentJointUpdate.actual_closed_parent_joint_partition

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/ActualClosedParentJointUpdate.actual_closed_parent_joint_partition (✓ std3). ∎

Source. Repository-derived.

Commentary.

The supplied Hamilton parent has the literal closed chain of an actual three-fragment Q path, intermediate children and the actual opened P path. Exact P source inventories and Q split identities construct three new paths while retaining all other old joint pieces. Their complete support, uncut edges, cut cardinality and endpoint-pair update belong to this same parent cycle.

References