Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Earn the Actual Native P Prefix and Retained Q Cuts

Abstract

Earn the Actual Native P Prefix and Retained Q Cuts.

Theorem 1.1 (Derive the Literal Two-Edge P Prefix).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeActualPJointPrefix.native_actual_p_joint_prefix

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

Source. Repository-derived.

Commentary.

Protected a and remaining b invariants of the actual old cycle, together with its exact joint inventory and native coordinates, earn the distinguished path two-edge prefix and the remaining actual tail. The supplier b edge has an unselected base terminal and differs from both old marked cut groups.

Theorem 1.2 (Locate the Actual Retained Q Prefix Edges).

Lean statement: D5/S3/Combinatorics/Graph/PrefixReversal/NativeActualPJointPrefix.native_actual_q_zero_cut_retained

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

Source. Repository-derived.

Commentary.

The actual old Q cycle invariants and literal next-frame zero-port coordinates imply that both new prefix edges occur in the old joint pieces. Terminal labels distinguish the new b edge from every supplier cut, and the a edge joins two unprotected remaining labels. The two endpoint vertices are proved distinct.

References