Adds Proposition 1.7 (Source-side simple-cycle property): in any
maximal planar graph G with single-vertex source v_0, for any vertex
v at level d and any connected component C' of G'_d incident to v,
the depth-d faces of F_{C'} at v form a single contiguous arc in v's
rotation in Pi_G. Equivalently: the source-side boundary of R_{C'}
is always a simple cycle in L_d, with no cut-vertices at level d.
Proof: contradiction via Jordan curve theorem. If two arcs of
depth-d faces at v exist, pick level-(d-1) neighbours p, q of v in
the two gaps. The BFS ball G[L_{<d}] is connected so admits a simple
path P from p to q. The closed walk v -> p -> P -> q -> v is a
simple cycle W (since v is the only vertex at level >= d on it). W
separates the plane into two regions; the two arcs at v lie on
opposite sides. Any dual path of depth-d faces from one arc to the
other must avoid v on its intermediate faces, but consecutive
intermediate faces share edges entirely in L_{>= d}, so the dual
path stays on one side of W. This contradicts the endpoints being
on opposite sides.
Lemma 1.8 (the tire-component lemma) now cites Proposition 1.7 to
justify that B_out is always a simple cycle. Level-(d+1) pinches
(cut-vertices of O) remain allowed and are accommodated by the
relaxed Definition 1.5.
The empirical search (n in [7, 12], 47k + 276k = 323k components,
13k+ pinches all level-(d+1) cut-vertices of O, zero level-d
pinches) is now subsumed by the structural proof.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
didericis
c2961b1833