Restore the Actual Native Third-Order Base State
Abstract
Restore the Actual Native Third-Order Base State.
Theorem 1.1 (Earn Both Native Templates from Eight Actual Paths).
Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeThirdOrderBoundaryBase.native_third_order_boundary_base
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeThirdOrderBoundaryBase.native_third_order_boundary_base (✓ std3). ∎
Source. Repository-derived.
Commentary.
Eight supplied actual third-order joint paths exhaust the same Hamilton cycle. Their literal native port coordinates earn both marked cut groups and the O3 and E3 restored boundary templates, including the distinguished-path and crossing identities. The theorem restores this concrete eight-path configuration and does not itself construct the eight paths or prove unconditional all-order existence.