dual_decomposition: pentagonal externals lemma + edge naming

- Name the edges of the reduced-dual construction (merged, spike, sides)
  via a new definition; use these names in lem:chord-apex.
- Add lem:pentagonal-externals with full exhaustive proof: any proper
  3-edge-colouring near a pentagonal face of a cubic plane graph has its
  five external edges forming, up to cyclic rotation, the pattern
  (a, b, c, c, c) with {a, b, c} = {1, 2, 3} (iff).
- Cite the new lemma in the chord-apex proof scaffold as the lifting step.
- Remove the icosahedron experimental remark.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-05-22 20:22:00 -04:00
parent 20f19f0869
commit 0303225f39
6 changed files with 165 additions and 34 deletions