Construct the Complete Native Parent from Independent Children
Abstract
Construct the Complete Native Parent from Independent Children.
Theorem 1.1 (Earn Full Parent Hamiltonicity).
Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeOuterChildAssembly.native_parent_cycle_of_child_paths
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeOuterChildAssembly.native_parent_cycle_of_child_paths (✓ std3). ∎
Source. Repository-derived.
Commentary.
Actual Hamilton paths on every independently defined native child, with their literal native endpoints, are joined in supply order into one Hamilton cycle on the full parent domain. Disjoint child domains prove disjoint support, the independent insertion partition proves complete parent coverage, and native c-generator seams close the same actual cycle. Its raw start, support and edge inventories are retained.