- Add section 3 with Algorithm 3.1 (iterated reduction with protected edges)
and remarks on invariants and chord-apex applicability.
- Add fig:iterated-reduction-trace illustrating the algorithm on G' =
dodecahedron (G' -> H_1 -> H_2 -> terminate).
- experiments/iterated_reduction.py: Sage implementation of the algorithm.
- experiments/draw_iterated_reduction.py: produces the 3 trace figures.
- experiments/check_dodecahedron_kempe.py: enumerate proper 3-edge-colorings
of the dodecahedron's reduced dual and check the chord-apex + Kempe-cycle
conditions (0 of 36 colorings satisfy all three).
- experiments/search_kempe_property.py: search across min-deg-5
triangulations; the n = 14 first plantri triangulation is the smallest hit
(reduced dual has 20 v, 30 e).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Update def:edge-names to distinguish side-0 ({A_i, v_n}) and side-1
({A_{i+2}, v_n}); merged and spike unchanged.
- Add a paragraph defining the {a,b}-Kempe cycle in a 3-edge-coloured cubic
graph.
- Add lem:kempe-spike: in any proper 3-edge-colouring of the reduced dual,
the {c, c_0}-Kempe cycle through the spike contains side-0 and merged
(symmetrically for side-1 with c_1).
- Proof by Kempe swap: a hypothetical alternative cycle K containing merged
but not spike would, after swapping c <-> c_0 on K, give a proper
3-edge-colouring under which spike and merged disagree --- contradicting
lem:chord-apex.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Replace the chord-apex TODO with a full proof by contradiction: assume
merged != spike, define X, Y, Z, W, lift to G' so that the externals
inherit \psi(f) = (X, Y, Z, W, W), and split on W in {X, Z}. Either case
meets the hypothesis of lem:pentagonal-externals, which extends \psi to a
proper 3-edge-colouring of G' --- contradicting non-3-edge-colourability
via Tait.
- Add fig:chord-apex-proof: the assumed reduced-dual colouring on top, and
the two lifted-G' cases (W=Z, W=X) below, rendered on the dodecahedron.
- Add experiments/draw_chord_apex_proof.py.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- 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>
Add Definition 2.1 (reduced dual) and a remark on cubicity/planarity, plus an
experiment verifying it on the icosahedron/dodecahedron and four figures, one
per construction step.
reduced_dual.py builds G' = dodecahedron (dual of the icosahedron), applies the
construction, and confirms the result is a cubic, planar, simple graph whose
dual is a simple triangulation. Finding: the construction is an n -> n-2
reduction (12 -> 10 here), not n-1, since the single apex v_n collapses one more
vertex than a standard pentagon re-triangulation; the result also re-introduces
degree-3 and degree-4 vertices (degree seq [7,5,5,5,5,5,5,4,4,3]).
draw_reduced_dual_steps.py renders fig_reduced_dual_step1..4.png, embedded as a
2x2 grid after the definition.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Remove the Introduction and Strategy sections and everything after the
separating-cycle definition (no-separating-triangle lemma, 5-connectivity
proposition, and the Step 2-6 stubs). Rename the section heading from
"Step 1: The minimal counterexample" to "The minimal counterexample", drop
the now-unused separating-cycle definition, and adjust the lead-in to mention
only the degree reduction. Remaining: reduction-to-triangulations lemma,
minimal-counterexample definition, |V|>=12 remark, and minimum-degree-5 lemma.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
New paper "Dual Decomposition of Minimal Counterexamples" outlining a six-step
cut-and-recombine attack on the 4CT via the dual cubic graph: minimal
counterexample -> dualise -> minimum (cyclic) edge cut -> cap to cubic ->
3-edge-colour the pieces -> reconnect. Strategy section flags steps 1-5 as
standard machinery and step 6 (recombination) as the crux.
Step 1 written in full: reduction to triangulations, definition of the minimal
counterexample, minimum-degree >= 5 (degree <=3 and degree-4 Kempe cases), and
no separating triangle => 4-connected. 5-connectivity stated as Birkhoff's
separating-4-cycle reduction (attributed, not re-derived).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
didericis