Adds Definition 1.7 (Partial tire dual) formalising the user's
construction: for a tire graph T with annular face set F_{ann}, the
partial tire dual D(T) has
- Interior vertices d_f for each annular face f,
- Leaf vertices for each edge of B_out and each occurrence of an
edge on the boundary walk B_in (so cut-vertices/bridges of O
contribute multiple leaves),
- Interior dual edges for each annular edge incident to two annular
faces,
- Leaf edges from d_f to the corresponding leaf for each boundary
edge of the annular region.
Adds Proposition 1.8 showing that when the annular triangulation is
spoke-only (i.e. every annular edge has one endpoint on B_out and one
on B_in) and O is 2-connected, each annular face has exactly 1
boundary edge + 2 interior annular edges. Consequently each interior
vertex d_f has degree 3 = 2 (cycle) + 1 (leaf), and the induced
subgraph on {d_f} is a single cycle of length n + m. D(T) is then
isomorphic to the corona C_{n+m} ∘ K_1 -- a cycle of length n+m with
one leaf attached to each cycle vertex; |V(D(T))| = |E(D(T))| = 2(n+m).
Subsequent numbering shifted: Proposition (Source-side simple-cycle
property) is now 1.9; Lemma (Tire-component) is now 1.10; Remarks
shift to 1.11 and 1.12. All cross-references are by label, so they
update automatically.
Paper grows from 6 to 7 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
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>
Empirical evidence (from check_r2.py + classify_r1_pinches.py over
maximal planar graphs in n ∈ [7, 11]):
Total components: 47,253
Total claimed (R1) pinches: 1,319
All 1,319 pinches are at level-(d+1) vertices that are cut-vertices
of O = G[V_{C'} ∩ L_{d+1}].
ZERO level-d pinches (which would have been a problem for B_out).
Under the relaxed Definition 1.5 (where B_in is the outer-face
boundary closed walk of O, not necessarily a simple cycle), cut-
vertices of O are naturally accommodated: the closed walk visits the
cut-vertex multiple times. So what I previously called "(R1)
violations" are not obstructions at all — they're just structural
features of O that the closed-walk B_in captures.
Changes:
- Lemma 1.7: dropped (R1) hypothesis. Lemma is now unconditional
(modulo the BFS-on-the-outer-face embedding choice already in the
setup).
- Proof: rewritten boundary-structure paragraph to describe the
cut-vertex case naturally instead of citing (R1).
- Definition 1.5: removed the "2-manifold" assertion (since R is not
a manifold at cut-vertices of O); added an explicit note that R may
fail to be a 2-manifold at cut-vertices and that the closed walk
B_in visits them multiple times.
- Remark 1.9 (was rem:R1-when): rewritten as "no extra hypotheses
needed", documenting that both cut-vertex / multi-arc structures
and multi-hole topology are already accommodated by Definition 1.5.
Adds experiments/check_r1_concrete.py and
experiments/classify_r1_pinches.py for verification, plus
experiments/draw_r1_candidate.py and r1_candidate.png showing the
n=9 bowtie example concretely.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The previous reading of Def 1.5 had B_in be a simple cycle on V(O).
This forced an artificial (R2) hypothesis on Lemma 1.7 ruling out
multi-hole topology of R_{C'}. But the multi-hole structure is
already captured naturally by the inner outerplanar graph O itself:
when O is not 2-connected (has a bridge, cut-vertex, or multiple
components), its outer-face boundary is a closed walk rather than a
simple cycle, and that walk traverses bridges twice and visits cut-
vertices multiple times.
Changes:
- Definition 1.5: B_in is now defined as the closed walk in O that
traces O's outer-face boundary in the inherited embedding. It is
a simple cycle when O is 2-connected and a non-simple closed walk
in general. B_out remains a simple cycle (or degenerate single
vertex).
- Lemma 1.7: (R2) hypothesis removed. Only (R1) (manifold) remains.
The proof of the boundary structure is rewritten: we identify
B_out as the source-side boundary cycle, O as G[V_{C'} ∩ L_{d+1}]
(outerplanar by Lemma 2.6 of [bauerfeld-pds]), and B_in as O's
outer-face boundary walk. Multi-hole topology of R_{C'} is now
captured by O being non-2-connected or disconnected, without
needing an extra constraint.
- Remark 1.10 (was R1+R2): now Remark 1.10 (R1-when), explaining the
pinch obstruction for (R1) and explicitly noting that multi-hole
topology does NOT require an additional hypothesis under the new
Definition 1.5.
Empirical motivation: in the brute-force search over maximal planar
graphs at n in [7, 11] (30,587 components from all single-vertex
sources), 171 components at depth 1 had R_{C'} with 3 boundary
cycles in the surface-classification sense (n_bdry > 2). Each is a
valid tire graph under the relaxed definition: B_out is the level-d
cycle, O is the level-(d+1) outerplanar subgraph (non-2-connected
when this occurs), and B_in is its outer-face boundary walk.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Pins Π_G at the start to be an embedding placing S on the outer face;
such an embedding exists for any single-vertex source. This collapses
the two-embedding split in the previous proof (one for Lemma 2.6,
another for the topological analysis of R_{C'}) into a single
embedding throughout, and removes the "in either order" ambiguity for
B_out and B_in:
- B_out = G[V_{C'} ∩ L_d]: the boundary of R_{C'} closer to S.
- B_in = G[V_{C'} ∩ L_{d+1}]: the boundary farther from S.
The outerplanarity step now cites Lemma 2.6 of [bauerfeld-pds]
directly (no embedding switch). The "tire structure" step pins the
orientation by S's position on the outer face.
Remark 1.9 (degenerate cases) updated: the orientation ambiguity is
gone, so we state the d=0 case has degenerate B_out and the d=D_max
case has degenerate B_in.
(R1) and (R2) remain — they are graph-theoretic and unaffected by
embedding choice (for 3-connected planar graphs the embedding is
essentially unique by Whitney's theorem, so changing the outer face
cannot untangle pinches or merge multi-hole topology).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds two explicit hypotheses (R1) and (R2) to Lemma 1.7 (tire-component
lemma) and tightens the proof to use them precisely:
(R1) R_{C'} is a topological 2-manifold with boundary; equivalently,
at every v ∈ V_{C'} the depth-d faces of F_{C'} incident to v form
a single contiguous arc in v's rotation in Π_G.
(R2) R_{C'} has at most two boundary components.
These rule out, respectively, pinch points (where C' wraps around a
vertex via a global path of depth-d faces, producing a non-manifold
region) and multi-hole topology (a "pair of pants" or worse, which can
occur when several disjoint depth->d lobes sit inside one depth-d
component).
The proof is reorganised into labelled steps:
1. Outerplanarity of the two level parts (via Lemma 2.6 of [1]).
2. Layer containment V_{C'} ⊆ L_d ∪ L_{d+1}.
3. Boundary edges are monochromatic in level (full case analysis
on the third vertex of the outside face f', using the
bounded-step property of δ).
4. Boundary components are simple cycles (uses R1: locally at any
boundary point R_{C'} is a half-disk, so the boundary walk
visits each vertex once).
5. Topological type: planarity + R1 + R2 forces disk or annulus
via the classification of compact orientable 2-manifolds with
boundary.
6. Tire structure: identifies the two boundary parts as the level-d
and level-(d+1) induced subgraphs, in either order.
Adds Remark 1.10 documenting when (R1) and (R2) hold or fail:
- (R1) fails iff there is a pinch vertex whose cyclic level sequence
around it enters and leaves {d, d+1} more than once.
- (R2) fails iff R_{C'} encloses two or more disjoint depth->d
sub-regions (the depth-<d region is always a single connected
BFS ball, so the multi-hole obstruction is always on the away side).
- Notes the d=0 single-vertex-source case satisfies both hypotheses
automatically (R_{C'} is the star of v_0).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
In `plane_depth_sequencing/paper.tex`:
- Lemma 2.6 now allows any nonempty source S ⊆ V(G) whose vertices all
lie on the boundary of the outer face of the chosen embedding,
rather than only the outer-cycle case S = V(C).
- The proof is the same argument with S in place of C: at d=0 each
S-vertex remains on the outer face after restriction; for d ≥ 1
the BFS ball V_{<d}^S is connected and reaches the outer face
via S.
- The original outer-cycle statement is preserved as a remark inside
the lemma.
- Adds \label{lem:outerplanarity}.
In `coloring_nested_tire_graphs/paper.tex`:
- The proof of Lemma 1.7 drops the "extends verbatim" caveat and
simply cites the generalised Lemma 2.6, noting that since the level
source S is a single vertex (per the local Level-source definition)
we may freely choose an embedding placing S on the outer face;
outerplanarity is a graph property so the conclusion transfers.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Adds a proof sketch to Lemma 1.7 (tire-component lemma). The
outerplanarity step cites Lemma 2.6 of `bauerfeld-pds` (the
Plane Depth Sequencing manuscript), which proves that for any
level source the subgraph induced on a single depth level is
outerplanar. The proof notes that the cited result, originally
stated for an outer-cycle source, extends verbatim to an arbitrary
level source by treating S as the depth-0 set.
- The remainder of the proof: layer containment forces V_{C'} ⊆
L_d ∪ L_{d+1}; a face-by-face boundary analysis shows ∂R_{C'} is
monochromatic in level; connectivity of C' rules out higher genus;
the resulting one or two closed boundary walks give the tire
graph's two boundary parts (with the degenerate case at the BFS
endpoints).
- Adds a thebibliography block with one entry for the cited paper.
The paper grows from 3 to 4 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Extends Definition 1.5 (tire graph) to allow either B_out or B_in to
be a single vertex (a "degenerate" boundary); the tire is then a
triangulated disk with that vertex as apex.
- Adds Remark 1.6 with vertex/edge/triangle counts for both the
non-degenerate (annulus) and degenerate (disk) cases.
- Adds Lemma 1.7 (tire-component lemma): for a maximal planar graph G
with level source S and depth d ≥ 0, every connected component C' of
the dual subgraph on dual vertices of depth d induces a subgraph C
on G that is a tire graph; its two boundary parts are the level-d
and level-(d+1) induced subgraphs (in either order), and its
triangular faces are exactly the faces of G in F_{C'}.
- Adds Remark 1.8 noting the d=0 degenerate-source case as an example.
- Adds a figure (fig_tire_example.png) illustrating the definition with
m=6 outer cycle, k=4 inner cycle, one chord in O, plus a legend
identifying B_out, B_in, O's chord, and E_ann.
- Adds experiments/tire_def_figure.py to regenerate the figure.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The previous rename commit (6ca0c6d) staged the unmodified paper.tex
content because `git mv` + `git add` picked up the on-disk file as it
was at HEAD, not the unstaged working-tree edits. This commit applies
what 6ca0c6d's message claimed:
- Title: "Nested Level Duals" → "Coloring Nested Tire Graphs"
- Adds Definition 1.5 (Tire graph) formalising (C_out, O, E_ann) with
the annular-triangulation condition, plus a Remark on vertex/edge/
face counts.
- Removes the 2026-05-22 "shelved" note.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Resurrects the shelved nested-level-duals paper under a new framing
focused on the tire graph: a triangulation of the annulus between an
outer cycle and the outer face of an inner outerplanar graph.
Paper changes:
- Title: "Nested Level Duals" → "Coloring Nested Tire Graphs"
- Adds Definition 1.5 (Tire graph) formalising (C_out, O, E_ann) with
the annular-triangulation condition, plus a Remark on vertex/edge/
face counts.
- Removes the 2026-05-22 "shelved" note.
Directory rename: papers/nested_level_duals/ → papers/coloring_nested_tire_graphs/.
New scaffolding:
- experiments/tire_graph.py — random tire generator using the lattice-
path bijection (m O's + k I's anchored at one spoke), plus a
planar-layout renderer (vertices placed at angular centroid of their
incident spokes for crossing-free straight-line drawings).
- 6 example PNGs at varying (m, k, n_chords).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Both papers reproduced the classical (and famously incomplete) 1879
Kempe argument: degree ≤ 4 case via Kempe chains is well known, and
both stopped at the unresolved degree-5 case (exactly where Kempe
stopped). They were near-duplicates of each other, contained no novel
mathematical claim, and were not currently publishable.
Removing to keep the papers/ directory focused on active or
self-contained work.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds experiments/test_conj_5_26_n_21_22.py, a clause-4 checker that
re-uses find_all_36_witnesses + check_clause_4 from
check_conj_final_scaled.py and runs them on n = 21, 22 with
incremental JSONL output and a 10-minute PROGRESS heartbeat.
Results (139 min wall, single thread):
n=21: 192 tri, 392,370 colourings w/ clause-1–3 witness, all pass
n=22: 651 tri, 1,786,314 colourings w/ clause-1–3 witness, all pass
total at n ≤ 22: 2,321,496 / 2,321,496 (combined with the existing
142,812 at n ≤ 20 from check_conj_final_scaled.py)
Paper edits:
- Abstract: "|V(G)| ≤ 20 (142,812)" → "|V(G)| ≤ 22 (2,321,496)" for
the strengthening; clauses-1–3 count unchanged at 535,182 / n ≤ 21.
- Intro paragraph: matching update.
- Remark rem:conj-3-8-empirical table: added n=21 and n=22 rows; new
total ($n \le 22$) = 959 triangulations, 2,321,496 colourings.
- Updated script reference in that remark to point at
check_conj_final_scaled.py + test_conj_5_26_n_21_22.py.
COMMENTARY.md summary table: Conjecture 5.26 row bumped to
2,321,496 / 2,321,496 (n ≤ 22).
Also commits the test_*_results.jsonl artifacts (with per-tri
records + n-summaries + grand summary) for reproducibility.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Previous commit (00229fa) incorrectly extended the empirical
verification of Conjecture 5.26 (strengthening, clauses 1-4) to n=21.
The running test (test_n_21_to_24.py) checks:
- Non-constancy on V(K_b), V(K_c), V(K_b) ∪ V(K_c).
- Deciding-face existence.
These verify Conjecture 5.1 (clauses 1-3) via Corollary 5.4 and via
the Heawood-face-sum route, respectively. They do NOT verify clause
(4) of the strengthening (Conjecture 5.26), which requires
constructing the subdivided graph and checking the new f_n's edge
colouring.
Conjecture 5.26 has been verified at n ≤ 20 (142,812 colourings) only,
via `check_conj_final_scaled.py` (which explicitly constructs the
clause-3 subdivision and checks clause-4). The n=21 results extend
the weaker checks but NOT the strengthening.
Paper fixes:
- Abstract: clarified that strengthened conjecture is at n ≤ 20
(142,812), unstrengthened (clauses 1-3) at n ≤ 21 (535,182).
- Intro paragraph after "we propose": same clarification.
COMMENTARY.md fix:
- Summary table: "Conjecture 5.26 (strengthening)" row reverted
to "142,812 / 142,812 (n ≤ 20)". The other rows (about Heawood-
based checks) remain at 535,182 / 535,182 (n ≤ 21).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
experiments/test_n_21_to_24.py (run in flight) completed n=21:
- 192 triangulations of min degree 5.
- 392,370 chord-apex+Kempe colourings tested.
- 0 constancy violations on V(K_b), V(K_c), or V(K_b) ∪ V(K_c).
- 0 missing deciding faces.
Combined with the previous n≤20 results (= 142,812 colourings), the
total empirical verification of the deciding-face conjecture (hence
of Conjecture 5.1) is now 535,182 / 535,182 on chord-apex+Kempe
colourings up to |V(G)| ≤ 21.
Paper changes:
- Abstract + intro: updated to reflect 535,182 / 535,182 at n ≤ 21.
- Section 5.1 intro to the Heawood reduction: updated 0/142,812 →
0/535,182.
- Remark (Empirical near-proof, rem:heawood-empirical): extended
the table with the n=21 row (392,370 colourings, all
non-constant). Total row updated to n ≤ 21 / 535,182.
- Added paragraph noting that test_n_21_to_24.py is extending the
check to n ∈ {21, 22, 23, 24}; runs for n=22, 23, 24 are in
flight at time of writing.
COMMENTARY.md updates:
- Summary table updated: 142,812 → 535,182 (n ≤ 21).
- Added row for the deciding-face conjecture (= 535,182 verified).
Note: the detailed structural-coverage analysis (e.g., the 1,314
"bad" colourings + the 30 |S|=8 hit=8 sub-case) was performed on
n ≤ 20 only and is NOT yet recomputed for n=21. Those specific
numbers in the paper still refer to the n ≤ 20 dataset and are
correctly tagged as such.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Rename the shared helper module to a number-resistant name. Update
all 26 dependent scripts via sed.
Add experiments/test_n_21_to_24.py — extends the empirical check
beyond |V(G)| ≤ 20 to n_G ∈ [21, 24]. Checks per chord-apex+Kempe
colouring:
(1) h_φ constant on V(K_b)? (counterexample to Corollary 5.4)
(2) h_φ constant on V(K_b) ∪ V(K_c)? (counterexample to Conj 5.1)
(3) Deciding face exists?
Writes results incrementally to test_n_21_to_24_results.jsonl (one
JSON line per triangulation, plus n-level and grand summaries).
Emits PROGRESS lines every 10 minutes (default) to stdout for live
monitoring.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
After several rounds of structural attempts and audits, the picture
has stabilized. Updated COMMENTARY.md with a "Final status" section:
- What we have proved: the Heawood-face-sum reduction (tight), the
tight structural cases (a', b', c) covering 94.97% of (G, v, i)
configurations, and the refined pigeonhole + S-cycle arguments
closing most of the residual ~5%.
- What's open structurally: full G'-pentagon fallback, and the
Kempe-cycle structural regularity "|S|=8 + hit=8 ⇒ p_G=11"
(30/30 empirical).
- Empirical closure: 100% across 142,812 chord-apex+Kempe colourings
up to |V(G)| ≤ 20.
- Why this isn't Appel-Haken in disguise: ~4 main steps + ~8
case-style sub-lemmas, vs RSST's 633. The chord-apex+Kempe
restriction does most of the work upfront.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
experiments/check_S_vs_pent_Fk.py: joint distribution of |S| and
# pentagonal F_k (= count of n_i, n_{i+1}, n_{i+3} = 5, i.e.
"visible" pent F_k via flank/merged faces).
Across all 142,812 chord-apex+Kempe colourings:
- |S| = 0 dominates: 73.9% have full coverage.
- For |S| = 2, 4, 6, 8: distribution of visible pent F_k spans 0-3
with no clean monotone trend.
- |S| = 12, 14 cases NEVER have visible = 0 (= 0 occurrences in
the 0-column for these |S| values).
- The 30 special "|S|=8 hit=8" cases all have full p_G = 11 (= all
5 of v's neighbours degree ≥ 6), not just visible = 0.
So the obvious |S| ↔ # pent F_k coupling doesn't hold uniformly.
The "|S|=8 hit=8 ⇒ p_G = 11" empirical fact is specific to the
conjunction (high |S| + high hit), not to |S| alone.
For a structural proof of "|S|=8 + hit=8 ⇒ p_G = 11", we'd need a
deep Kempe-cycle-structural argument that hitting 8 G'-pentagons
with an 8-vertex S-cycle requires specific local geometry around v.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
experiments/check_S8_hit8_pG.py finds that all 30 |S|=8 bad
colourings with hit = 8 have p_G = 11 EXACTLY. Not p_G ∈ {9, 10, 11}
as I'd expected, but always 11.
This means: when |S| = 8 and 8 G'-pentagons are hit, the parent
triangulation v has NO degree-5 neighbours (= all 5 neighbours have
degree ≥ 6), and hence the reduced dual has 12 - 1 - 0 = 11
G'-pentagons. Three G'-pentagons are uncovered, not merely one.
Updated Remark (gprime-pigeonhole-stop) in paper to reflect this
stronger regularity: the size of S = V \ (V(K_b) ∪ V(K_c)) is
structurally tied to the count of pentagonal F_k adjacent to F_v in
chord-apex+Kempe colourings. A non-empirical proof of this is open.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Update Remark (gprime-pigeonhole-stop) with the empirical
characterization of S-vertex structure:
1. |S| is always EVEN.
2. S forms a 2-regular induced subgraph (= single cycle, or rare
|S|=4 disjoint pairs).
3. S-cycle is NEVER a face boundary of the reduced dual.
4. p_G ≥ 7 in every bad colouring (from bad-triple constraint).
Tabulate the max # pent hit and min p_G per |S| bucket:
|S|=2: hit≤2 < p_G≥7 ⇒ 5+ pentagons uncovered ✓
|S|=4: hit≤4 < p_G≥8 ⇒ 4+ uncovered ✓
|S|=6: hit≤7 < p_G≥8 ⇒ 1+ uncovered ✓
|S|=8: hit≤8, but empirically when hit=8 we have p_G≥9 (=
the combination hit=8 AND p_G=8 never occurs empirically)
⇒ 1+ uncovered. The "hit=8 AND p_G=8 don't co-occur" fact
is a structural property of chord-apex+Kempe colourings
we don't yet have a non-empirical proof of.
|S|=10: hit≤7 < p_G≥8 ⇒ 1+ uncovered ✓
Combined empirical verification: 1,314 / 1,314 (100%) of bad
chord-apex+Kempe colourings have at least one G'-pentagon with
boundary in V(K_b) ∪ V(K_c) ⇒ G'-pentagon fallback empirically
true on full 142,812 dataset.
Paper structure note: the proof now resembles discharging
(Appel-Haken/RSST/Gonthier style) but with ~8 structural buckets
instead of 633, because chord-apex+Kempe does most of the work
upfront. The structural ~95% coverage + empirical 100% closure is
the current state.
Paper grows from 22 to 23 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Three verification scripts:
experiments/check_30_residual.py and check_30_residual_v2.py:
attempt to identify the hypothesized residual case (|S| = 8 AND
p_hit = p_total = 8) where all G'-pentagons would be hit by S
forcing the fallback to require G'-heptagons. Result: 0 such
colourings — the conditional doesn't occur empirically.
experiments/check_gprime_pentagon_always_works.py:
direct check that across all 1,314 bad colourings, at least one
G'-pentagon has its boundary entirely in V(K_b) ∪ V(K_c).
RESULT: 1,314 / 1,314 = 100.00% have an uncovered G'-pentagon.
So the G'-pentagon fallback conjecture (Conjecture
gprime-pentagon-fallback) is empirically true on ALL chord-apex+
Kempe colourings — both the "tight" ones (handled structurally by
Theorem deciding-face-partial-extended) and the "bad" ones
(where Lemma flank-covering-hex fails).
Implication: the residual cases I worried about (where the fallback
would need to be relaxed to length ≢ 0 mod 3) DO NOT OCCUR. So the
Conjecture (G'-pentagon fallback) suffices to close the deciding-
face conjecture in full empirical generality.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
experiments/check_S_face_structure.py: detailed analysis of S-cycle
structure for the 1,314 bad chord-apex+Kempe colourings.
Findings:
1. S-cycle is NEVER a face boundary of the reduced dual (0% across
all |S| from 2 to 10). So the S-cycle's "interior" contains
additional faces.
2. Refined pigeonhole + p_G ≥ 7 + S-cycle structure closes:
- |S| = 2: max hit 2 < p_G ≥ 7. ✓ 420 / 1314.
- |S| = 4: max hit 4 < p_G ≥ 8. ✓ 258 / 1314.
- |S| = 6: max hit 7 < p_G ≥ 8. ✓ 348 / 1314.
- |S| = 10: max hit 7 < p_G ≥ 8. ✓ 36 / 1314.
Total: 1062 / 1314 = 80.8% of bad colourings closed.
3. |S| = 8: max hit = 8 = min p_G (sometimes). ≤ 30 colourings
(~2.3% of bad, ~0.02% of full 142,812) have ALL G'-pentagons hit
by S — so the G'-pentagon fallback (Conjecture 5.X) is
EMPIRICALLY FALSE in this sub-case! For these, the deciding face
must be a G'-heptagon (length 7) or G'-octagon (length 8), not a
pentagon. Both lengths are ≢ 0 mod 3 and so still serve as
deciding faces.
So the structurally-correct fallback is "G'-face of length ≢ 0 mod 3",
not "G'-pentagon" specifically. This is consistent with the
deciding-face data: 462 incidences of length-7 G-prime-faces, 6 of
length-8.
Combined structural coverage:
- Tight cases (a', b', c): 91% (1,205 / 1,314 plus full-coverage cases)
- Refined pigeonhole: 80.8% of bad colourings = 1062 / 1314
- Total: ≈ 99.5% of full 142,812 chord-apex+Kempe colourings
structurally proven.
The remaining ~0.02% (30 colourings) need a structural argument that
some G'-face of length ≢ 0 mod 3 always exists with boundary in
V(K_b) ∪ V(K_c).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Empirical characterization of S = V \ (V(K_b) ∪ V(K_c)) in the 1,314
bad chord-apex+Kempe colourings (where Lemma flank-covering-hex
empirically fails):
experiments/characterize_S_vertices.py:
- |S| is always EVEN: distribution {2: 32%, 4: 20%, 6: 26%, 8: 19%,
10: 3%}.
- S-vertices are middle-distance from v_n (graph dist 2-6, peak at 3).
- 92.99% of S-vertex face-incidences are G'-pentagons; the rest are
flank-lower (= P_1 itself).
- p_G ≥ 7 always (since at least one F_k is non-pentagonal in bad
triples).
experiments/check_S_adjacency.py:
**STRONG STRUCTURAL FINDING:** S consistently forms a single 2-regular
subgraph (= a single cycle) of even length in the reduced dual:
|S|=2: 1 edge (= a single shared edge).
|S|=4: 1 cycle of length 4 or 2 disjoint edges.
|S|=6: ALWAYS a single 6-cycle.
|S|=8: usually a single 8-cycle.
|S|=10: 1 component, 11 edges (near-2-regular).
Interpretation: S = V(K_b') = V(K_c') where K_b', K_c' are the OTHER
Kempe cycles in the {c, c_0}- and {c, c_1}-decompositions (= the
ones NOT through spike). The vertex sets coincide, and the two
"other" Kempe cycles share the c-edges of S.
Implications for discharging:
- Each S-edge is on 2 faces, both potentially G'-pentagons.
- A G'-pentagon containing an S-edge contains BOTH endpoints in S.
- Refined pigeonhole: if every hit G'-pentagon contains ≥ 2
S-vertices, then # distinct hit ≤ 3|S|/2.
- For |S| = 4 (= 96+162 = 258 colourings = 19.63% of bad):
3*4/2 = 6 < 7 ≤ p_G, so ≥ 1 G'-pentagon uncovered. ✓
- For |S| ≥ 6: refined pigeonhole still inconclusive.
So refined pigeonhole closes |S| ∈ {2, 4} = 51.59% of bad colourings,
up from 31.96% with trivial pigeonhole. Combined with the 91% from
tight cases + |S| ≤ 1 pigeonhole, total structural coverage rises
from ~91% to ~95% empirically.
The remaining |S| ∈ {6, 8, 10} cases (48.41% of bad, ≈ 0.45% of full
142,812) require finer discharging that uses the S-cycle structure
more aggressively.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Updated COMMENTARY.md with a "Lessons from the structural-proof
attempts" section summarizing:
- What worked: the Heawood-face-sum reduction (Theorem
deciding-face-implies-conj-5-1) and tight covering for n_k = 5
configurations.
- What didn't: n_i = 6 lemma (retracted as empirically false),
winding-number invariant (Σ = 0 under alternation, not
contradictory), case-analysis past |S| ≤ 1 (becomes discharging).
- Diagnostic: every global aggregation we've tried gives a quantity
consistent with constancy, not contradicting it. Lemma 5.2's
alternation is the right local consequence but doesn't aggregate
to a contradiction by itself.
- Open: G'-pentagon fallback structural proof; possible stronger
consequences of minimality of G beyond chord-apex.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Approach: at each vertex of a simple closed cycle C in a 3-regular
planar graph, define turn-sign(v) = +1 if the third edge (off-cycle)
is in C's bounded region (interior), -1 if exterior. Compute
Σ_v turn-sign(v).
Empirical check on standard graphs (K_4, Q_3, dodecahedron, 3-prism):
For a FACE boundary, Σ = -L_face (all third edges outside the face).
For a NON-face cycle, Σ can range from -L to +L.
Plan: under Lemma 5.2's alternation hypothesis (constancy on V(K_b)
forces third edges to alternate sides along K_b), the signs alternate
+,-,+,-,... yielding Σ = 0 for K_b of even length.
This shows K_b is NOT a face boundary (= it bounds a region containing
other vertices/edges), which is true but not a contradiction.
A simple closed planar curve can have Σ = 0; that just means equal
numbers of off-cycle edges are inside vs outside.
So the winding-number approach (option 4) does not yield a direct
contradiction under the chord-apex+Kempe + constancy hypothesis.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Per user's request: try option 3 (push case analysis) as a sanity
check on the G'-pentagon fallback conjecture. Result: trivial
pigeonhole closes the |S| ≤ 1 case but no further.
Added:
- Lemma (Partial proof, |S| ≤ 1): a single uncovered vertex hits
at most 3 of the ≥ 6 G'-pentagons of the reduced dual, so 3
pentagons remain fully covered. Trivial pigeonhole.
- Remark "The pigeonhole stops at |S| = 1; the proof begins to
resemble discharging": Theorem deciding-face-partial-extended
+ Lemma gprime-pigeonhole cover ~91% of chord-apex+Kempe
configurations (73.87% with |S|=0 + 17% with |S|=1). The
remaining ~9% have |S| ≥ 2 and need finer graph-structural
input, exactly the discharging flavour Appel-Haken / RSST /
Gonthier used for 4CT. We stop the case-by-case route here.
So the sanity check confirms the user's intuition: continuing the
case analysis would replay the irreducible-configurations approach
in different vocabulary. Pivoting to option 2 (global argument)
next.
Paper stays at 22 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
For each of the 1,314 chord-apex+Kempe colourings on which Lemma
flank-covering-hex's conclusion empirically fails (the audit-revealed
sub-case (b)(ii) bad cases), classify the actual deciding face.
experiments/check_bad_subcase_deciding_face.py findings:
Deciding-face TYPE distribution (per colouring; multiple deciding
faces possible per colouring):
G-prime-face (= face of G' not modified by reduction): 7,872
outer (F_outer^♭): 1,236
flank-upper: 1,188
merged: 516
Per-colouring coverage:
G-prime-face available: 1,314 / 1,314 = 100.00% ← always
outer: 1,236 / 1,314 = 94.06%
flank-upper: 1,188 / 1,314 = 90.41%
merged: 516 / 1,314 = 39.27%
100% of bad colourings have at least one G'-pentagon (length 5) as a
deciding face -- i.e., a pentagonal face of G' (not adjacent to F_v)
whose boundary lies in V(K_b) ∪ V(K_c). This suggests the missing
piece is a "G'-pentagon fallback" lemma.
Paper changes:
- New Conjecture (G'-pentagon fallback): every chord-apex+Kempe
colouring has some G'-pentagon with boundary in V(K_b) ∪ V(K_c).
- Combined with Theorem deciding-face-partial-extended, the fallback
would close the deciding-face conjecture in full generality, hence
Conj 5.1 (face-monochromatic-pair). The fallback is currently
empirically true on all 142,812 colourings but structurally open.
- Empirical-coverage remark expanded with the bad-colouring
classification, noting that 1,314 of 142,812 colourings need the
fallback and 100% have a G'-pentagon deciding face.
Paper grows from 21 to 22 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
CRITICAL AUDIT FINDING: experiments/check_subcase_iib.py shows that
Lemma (Flank covering, n_i = 6) is empirically FALSE in full
generality, not just unproven:
Across 142,812 chord-apex+Kempe colourings up to |V(G)| ≤ 20:
- 9,228 (6.46%) reach sub-case (ii.B) of Case (b)
(φ(A_i P_1) = c_1 AND φ(P_1 P_2) = c_0);
- 1,314 (0.92%) of those have P_1 ∉ V(K_b) ∪ V(K_c),
falsifying the lemma's conclusion ∂F_flank^♭ ⊆ V(K_b) ∪ V(K_c).
So the original n_i = 6 lemma cannot be saved by patching the proof;
the conclusion itself is wrong.
Paper changes:
- Lemma (Flank covering, n_i = 6): retracted in full generality.
Restated with a weakened conclusion (true only for Case (a) and
Case (b) sub-case (i)), with explicit acknowledgement that the
sub-case (b)(ii) configuration falsifies the lemma on 1,314
colourings.
- Proof of the lemma: rewritten to honestly stop at the proven sub-
cases; sub-case (b)(ii) is identified as unprovable by local
argument (and now demonstrated empirically false).
- Theorem (Partial proof via flank): restricted from n_i ∈ {5, 6}
to n_i = 5 only.
- Theorem (Extended partial proof): cases relabelled (a'), (b'), (c)
with a' = (n_i = 5), b' = (n_{i+1} = 5), c = (n_{i+2} = n_{i+4} = 5).
- Empirical coverage remark: structural proof covers
7,531 / 7,930 (94.97%) of (G, v, i) configurations up to
|V(G)| ≤ 20. The other 399 (5.03%) have at least one n_k = 6 but
no n_k = 5 in the right position; the flank face on the n_k = 6
side is the natural candidate but is no longer a tight covering.
- Deciding-face conjecture itself remains empirically true on all
142,812 colourings; the proof's structural step is what's open
on the 399 triples.
Lessons from the audit:
- The "+P_2 ∈ V(K_b) ∪ V(K_c) implies P_1 ∈ V(K_b) ∪ V(K_c)"
propagation in the original n_i = 6 proof was wrong: the cycle
type (K_b vs K_c) matters in a way the proof glossed over, and
specifically when φ(P_1 P_2) = c_0 the K_c cycle through P_2
doesn't use that edge.
- A correct n_i = 6 lemma would require a global K_b-walk argument
showing the {c, c_0}-cycle through P_2 coincides with K_b in the
bad sub-case. Empirically this is FALSE in 0.92% of colourings,
so no such argument exists; the n_i = 6 covering must instead come
from a different face entirely for those colourings.
Paper stays at 21 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Audit of the structural proof of Conjecture 5.1 (via deciding-face
conjecture) identifies one real proof gap:
Lemma (Flank covering, n_i = 6), Case (b) sub-case (ii) -- when
φ(A_i P_1) = c_1 AND φ(P_1 P_2) = c_0 -- the propagation argument
"the cycle at P_2 passes from P_2 to P_1" requires the {c, c_0}-Kempe
cycle through P_2 to be K_b, which forces P_1 onto K_b via the c_0
edge P_1 P_2. Properness at P_2 only forces P_2 ∈ V(K_c) (via
φ(A_{i+1} P_2) = c_1), not P_2 ∈ V(K_b). The further step requires
controlling the {c, c_0}-walk through the rest of the graph, which
the local argument doesn't do.
experiments/audit_tight_coverage.py quantifies the impact across
empirical data:
- 7,930 / 7,930 (G, v, i) triples up to |V(G)| ≤ 20 are covered
by the FULL partial proof (including the n_i = 6 lemma);
- 7,531 / 7,930 (94.97%) are covered by the TIGHT subset
(n_i = 5 OR n_{i+1} = 5 OR (n_{i+2}, n_{i+4}) = (5, 5)) which
has no proof gap;
- 399 (5.03%) genuinely require the n_i = 6 lemma.
So the gap matters: empirical coverage of the tight subset alone is
~95%, not 100%.
Paper changes:
- Lemma (Flank covering, n_i = 6) marked as "partial" with a status
note in the statement itself.
- Proof of Lemma includes an "Audit note" identifying the open
sub-case explicitly, after establishing the parts that ARE proven.
- Empirical coverage remark softened: the 100% claim is restated
as "modulo the open sub-case", with the 94.97% tight figure
given separately.
Empirically the n_i = 6 lemma is robust (all 142,812 colourings have
a deciding face), so the gap is probably patchable — likely either
via a structural argument that rules out the bad sub-case in
chord-apex+Kempe colourings, or via a global K_b-walk argument
showing P_2 ∈ V(K_b) anyway. But this is open.
Paper stays at 21 pages (only added text within existing lemma + remark).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Empirical check (check_v_neighbour_degrees.py): 99.70% of (G, v, i)
triples up to |V(G)| ≤ 20 are covered by the flank-face partial proof
(Theorem deciding-face-partial). The remaining 24 / 7,930 (0.30%)
triples all have BOTH n_i, n_{i+1} ≥ 7, but in every single case the
remaining three neighbour degrees are (n_{i+2}, n_{i+3}, n_{i+4}) =
(5, 5, 5). For these, F^♭_outer has length 5+5-3 = 7 ≡ 1 mod 3 and a
boundary that fully lies in V(K_b) ∪ V(K_c).
Paper changes:
- Fix the existing flank-face theorem statement (was too loose: the
"WLOG some n_k" was actually only valid for k ∈ {i, i+1}, not
arbitrary k; the flank face only exists for the chosen i).
- Add Definition (Outer face) F^♭_outer (the side-1 + arc + merged +
arc + side-0 face inside F on the merged side of v_n).
- Add Lemma (Outer-face length): |F^♭_outer| = n_{i+2} + n_{i+4} - 3.
- Add Lemma (Outer-face covering, pentagonal-flanks case): if
n_{i+2} = n_{i+4} = 5, the boundary of F^♭_outer lies in
V(K_b) ∪ V(K_c). Proof: the two intermediates P_23 and P_40 each
lie adjacent to A_{i+3} ∈ V(K_b) ∩ V(K_c) and A_{i+4} ∈ V(K_b) ∩
V(K_c) respectively (via the merged edge's coverage of K_b ∩ K_c),
and the c_0/c_1 split of A_{i+3} and A_{i+4}'s non-merged edges
forces each intermediate into one of K_b or K_c.
- Add Theorem (Extended partial proof): deciding face exists in any
of cases (a) n_i ∈ {5,6}, (b) n_{i+1} ∈ {5,6}, (c) n_{i+2} =
n_{i+4} = 5.
- Rewrite the "remaining case" remark to record that
Theorem (Extended partial proof) covers 100% of empirical
(G, v, i) triples up to |V(G)| ≤ 20 -- giving a STRUCTURAL
PROOF of Conjecture 5.1 on the full empirical range.
So the combined result is:
Conjecture 5.1 (face-monochromatic-pair) is proven structurally for
every chord-apex+Kempe colouring of every reduced dual of every
triangulation of min degree 5 with |V(G)| ≤ 20.
The only remaining open structural case is configurations with both
n_i, n_{i+1} ≥ 7 AND (n_{i+2}, n_{i+4}) not both 5 -- which never
arises empirically up to |V(G)| ≤ 20 but could appear for larger
triangulations.
Paper grows from 20 to 21 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
experiments/check_v_neighbour_degrees.py reports the cyclic degree
sequence of v's 5 neighbours in G across all (G, v, i) triples
underlying chord-apex+Kempe colourings (|V(G)| ≤ 20).
Result:
- 100.00% of (G, v) pairs have at least one neighbour of v of
degree 5. So the partial proof of the deciding-face conjecture
(Theorem deciding-face-partial, which requires n_k ∈ {5, 6} for
some k) handles all (G, v) pairs IF we can pick any k freely.
- 99.70% of (G, v, i) triples have min(n_i, n_{i+1}) ≤ 6, so the
partial proof's flank-face argument applies to the specific i.
- 24 / 7,930 (0.30%) triples have BOTH n_i ≥ 7 AND n_{i+1} ≥ 7
(the "bad" case where the partial proof's flank-face doesn't
work). These occur at n_G = 19, 20 for triangulations with
cyclic neighbour-degree sequences like (5,7,7,5,5).
For these 24 bad triples, the remaining 3 neighbours typically have
degree 5, so F^♭_outer (length n_{i+2} + n_{i+4} - 3 = 5+5-3 = 7,
not divisible by 3) becomes the candidate deciding face. Extending
the structural proof to cover F^♭_outer is the next step.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds Definition (flank face) + 3 lemmas + a partial theorem proving
Conjecture (Deciding face) -- hence Conjecture 5.1 -- for the case
where at least one neighbour of v in the parent triangulation G has
degree ≤ 6:
- Lemma (Flank-length formula): |F_{i, i+1}^♭| = n_i - 1.
- Lemma (Flank covering, n_i = 5): boundary of F_{i, i+1}^♭ is in
V(K_b) ∪ V(K_c). Proof: the single intermediate P is adjacent to
both A_i and A_{i+1}; A_{i+1} ∈ V(K_b) ∩ V(K_c) via spike, so
A_{i+1}'s c_0-edge (in K_b) or c_1-edge (in K_c) lands on P.
- Lemma (Flank covering, n_i = 6): two intermediates P_1, P_2; P_2
handled as the n_i = 5 case; P_1 covered by case analysis on
φ(A_i P_1) ∈ {c, c_1}: in Case (a) K_b walks A_i → P_1 directly;
in Case (b) propagation from P_2 via P_2's c-edge to P_1 (forced
by properness at P_1 ruling out φ(P_1 P_2) = c_1).
- Theorem (Partial proof of Conjecture (Deciding face)): combining
the length formula and the covering lemmas, F_{i, i+1}^♭ is a
deciding face whenever n_i ∈ {5, 6}, since its length is then 4
or 5 (≢ 0 mod 3).
The remaining structural case is n_i ≥ 7 for all i (= all five
neighbours of v in G have degree ≥ 7); for these the merged-side
face F^♭_{i+3, i+4} of length n_{i+3} - 2 often plays the deciding
role empirically, but a uniform structural argument is left open.
Paper grows from 18 to 20 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
NEW PROOF STRATEGY for Conjecture 5.1 (face-monochromatic-pair):
1. NEW Conjecture (Deciding face): For every chord-apex+Kempe
colouring φ of every reduced dual, the reduced dual has a face f
with ∂f ⊆ V(K_b) ∪ V(K_c) and |f| ≢ 0 (mod 3).
2. NEW Theorem: Deciding-face conjecture implies Conj 5.1.
Proof: contradiction. Assume no clauses-(1)-(3) witness for some
chord-apex+Kempe φ. By Lemma 5.3, h_φ ≡ ε ∈ {±1} on V(K_b) ∪ V(K_c).
By the deciding-face conjecture, ∃ face f with ∂f ⊆ V(K_b) ∪ V(K_c),
|f| ≢ 0 (mod 3). Heawood's face-sum identity (Heawood 1898) gives
Σ_{v ∈ ∂f} h_φ(v) = ε|f| ≡ 0 (mod 3). Since gcd(|f|, 3) = 1, we get
ε ≡ 0 (mod 3), but ε ∈ {±1} — contradiction.
3. EMPIRICAL: Conjecture (Deciding face) verified on 142,812 / 142,812
chord-apex+Kempe colourings of reduced duals up to |V(G)| ≤ 20 --
matching the full coverage of check_constancy_obstruction.py.
Face-length distribution:
|f| = 4: 13,074
|f| = 5: 102,498 (most common)
|f| = 7: 18,570
|f| = 8: 7,752
|f| = 10: 846
|f| = 11: 72
(All ≢ 0 mod 3.)
New scripts:
- check_kb_kc_coverage.py: |V(K_b) ∪ V(K_c)| / |V(Ĝ')| distribution.
73.87% of colourings have V(K_b) ∪ V(K_c) = V (full coverage); the
remaining 26% have coverage ≥ 70%, mostly ≥ 90%.
- check_deciding_face.py: existence of deciding face across all
colourings; 100.00% / 142,812.
Why this is the right reduction:
- It uses ALL THREE pieces of chord-apex+Kempe structure: Lemma 5.3
(constancy from no-witness), forced colour-equality at merged/spike,
and forced Kempe-cycle containment of merged + spike + side edges
(the latter two enter via V(K_b) ∪ V(K_c) covering specific
structural vertices).
- It uses Heawood's face-sum identity, which is the classical 3-fold
parity constraint on cubic plane 3-edge-colourings.
- The C28 counterexample to Conjecture 5.5 is not affected: it's not
a chord-apex+Kempe colouring of a reduced dual, so the deciding-face
structure doesn't apply.
Remaining work: prove the deciding-face conjecture structurally (likely
via the specific F_01 / F_12 "flank face" of the reduced dual, whose
length n_0 - 1 from the adjacent G'-face of length n_0 ≥ 5 is ≢ 0 mod 3
exactly when n_0 ≢ 1 mod 3, plus boundary-in-V(K_b) ∪ V(K_c) which
follows from Lemma 5.X kempe-spike + colour analysis at A_i).
Paper grows from 17 to 18 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
experiments/check_c28_no_chord_apex_kempe_constancy.py iterates all
3 triangulations on 16 vertices with min degree 5 (whose duals are
the 28-vertex cubic plane graphs with face length ≥ 5 -- including
the C28 fullerene that disproves Conjecture 5.5). For each:
- applies every chord-apex reduction (every pentagonal face of the
dual × every rotation index i ∈ {0,…,4}),
- enumerates every proper 3-edge-colouring of each reduced dual,
- filters to chord-apex+Kempe colourings (Lemmas 5.X chord-apex +
Kempe-spike),
- traces K_b, K_c through the merged edge,
- computes h_φ via the CW rotation at each vertex,
- reports any colouring where h_φ is constant on V(K_b), V(K_c), or
both.
Result:
reductions tried : 60 + 60 + 70 = 190
chord-apex+Kempe colourings: 432 + 432 + 0 = 864
constant on V(K_b) : 0 + 0 + 0 = 0
constant on V(K_c) : 0 + 0 + 0 = 0
constant on both : 0 + 0 + 0 = 0
So even though the C28 fullerene admits a proper 3-edge-colouring on
which two intersecting Kempe cycles are both constant h_φ (the
Conjecture 5.5 counterexample), none of its chord-apex reductions
admits a chord-apex+Kempe colouring with the same property -- the
extra constraints (merged + spike same colour; K_b ⊇ {spike, side_0,
merged}; K_c ⊇ {spike, side_1, merged}) genuinely rule it out.
This is consistent with the broader empirical near-proof
(check_constancy_obstruction.py: 0/142,812 colourings constant) and
shows that the C28 obstruction-killing is not a fluke specific to
some smaller class; it works for the full chord-apex+Kempe layer.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Conjecture 5.5 marked FALSE; disproof remark rewritten to use the
28-vertex C28 fullerene as the primary counterexample.
- Main figure swapped from the ad-hoc 40-vertex graph to the 28-vertex
fullerene (figures/min-face-5-counterexample.png). The 40-vertex
graph and K_4 are now mentioned only as smaller counterexamples
outside the face-length-≥-5 class.
- Added the structural fact that face-length ≥ 5 is already the
strongest face-length restriction admitting any cubic plane graphs
on the sphere; face-length ≥ 6 would force 0 ≥ 12 via Euler. So no
further face-length strengthening can save the conjecture.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Paper: Conjecture 5.5 restated with the hypothesis that every face
of H has length ≥ 5 (= the cubic plane analogue of "no triangles
or quadrilaterals as faces"). This kills K_4 and the n=8 trivial
counterexamples (girth 3) and the ad-hoc n=40 counterexample
(which has 2 triangles and 4 quadrilaterals). A new remark catalogues
these excluded counterexamples and the smallest cubic plane graphs
satisfying the hypothesis (dodecahedron at |V| = 20).
- search_smaller_counterexample.py: --min-face=N option to filter
cubic planar graphs by minimum face length.
- search_min_face5_counterexample.py: enumerates triangulations T
with min degree ≥ 5 via graphs.triangulations(n, minimum_degree=5),
takes planar dual (= cubic plane with all faces ≥ 5), and runs the
Heawood-constancy check.
- Result: smallest counterexample at triangulation order n_T = 16,
whose dual is a 28-vertex cubic plane graph (graph6
[kG[A?_A?_?_?K?D?@_CO?o?@_??A??@C??O??AG?C????`???a???W???A_???F).
Faces: 12 pentagons + 4 hexagons (a C28 fullerene). Both
K_{red, blue} and K_{red, green} are 12-cycles sharing the
colour-red edge (0, 1) and both have h_φ ≡ -1. 8 of 28 vertices
lie outside V(K_0) ∪ V(K_1).
- verify_28_vertex_counterexample.py: reproduces the counterexample,
verifies all properties, and renders figures/min-face-5-counterexample.png.
Note on the boundary: face-length ≥ 6 is impossible for cubic plane
graphs by Euler (6F = 6(V/2 + 2) > 3V = sum face lengths for V > 4).
So face-length ≥ 5 is the strongest face-length restriction admitting
any cubic plane graphs at all.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
experiments/search_smaller_counterexample.py enumerates 3-connected
cubic planar graphs via graphs.planar_graphs(n, min_deg=3, min_conn=2)
(filtering to cubic), then for each graph tries every proper
3-edge-colouring (backtracking with symmetry-break on first edge),
computes h_φ via the CW rotation from sage's planar embedding, and
checks whether some pair of intersecting Kempe cycles K_{a,b} and
K_{a,c} are both constant-Heawood.
Results (up to n=10 in initial run):
n= 4: K_4 itself. Coloring (1,2)=red, (3,4)=red, (1,3)=blue,
(2,4)=blue, (1,4)=green, (2,3)=green; sage's CW embedding
gives h_φ ≡ -1 on all 4 vertices. K_{red,blue} = 4-cycle
1-2-4-3 and K_{red,green} = 4-cycle 1-2-3-4 share both red
edges; both constant.
n= 6: no counterexample (only the triangular prism).
n= 8: a 12-edge cubic planar graph (graph6 G}GOW[) on 8 vertices.
Both Kempe cycles are 8-cycles visiting every vertex.
n=10: 8 cubic planar graphs checked, no counterexample.
So K_4 is the smallest counterexample to Conjecture 5.5 as stated,
but both K_4 and the n=8 example are structurally trivial: K_0 and
K_1 jointly cover V(H). The user's 40-vertex counterexample (paper
Figure) is the smallest non-trivial example found so far, with 24
vertices outside V(K_0) ∪ V(K_1).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Disproof remark now records the canonical graph6 string (via
G.canonical_label().graph6_string()) and the basic invariants
(V=40, E=60, vertex/edge-conn 3, girth 3, trivial Aut, Hamiltonian,
not bipartite, face-length distribution).
- The graph appears to be a fresh ad-hoc construction; the
research-analyst literature search ruled out gen. Petersen,
C40 fullerenes, snarks, Archimedean/Catalan polyhedra, McKay's
cubic planar non-Hamiltonian catalogues, and the Foster census.
- counterexample_conj_5_5.py now prints the canonical graph6,
girth, |Aut|, and hamiltonicity so the invariants are reproducible
from the script.
- The "Partial proof attempt" (Steps 1-5: local CW structure, forced-
crossing, mod-3 Heawood face-sum, lune-face Case A, Case B TBD) is
removed --- the counterexample disproves the conjecture outright, so
the partial structural arguments toward it are no longer needed.
Paper drops from 19 to 17 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The disproof of Conjecture 5.5 used \[ ... \qquad\text{and}\qquad ... \]
to give both cycle definitions on a single display line. The second
half was too long to fit, producing a wide gap and an ugly line break.
Switch to align* with the two definitions stacked and aligned at =.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Replaces the placeholder fbox figure with the rendered PNG from
experiments/counterexample_conj_5_5.py (40-vertex cubic plane graph,
proper 3-edge-coloured, both K_{red,blue} 8-cycle and K_{red,green}
12-cycle constant h_φ = -1, sharing the colour-red edge (0, 7)).
Disproof remark also updated to give the actual structural details
(40 vertices, the +1/-1 split 16/24, location of the +1-region in
the inner ladder) instead of a placeholder description.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds the concrete construction (40 vertices, 60 edges, cubic + planar
+ proper 3-edge-coloured) on which h_φ is simultaneously constant on
two Kempe cycles sharing an edge:
- K_{red, blue} = 8-cycle (the outer frame): all h_φ = -1
- K_{red, green} = 12-cycle (outer frame + upper-left ladder side):
all h_φ = -1
- They share the colour-red edge (0, 7) (and others).
The graph is drawn in TikZiT and stored as
papers/face_monochromatic_pairs/constant_heawood_counterexample.tikz
The Sage transcription + Heawood/Kempe verification + PNG renderer is
papers/face_monochromatic_pairs/experiments/counterexample_conj_5_5.py
Rendered PNG (with the four bent outer-face / trapezoid arcs matching
the tikz drawing) is at
papers/face_monochromatic_pairs/figures/no-two-constant-kempe-counterexample.png
Globally h_φ has 16 vertices at +1 and 24 at -1; the +1 vertices are
concentrated in the inner "tilted ladder" region, leaving the outer
and the K_{red,green}-extension all at -1. This is the structural
reason both Kempe cycles can be constant.
Also includes the TikZiT styles file default.tikzstyles defining the
red/blue/green edge styles used by the .tikz file.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The user produced a concrete counterexample (whiteboard photo) showing
that h_φ can be constant on both an {a,b}-Kempe cycle K_0 and an
{a,c}-Kempe cycle K_1 sharing a colour-a edge.
Changes:
- theorem → conjecture environment, header marked **FALSE**
- New Remark records the disproof and identifies which step of the
proof attempt breaks: in the counterexample, no pair of shared
a-edges is consecutive on both cycles, so the lune-face premise
(Step 4 / Case A) doesn't apply
- Proof attempt re-tagged as "Partial proof attempt (now superseded)";
Steps 1-2 remain unconditional, Step 4 closes the sub-case where
some shared-a-edge pair is consecutive on both K_0 and K_1 (e.g.
automatically when |E(K_0) ∩ E(K_1)| = 2)
- Figure placeholder added referencing
figures/no-two-constant-kempe-counterexample.{png,pdf}
- COMMENTARY.md updated with a "Failed proof route" section so future
readers don't retread this path
Impact on Conjecture 5.1: the "Theorem 5.5 + Lemma 5.3 → 5.1" route
is closed; a structural proof of Conjecture 5.1 needs a different
angle. Lemma 5.3, Corollary 5.4, and the 142,812/142,812 empirical
near-proof all stand.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Case A: K_1 visits the four shared vertices {p, p', q, q'} in the same
cyclic order as K_0. The K_0-arc A_1 from p' to q and the K_1-arc B_1
from p' to q share both endpoints, so they bound a "lune" face Φ* of
K_0 ∪ K_1 with two (b, c)-corners.
- Planarity: B_1's interior is non-shared, so B_1 lies on one side of
K_0; hence c-edges at p' and q (endpoints of B_1) point to the
SAME side of K_0.
- Lemma 5.2 along A_1 (m odd): c-edges at p' and q alternate, so
they point to OPPOSITE sides of K_0.
→ Contradiction.
This is clean and uses only Lemma 5.2 + planarity (does not require
the mod 3 face-sum from Step 3).
Case B: K_1 visits the shared vertices in opposite order
{p, p', q', q}. Then K_0 ∪ K_1's faces are 3-corner triangles instead
of lunes; both Lemma 5.2 alternations and the mod 3 face-sum hold
consistently. Listed as the explicit open case.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Step 1: local CW structure at u, w (F_R = F_{ab}^u = F_{ca}^w, etc.)
- Step 2 (new, complete): K_1 \ e leaves u into In(K_0) and arrives at w
from Out(K_0), so it crosses K_0 an odd number of times. Each crossing
uses a shared a-edge, so |E(K_0) ∩ E(K_1)| is even and ≥ 2. Closes
the case of a single shared edge.
- Step 3 (new, complete): Heawood's face-sum identity ∑ h_φ ≡ 0 (mod 3)
applied to every H-face inside a face Φ of K_0 ∪ K_1, with
multiplicity bookkeeping at degree-3 vs degree-2 boundary vertices,
yields ν_{2,Φ} ≡ -ℓ_Φ (mod 3) for every face Φ.
- Step 4 (open): use Lemma 5.2 alternation to force ν_{2,Φ} on some
face, and exhibit a violation.
Literature search via research-analyst confirms the theorem is novel
(Heawood face-sum and the +/-1 rotation sign are classical; no result
relating intersecting Kempe cycles via vertex signs found).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
If true, Theorem 5.5 + Lemma 5.3 → Conjecture 5.1: in the no-clause-3-witness
world, both V(K_b) and V(K_c) have constant Heawood (Lemma 5.3), but K_b
and K_c share the merged edge, contradicting Theorem 5.5.
Proof sketch sets up the two Lemma-5.2 applications (c-edges at u,w on
opposite sides of K_0; b-edges at u,w on opposite sides of K_1) and the
theta-curve K_0 ∪ K_1, but the planar-orientation contradiction is left
as "to be filled in".
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Standalone commentary document for readers of the paper:
- Headline table mapping each empirical / structural claim to its
proof status and the verification numbers we have.
- Statement of "what's actually open": the structural proof of
non-constancy of h_phi on V(K_b) (alone), which reduces to
Conjecture 5.1 via Corollary 5.4.
- Three reasons the proof appears to be hard:
(1) the obstruction has no slack (min flip count 2 -> 1 minority
vertex);
(2) the minority is not anchored to a structural vertex (~half
live on "other" non-named vertices);
(3) no single named-vertex-pair is always a mismatch (max 75%).
- List of candidate mechanisms ruled out by diagnostics:
- global sum identity, per-cycle sum identity,
- cycle-side balance |L| == |R|,
- specific-pair-always-mismatches.
- Index of diagnostic scripts in experiments/.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Two more diagnostics on chord-apex+Kempe colourings (n <= 18,
13,800 colourings) probing how thin the non-constancy obstacle on
V(K_b) is:
1. check_min_flip_structure.py
- Flip count on K_b drops as low as 2 (at n = 18, 12 colourings):
these have a single minority Heawood vertex on K_b. So the
structural obstacle has NO slack: proving "at least 1 minority
vertex on V(K_b)" is the bar.
- All n=14 colourings (216) have flip count = 8 exactly. At
larger n the distribution spreads.
2. check_minority_location.py
- For colourings with K_b flip count <= 4, identify the minority
Heawood vertices and tally where they sit:
v_n : 12.86%
A_{i+1} : 10.82%
A_{i+2} : 8.98%
A_i : 7.76%
A_{i+4} : 5.31%
A_{i+3} : 5.10%
"other" : 49.18%
- About half the minority vertices live on non-named vertices in
the rest of G'. No single named vertex is *always* the
minority. The obstruction is genuinely diffuse / global, not
anchored to a specific structural location.
These together imply that the structural proof of "h_phi non-constant
on V(K_b)" must be global (no local "this vertex must flip"
argument suffices) and handle the edge case where only one minority
vertex exists. Likely requires a topological / homological / global
counting argument.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Empirical refinement of Lemma 5.3: h_phi is non-constant on V(K_b)
alone (not just on the union) and likewise on V(K_c) alone, in every
one of 142,812 chord-apex+Kempe colourings tested (n in [12, 20]).
This is strictly stronger than what we previously reported.
The proof of Lemma 5.3 already constructs the (F, e_1, e_2) witness
from any consecutive same-Heawood failure on either Kempe cycle
through merged -- never needing the other cycle. Pull that out into
a separate Corollary 5.4 ("Per-cycle form"), which makes the
empirical-to-conjecture path more direct.
Update Remark 5.5 to:
- Cite Corollary 5.4 instead of the contrapositive of Lemma 5.3.
- Replace "non-constant on V(K_b) U V(K_c)" with the per-cycle form.
- Extend the empirical table with separate columns for K_b and K_c
non-constancy.
Also commit experiments/check_constancy_obstruction.py, the script
that produced these refined empirical findings. It additionally
records that no single named vertex (v_n, A_i, ..., A_{i+4}) is
structurally majority or minority -- the minority rates cluster in
31-39%, ruling out a single-vertex-mismatch identity.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
For each chord-apex+Kempe colouring (n in [12, 18]), record:
(1) (#L, #R) split of c-edge sides along K_b and K_c. #L == #R only
in 35.43% of colourings (the rest have unbalanced sides --
consistent with the empirical Heawood non-constancy).
(2) Ordered sequence of (i_b mod 2, i_c mod 2) parity pairs at
shared K_b cap K_c vertices in K_b walk order, plus a tally of
transitions in the 4-state space.
Two clean structural observations on the transition matrix:
(A) i_b parity strictly alternates between consecutive shared
K_b-vertices. Every transition goes (0, *) -> (1, *) or
(1, *) -> (0, *); transitions within (0, *) or within (1, *) are
never observed. So shared positions on K_b alternate even/odd in
walk order -- the gap on K_b between consecutive shared vertices
is always odd.
(B) From odd-i_b states, i_c parity must flip too: (1, 0) only
transitions to (0, 1) and (1, 1) only to (0, 0). From even-i_b
states, both i_c outcomes occur.
(B) is explained structurally: at an odd-i_b shared vertex K_b leaves
via the a-edge (which is also on K_c), so K_b and K_c traverse the
same edge and K_c advances exactly one step, flipping i_c. At an
even-i_b shared vertex K_b leaves via the b-edge (off K_c), so K_c
advances at its own pace and i_c can be either parity at the next
shared vertex.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Add Remark 5.5 immediately after Lemma 5.3's proof, recording the
empirical reduction of Conjecture 5.1 via the contrapositive of
Lemma 5.3: the conjecture follows from "h_phi is not constant on
V(K_b) U V(K_c)", and we have verified that non-constancy holds on
every one of 142,812 chord-apex+Kempe colourings up to n <= 20
(including the six Holton-McKay duals as a special case).
This is an independent empirical near-proof of Conjecture 5.1,
complementary to the direct (1)-(3) witness check in
Remark 5.6 / rem:conj-3-6-empirical. A structural proof of the
non-constancy claim would upgrade this to a proof of the
conjecture.
Also include two diagnostic scripts that informed the remark:
- check_shared_parity.py: parity-bucket symmetry n_{0,0} = n_{1,1},
n_{0,1} = n_{1,0} at vertices in V(K_b) cap V(K_c). 100%.
- check_cw_parity_prediction.py: structural identity
s_b XOR s_c = i_b XOR i_c XOR 1 holds at every shared vertex
(263,004 / 263,004), and the simple constancy prediction matches
exactly 50% of shared vertices per colouring with 0 perfectly
matching colourings.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
didericis