Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Update the Complete Actual Native Joint Partition

Abstract

Update the Complete Actual Native Joint Partition.

Theorem 1.1 (Earn the New Joint Partition on the Same Parent Cycle).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeActualJointUpdate.native_actual_closed_parent_joint_update

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeActualJointUpdate.native_actual_closed_parent_joint_update (✓ std3). ∎

Source. Repository-derived.

Commentary.

Given the concrete closed parent Hamilton cycle, the actual opened old P path and its exact deleted marked-edge inventory, the actual three-fragment Q split, and the literal chain connecting the other children, the proof earns a complete next joint partition. Actual vertex counts, uncut edges, endpoint pairs, disjoint marked groups and their erase identities all refer to this same parent cycle. This is a concrete propagation interface; unconditional all-order existence is not claimed.

References