Replaces the earlier sketch with a more detailed two-stage proof:
Stage 1: BFS level-set lemma.
Lemma (BFS-adj): adjacent edges in line graph differ in depth by
at most 1. Proof: BFS-distance property.
Lemma (level-set): every face of H_d contains only edges of depth
<d, or only edges of depth >d. Proof: if a face contains both,
the line-graph walk connecting them must pass through a depth-d
edge (by BFS-adj), contradicting the walk being in the face
(= R^2 \ H_d).
Stage 2: faces of H_{d+1} embed in faces of H_d.
Key claim: no H_d edge sits strictly inside any face of H_{d+1}.
Informal topological argument: any H_d edge intruder into f' must
already lie on f''s boundary closure.
Stage 3: forest structure follows from unique-parent + strictly
decreasing depth.
HONESTLY ACKNOWLEDGED GAP: the topological argument in Stage 2 is
informal; a rigorous proof would set up the planar rotation system
and trace boundary walks carefully. Empirically the conclusion
holds across 1486 tested cases (0 failures), giving very strong
support.
Note grows to 5 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
didericis
410c2a1b35