Selected Terminal Labels of the Same Actual c Edges
Abstract
The literal F2 seams and the exact inventory of one supplied frame walk earn the selected-terminal condition for every actual c edge.
Theorem 1.1 (Every Literal Seam Endpoint Has a Selected Terminal).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeJ2SelectedC.native_f2_seam_selected_terminal (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every m at least five, every literal F2 seam e, and every endpoint x of e, the terminal label x(m) is zero or m. For a T seam, its starting endpoint is the finish of its own indexed deleted a or b edge. The complete a-cut classification puts both terminal labels in {0,m}; the b-cut classification puts its terminal in the same set. An E seam similarly starts at the finish of its own indexed deleted b edge. The generator c fixes the terminal position, so the second endpoint keeps that label. This proves the condition directly from the independently defined seams.
Theorem 1.2 (The Supplied Frame Walk Earns Its Selected c-Terminal Condition).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeJ2SelectedC.native_j2_frame_c_selected (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every m at least five and every SupplyFrame(m,2), take any supplied closed walk w in the actual FrameDomain, with its exact undo-relabel inventory of native-minus-deleted edges together with F2 seams. Whenever x,y are actual frame vertices, y=x*c and their actual subtype edge occurs in w, the terminal label of x belongs to F.selected.toFinset. The c generator differs from both native generators a and b, so the retained native branch of this same inventory cannot supply that edge. The seam branch supplies the raw {0,m} terminal condition, and the same earned frame relabelling maps that set exactly to F.selected. The proof keeps this particular walk and earns its c-edge condition; no replacement cycle or separate target invariant is assumed.