Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Literal Native Domains for the Same Recursive Cycle

Abstract

Literal Native Domains for the Same Recursive Cycle.

Theorem 1.1 (Rotate the Base to the Actual Child Gap).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.native_child_frame_domain

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

Source. Repository-derived.

Commentary.

Rotating only the base list of a supplied frame to gap j gives a prior marked special domain equal to the independently defined outer child at j, for every configuration. The selected list and terminal retain their literal values.

Theorem 1.2 (Identify All Child Vertices).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.child_marked_domain_map_bijective

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

Source. Repository-derived.

Commentary.

The identity map on actual configurations between the rotated prior marked domain and its independent child domain is bijective.

Theorem 1.3 (Earn the Actual Ordinary Supplier Cut).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.native_child_frame_specified_ordinary

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

Source. Repository-derived.

Commentary.

A Hamilton cycle on the rotated prior marked domain with its remaining-b invariant yields a specified ordinary child cycle for the parent constructor. The invariant proves that the literal supplier cut belongs to the same mapped cycle; raw support, edges and both protected selected labels are preserved.

Theorem 1.4 (Selected Orders Share One Marked Domain).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.native_marked_orders_same_domain

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

Source. Repository-derived.

Commentary.

Two supplied marked frames have the same actual special domain when their selected label sets, ordered bases and terminals agree. Their ports may differ; the equality concerns every actual vertex configuration.

Theorem 1.5 (Reindex Marked Orders by the Identity Map).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.marked_order_domain_map_bijective

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

Source. Repository-derived.

Commentary.

The configuration identity between two marked orders with equal selected sets, bases and terminals is bijective, allowing both order descriptions to refer to one supplied cycle.

Theorem 1.6 (Selected Orders Share One Outer Parent).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.native_outer_orders_same_domain

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

Source. Repository-derived.

Commentary.

Two outer parents obtained from frames with equal selected label sets, terminal and remaining base share every actual native parent vertex. The ordered remaining base is kept.

Theorem 1.7 (Identify the Two Outer Parent Orders).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.parent_order_domain_map_bijective

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

Source. Repository-derived.

Commentary.

The identity on actual configurations between the two equal outer parent domains is bijective.

Theorem 1.8 (Identify the Complete Prior P Child).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.native_p_marked_domain_eq_child

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

Source. Repository-derived.

Commentary.

When a supplied prior base is A followed by u and A has length at least three, its entire marked special domain equals the final child of its outer frame. The proof uses the literal circular rotation, extending ownership beyond the marked endpoints.

Theorem 1.9 (Identify the Complete Next Marked Domain).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.native_next_marked_domain_eq_parent

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

Source. Repository-derived.

Commentary.

The actual parent domain of the outer frame is exactly the next marked special domain. Prepending u to the selected list and rotating the terminal around the remaining base earns the identity for every configuration.

Theorem 1.10 (Carry Every Parent Vertex to the Next Marked Frame).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.parent_next_marked_map_bijective

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

Source. Repository-derived.

Commentary.

The configuration identity from the actual current parent domain to the next marked domain is bijective.

Theorem 1.11 (Transport the Same Cycle and Its Earned Edges).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.native_same_parent_cycle_next_marked

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

Source. Repository-derived.

Commentary.

A supplied parent Hamilton cycle with protected-a and remaining-b invariants maps to the next marked domain without changing any raw configuration, support entry or edge. Both retained-edge invariants hold on this exact mapped cycle; no replacement cycle is chosen.

Theorem 1.12 (Include the Complete Prior P State).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeMarkedFrameDomains.p_marked_parent_lift_injective

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

Source. Repository-derived.

Commentary.

The configuration identity including the complete prior P marked domain into the actual current outer parent is injective, allowing actual prior walks and partitions to be mapped without identifying distinct vertices.

References