The Sixth Actual J2 Path Component
Abstract
The two remaining independently specified J2 ports are joined by a sixth actual complete path component.
Theorem 1.1 (The Actual Component from L1 to Bar L0).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeJ2SixthComponent.native_j2_sixth_full_component (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every m at least five, the theorem constructs an actual simple path in survivingGraph(m) from port(m,(1,false,true)) to port(m,(0,true,true)). Its support consists exactly of all vertices reachable from the first port, and it contains every actual surviving edge incident to that component.
Apply the endpoint-aware six-cut slicing theorem to the same actual F2 Hamilton cycle containing the six independently specified marked edges. Map and transfer the resulting subtype walks into the actual surviving graph. Their supports partition the full F2 domain and their edges are exactly the surviving inventory. Disjointness and edge saturation therefore make each piece a whole component. Every port is a graph leaf, so it can occur only at a path endpoint. The five constructed literal word components exclude ten of the twelve ports from the component of L1. The actual surviving a edge at L1 rules out a nil piece. Its other endpoint must consequently be bar L0, and reversing the actual slice when necessary earns the stated orientation.
Higher actual recursive expansion and Hamilton cycles for all sizes remain separate obligations.