Previous figures drew σ as VERTEX colors on a 6-cycle. This was
misleading: σ = (1,2,3,2,3,1) is not a proper vertex 3-coloring of
a hexagon (σ_5 = σ_0 = 1 at adjacent vertices), and the user
correctly flagged this.
σ is the coloring of the 6 *spoke edges* -- the G'-edges of G' that
cross γ, equivalently the 6 edges of γ ⊂ G under the duality
γ-edge ↔ crossing G'-edge.
Adjacent γ-edges meet at γ-vertices, which are not G'-vertices, so
σ has NO proper-coloring constraint on itself. Proper-edge-coloring
constraints live on each tire's full annular cycle, which is longer
than 6 (T_1's is 12, T_2's is 9), with γ-spokes interleaved among
non-γ spokes; that's where the extendibility of σ is actually
checked.
Redrawn figures:
- fig_rainbow_orbit.png: σ drawn as edge colors of γ (not vertex
colors), all 6 orbit elements.
- fig_rainbow_pattern.png: abstract pattern abcbca as edge labels,
with explanatory text in the legend.
- fig_rainbow_setup.png: shows γ between the two tires with each
tire's full annular cycle (length 12 and 9), the interleaved
non-γ dual vertices, the dashed G'-spoke edges crossing γ
colored by σ, and T_1's antipodal chord in O_1.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Bypasses the 3^n brute-force iteration in tire_fiber_chords.py by
directly constructing the 2^n proper edge 3-colorings of C_n via a
vectorized binary-branch numpy build. Benchmarked 146× speedup at n=12,
424× at n=15; brings n=18 to 0.1s and n=24 to 6.6s.
Step-2 extension at k=9 (13 pairs) and k=12 (10 pairs): every tested
pair is compatible (23/23, bringing total to 46/46 with the earlier
note). The S_3-orbit observation extends: the smallest tested
intersection at k=12 is again exactly 6 elements forming a single
S_3-orbit of the pattern (1,2,3,2,2,1,3,3,2,3,1,1) — each of T1's four
chord-induced faces receives a permutation of {1,2,3} as its σ-values,
a "Latin-style" assignment.
Note conjectures a structural theorem: every SP-feasible tire's
projection support contains the "Latin-flavoured" subset where each
O-face sees a permutation of {1,2,3}, and this gives a common
substructure that makes chain-pigeonhole succeed.
Caveat: intersection sizes are all multiples of 6, consistent with the
S_3 invariance of both supports.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds three figures visualising the rainbow-orbit intersection from
tire_fiber_step2.tex (Observation rainbow):
k=6, T_1=(m=6, chord=(0,3), SP) vs T_2=(k=3, no chord, SR)
|S_1 ∩ S_2| = 6 = the S_3-orbit of (a,b,c,b,c,a)
Files:
- fig_rainbow_orbit.png: 6-panel grid showing all 6 orbit elements,
each as a hexagon coloured by the corresponding σ.
- fig_rainbow_pattern.png: abstract pattern abcbca on the shared
cycle γ with explicit position-class legend.
- fig_rainbow_setup.png: geometric setup — T_1 outside γ with its
antipodal chord (v_0, v_3) ∈ O_1, T_2 inside γ (a triangle), and
the orbit element σ = (1,2,3,2,3,1) shown on γ.
Adds experiments/draw_rainbow_orbit.py generator script.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
For pairs (T1, T2) sharing a cycle γ, intersect T1's D-projection
(inner-spoke pattern from outer tire) with T2's U-projection
(outer-spoke pattern from inner tire) on γ. Compatibility = nonempty
intersection.
Result: 23/23 tested pairs are compatible, spanning k ∈ {3,4,5,6},
both SR/SP models, and a range of chord configurations on each side.
Notable: small intersections have clean S_3-orbit structure. Worst
tested case (k=6, antipodal-chord T1 vs unchorded SR T2) has
intersection of size 6 — exactly the 3! rainbow patterns (a,b,c,b,c,a).
This suggests structural rather than accidental overlap, and points to
a theorem worth proving.
Caveats: 23 cases at k≤6 isn't a proof; longer chains (step 3) require
more than pairwise overlap.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Companion to tire_fiber_data.tex. The chord case forces a modelling
choice for the surrounding G: Steiner-rich (each B_in edge gets its
own sub-triangle, chords are invisible to T'_{f'}) vs Steiner-poor
(each O-face is one G-face, chord set determines feasibility).
Under SP, a tire with k > 3 is infeasible unless O already contains
enough chords to keep every O-face at most 3 B_in edges. With chords:
support is positive but much smaller than SR — π_D never reaches 3^k,
and π_D's shrinkage is m-independent. More chords = smaller faces =
MORE support (each chord splits a hard constraint into easier ones).
Side-by-side data table for (m, k) ∈ {3,4,5,6,...}² with various
chord sets, plus 3-page note documenting the modelling choice and
implications for chain pigeonhole.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Step 1 of birkhoff_heesch_reducibility action items. Brute-force
enumerates N(T'_{f'}; σ) for G_n = C_n + n pendants at 3 colors,
n=3..12. Two empirical findings: (1) fiber sizes are always 1 or 2
(constant σ on even n gives size 2; everything else gives size 1);
(2) projecting C onto k evenly-spread positions covers {1,2,3}^k iff
n ≥ 2k. The second implies that for a tire with |B_out| ≥ |B_in|,
every ring coloring on the inner boundary is realisable — so the
chain-pigeonhole intersection step is trivially nonempty whenever the
shared cycle is not locally the longest. Includes script, raw JSON,
text dump, and 4-page data note.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Summarises classical reducibility theory (Birkhoff 1913, Heesch
discharging, Appel-Haken, RSST) in modern notation, then maps it
onto the spoke-fiber decomposition: ring colorings ↔ spoke configs,
good/bad colorings ↔ realisable/unrealisable σ, D-reducibility ↔
chain-pigeonhole conductivity. Honest assessment: framework gives
vocabulary and a Sage-checkable template for small tires, but does
not give a uniform argument across tire sizes.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Decomposes P_e(T'_{f'}, k) into fibers over spoke configurations σ,
specializes to the menagerie §6 formula when there are no spokes, and
sets up the cross-tire compatibility step on shared boundary spokes.
Includes brute-force-verified worked example on C_4 with four pendants.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds a new definition partitioning V(T'_{f'}) \ V(f') by geometric
location relative to the face f':
V_out(T'_{f'}) := { v in V(T'_{f'}) \ V(f') : v lies outside the
closure of f' }
= "outer spokes"
V_in(T'_{f'}) := { v in V(T'_{f'}) \ V(f') : v lies inside the
open region f' }
= "inner spokes"
These are well-defined because the boundary walk of f' is V(f') by
definition, so no element of V(T'_{f'}) \ V(f') sits on ∂f'.
In the spoke-only setting (T'_ann = C_{n+m}), the inner spokes of
the inner face are the O-side non-annular dual vertices and the
outer spokes are the source-side non-annular dual vertices (and
vice-versa for the outer face).
Paper stays at 10 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Renames Definition 1.16 from "Partial tire facial dual" to "Tire
annular face connector" to match the family of "tire annular ..."
terminology (cf. Definition 1.15 "Tire annular subgraph").
Symbol T'_{f'} unchanged.
Updates:
- Definition 1.16 title and body wording
- Label changed to def:tire-annular-face-connector
- Figure suptitle in fig_facial_dual_choices.png
- Module docstring of draw_facial_dual_choices.py
Paper stays at 10 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Revert the previous renaming of G'_ann; the symbol is back to
T'_ann. The CONCEPT NAME is changed from "annular dual subgraph"
to "tire annular subgraph" to clarify it's the tire's annular
portion as seen in G'.
Updates:
- Definition 1.15 retitled "Tire annular subgraph"
- Label changed to def:tire-annular-subgraph
- Cross-references in Definition 1.16 and the spoke-only remark
- Figure suptitle reverted to T'_ann
- Regenerated fig_facial_dual_choices.png
Paper stays at 10 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Splits the old Definition 1.15 (which combined the annular dual
subgraph and the partial tire facial dual) into two separate
definitions:
Definition 1.15 (Annular dual subgraph):
G'_ann := G'[{d_f : f ∈ F_ann}], with planar embedding inherited
from G'. Renamed from T'_ann to G'_ann (since it's an induced
subgraph of G', not of T).
Definition 1.16 (Partial tire facial dual):
T'_{f'} := closed G'-neighborhood of V(f') with every G'-edge
incident to V(f'), for f' a face of G'_ann.
Updates all references in paper.tex and in the Figure 5 caption /
figure title; regenerates fig_facial_dual_choices.png.
Paper stays at 10 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds fig_facial_dual_choices.png showing T'_{f'} for the three faces
A, B, C of T'_ann = θ(1, 3, 3) in the bridge case:
Face A (outer): V(A) = all 6 vertices; T'_A pulls in all four
external neighbors u_1, u_2, u_4, u_5.
Face B (inner right): V(B) = {v_0, v_1, v_2, v_3}; T'_B pulls in
only u_1, u_2 and the cycle-neighbors v_4, v_5.
Face C (inner left): mirror image of B.
The figure also visually conveys that the chord endpoints v_0, v_3
(= the two annular faces sharing the bridge edge) have all three
G'-edges inside T'_ann, so neither contributes an external u_v.
Adds:
- experiments/draw_facial_dual_choices.py
- notes/fig_facial_dual_choices.png
- Figure 5 in paper.tex referencing the new image.
Paper grows from 9 to 10 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds a new definition formalizing the "partial tire facial dual" T'_{f'}:
(i) Annular dual subgraph T'_ann := G'[{d_f : f ∈ F_ann}], with
planar embedding inherited from G' (where G' is the inner
planar dual of the maximal planar G).
(ii) For each face f' of T'_ann in its inherited embedding,
T'_{f'} := closed G'-neighborhood of V(f') together with
every G'-edge incident to V(f').
Adds a remark noting that in the spoke-only case T'_ann = Γ ≅ C_{n+m}
has two faces (both with V(f') = all interior dual vertices), and
T'_{f'} recovers the planar dual of T when G is the tire plus one
source-side and one O-side face.
Paper stays at 9 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds a 'General method' paragraph to menagerie §6 describing how to
compute P_e(G, k) for any G = C_n + (matching of non-crossing chords):
P_e(G, k) = Σ_{(c_1,...,c_r)} N(C_n; forbidden(c_1,...,c_r), k)
where the sum is over chord-color assignments and N counts proper
k-edge-colorings of C_n subject to per-edge forbidden colors (= the
chord colors at adjacent chord endpoints). For each chord-color
choice the inner count is a transfer-matrix product on the polygon,
computed in O(n k^2) time, so the full polynomial is computable in
O(n k^{r+2}) time.
The method specializes to the closed form for θ(1, p, q) (r = 1) and
generalizes to any number of non-crossing chords. Verified against
Sage's chromatic polynomial of the line graph on:
- θ(1, 3, 3): 30
- C_8 + {(0,2), (3,7), (4,6)}: 6
- C_10 + {(0,2), (3,5), (6,8)}: 18
Note grows by ~1/2 page; still 5 pages total.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds a worked example: G = C_8 with three non-crossing chords
{(v_0,v_2), (v_3,v_7), (v_4,v_6)}. Walks through the calculation
of P_e(G, 3) by propagating constraints:
1. Fix chord c_0 = a (3 choices).
2. Forces {c(e_0), c(e_7)} = {b, c} and {c(e_1), c(e_2)} = {b, c}
at v_0 and v_2; cycle constraint at v_1 ties them together.
3. Propagating to chord 3-7 forces c_3 = a and the adjacent
cycle edges to alternate {b, c}.
4. Propagating to chord 4-6 forces c_4 = a and cycle edges
continue the alternation.
Result: cycle edges alternate b, c around C_8 (OK since |C_8| is
even); all 3 chords get the same color a. Total proper 3-edge-
colorings: 3 (choice of a) × 2 (b/c assignment) = 6, verified by
Sage's chromatic-polynomial computation on L(G).
Note that the graph admits a UNIQUE proper 3-edge-coloring modulo
permutation of the 3 colors -- the chord structure forces all
three chords to take the "third" color absent on the polygon cycle.
Adds:
- draw_3chord_example.py
- fig_3chord_example.png
Paper grows from 4 to 5 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds fig_theta133.png illustrating the polygon-with-one-chord case:
hexagon C_6 with the chord between v_0 and v_3 (the two trivalent
vertices), edges colored with a valid proper 3-edge-coloring using
the 3 colors a, b, c. Replaces the previous bracketed placeholder
text in §6 of menagerie.tex.
Adds draw_theta_133.py generator script.
Paper stays at 4 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
θ(1, p, q) IS in the menagerie (= subcubic outerplanar), so the
section about θ being outside no longer applies. Removed:
- menagerie.tex: the entire 'Outside the menagerie' section.
- generate_figures.py: fig_theta function and its main() call.
- fig_theta.png: orphaned figure file.
Note: the paper now ends cleanly with the block-cut decomposition
section. 4 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
User correctly pointed out:
(1) The Figure 4 partial-tire-dual interior structure is not a "theta
graph" in the K_{2,3} sense (which requires all three paths of
length ≥ 2). It is θ(1, 6, 6): a 12-cycle with one chord.
(2) θ(1, p, q) IS outerplanar (just a polygon with one chord), so it
belongs IN the menagerie, not outside it.
Revisions:
- Section 6 ("2-connected outerplanar with Δ ≤ 3"): previously claimed
the class is just cycles; corrected to "cycle, possibly with a
matching of chords." Added explicit description of θ(1, p, q) and
a closed-form for its proper 3-edge-coloring count:
P_e(θ(1,p,q), 3) = (2^{p+q} - 2^p (-1)^q - 2^q (-1)^p + 10 (-1)^{p+q}) / 3.
Verified against Sage's chromatic polynomial for all p, q ∈ {2..6}.
- "Outside the menagerie" section: previously said "theta graphs (all
flavours) are not outerplanar." Corrected to clarify that only
θ(p, q, r) with all three paths of length ≥ 2 (= K_{2,3} subdivisions)
is not outerplanar. Explicitly noted that the bridge-case partial
tire dual gives θ(1, p, q) which IS in the menagerie, with edge-3-
coloring count given by the closed form.
The Figure 4 partial-tire-dual (m=4 outer cycle + barbell O with
bridge) has θ(1, 6, 6) as its interior dual subgraph and so admits
exactly 1326 proper 3-edge-colorings on the interior cycle-with-
chord; leaves contribute their forced colors as in the spoke-only
case.
Paper unchanged. This is a correction within the notes/ subdir only.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Standalone 4-page LaTeX note in notes/menagerie.tex with figures
generated by notes/generate_figures.py, summarizing edge 3-coloring
counts for the menagerie of subcubic outerplanar graphs:
- Path P_n: P_e(P_n, 3) = 3 · 2^{n-2}.
- Cycle C_n: P_e(C_n, 3) = 2^n + 2(-1)^n.
- Star K_{1,3}: P_e = 6.
- Corona C_n ∘ K_1: same as C_n (leaves are forced).
- Trees with Δ ≤ 3: product over BFS-order via greedy.
- 2-connected blocks: just cycles (chords force Δ > 3 generically).
- Block-cut tree decomposition for general subcubic outerplanar.
- Outside the menagerie: theta(2,2,2) = K_{2,3} (not outerplanar),
which is the interior-dual structure of D(T) when O has a bridge.
The note is meant as a quick reference for the partial-tire-dual
paper, particularly for the spoke-only case (corona) and as
motivation for the theta-graph carve-out in the bridge case.
6 small PNG figures included.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The previous bridge example used a pendant edge as the bridge. A
pendant edge IS technically a bridge (single-edge cut), but the
intended notion was a "proper" non-pendant bridge: an edge cut
connecting two non-trivial subgraphs. Replaced with the smallest
example:
- B_out = 4-cycle on {0, 1, 2, 3}.
- O = barbell on {4..9}: two disjoint triangles {4, 5, 6} and
{7, 8, 9} connected by the bridge edge 6-7.
- Annular triangulation by hand (12 triangles, all listed in the
generator script with planarity verified by Sage).
The barbell case is structurally cleaner: BOTH endpoints of the
bridge have degree >= 2 in O, and the interior dual subgraph has
the two bridge-incident annular faces (d_5, d_6) as its trivalent
theta-graph vertices (in the pendant case, the trivalent vertices
were NOT bridge-incident, which was confusing).
Updates fig_partial_tire_dual_bridge.png and the figure caption.
Paper stays at 9 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds fig_partial_tire_dual_bridge.png beneath the existing partial-
tire-dual figure (Figure 3). The new figure shows a tire graph
whose inner outerplanar O has a bridge:
B_out = triangle on {0, 1, 2};
O = triangle {3, 4, 5} plus pendant edge 5-6 (the bridge);
annular triangulation with 8 triangles (constructed by hand).
Key contrast with the previous figure: because both faces incident
to the bridge are annular triangles, the bridge contributes an
INTERIOR DUAL EDGE rather than two leaves. Consequently the
interior dual subgraph is no longer a single (n+m)-cycle (as in
Prop 1.8 for spoke-only tires) but a theta graph: two trivalent
d_f vertices connected by three internally vertex-disjoint paths.
Leaves come only from B_out (3 of them) and the three non-bridge
triangle edges of O (the inner-triangle face boundary).
Adds experiments/draw_partial_tire_dual_bridge.py to generate the
figure.
Paper grows from 8 to 9 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds Proposition 1.13 (Edge-vertex coloring bijection for D(T)): for
a tire graph T satisfying the spoke-only hypothesis of Prop 1.8 (so
D(T) ~= C_{n+m} ∘ K_1), the number of proper 3-edge-colorings of D(T)
equals the number of proper 3-vertex-colorings of its interior dual
subgraph Γ ~= C_{n+m}, and both equal 2^{n+m} + 2 · (-1)^{n+m}.
Proof: Two bijection steps.
Step 1: Restriction is a bijection between proper 3-edge-colorings
of D(T) and proper 3-edge-colorings of the cycle C_L (where
L = n+m), because at each d_f the leaf's color is forced to be
the unique third color absent from the two cycle edges, and
leaves impose no further constraint.
Step 2: Proper 3-edge-colorings of C_L = proper 3-vertex-colorings
of L(C_L) = proper 3-vertex-colorings of C_L (since L(C_L) ~= C_L).
Step 3: Chromatic polynomial of C_L at k=3 is 2^L + 2 · (-1)^L.
Adds Remark 1.14 noting the closed form depends only on n+m, not
on the specific spoke-only annular triangulation or chord structure
of O.
Empirically verified for L in [3, 10] via Sage's chromatic
polynomials: edge-3-colorings of D(T) = vertex-3-colorings of C_L
= formula in every case.
Paper grows from 7 to 8 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The complete tire dual D*(T) and Tait correspondence material was
giving exact counts but only via Tait colorings with XOR-to-0
conditions at high-degree vertices -- not proper edge colorings,
which was the original goal. Removed:
- Definition 1.13 (Complete tire dual) and its figure.
- Proposition 1.14 (Tait correspondence on complete tire dual).
- Remark 1.15 (Tait construction).
- Remark 1.16 (octahedron verification).
- Tait1880 bibitem (no longer cited; the body-text mention of
Tait's theorem in the introduction remains).
- experiments/draw_complete_tire_dual.py + its PNG.
- experiments/draw_tait_coloring_example.py + its PNG.
- fig_complete_tire_dual.png from the paper root.
The partial tire dual definition (Def 1.7), structure proposition
(Prop 1.8), figure, and associated scripts (tire_graph.py,
draw_partial_tire_dual.py) are retained.
Paper shrinks from 9 to 7 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds fig_complete_tire_dual.png next to Definition 1.13 of the
complete tire dual. The figure uses the same m=6, k=4 spoke-only
tire as the partial-tire-dual figure (so the two figures can be
directly compared), with the n=6 outer leaves merged into a single
outer-face vertex v_out (blue hexagon, drawn outside the tire) of
degree 6, and the m=4 inner leaves merged into a single inner-face
vertex v_in (red hexagon, drawn at the centre of the inner cycle)
of degree 4.
Generator: experiments/draw_complete_tire_dual.py.
Paper grows from 8 to 9 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The previous Proposition (Tait correspondence on partial tire dual)
stated equality between non-equivalent 4-vertex-colorings of T and
non-equivalent 3-edge-colorings of D(T). This is wrong as
empirically verified on the octahedron (n=m=3, O=C_3, spoke-only):
- Octahedron: 96 4-vertex-colorings -> 4 classes mod S_4.
- Partial tire dual C_6 ∘ K_1: 66 3-edge-colorings -> 11 classes
mod S_3.
Replaces that proposition with a variant on the COMPLETE tire dual
D*(T) that incorporates non-annular constraints:
Definition 1.13 (Complete tire dual): Quotient D(T)'s leaves into
non-annular-face vertices. Outer leaves merge into a single
outer-face vertex v_out of degree n; for each bounded face F of
O interior to B_in, the corresponding inner leaves merge into
v_F of degree |F|. Equivalently, D*(T) is the planar dual of T.
Proposition 1.14 (Tait correspondence on complete tire dual): the
number of non-equivalent 4-vertex-colorings of T (mod S_4) equals
the number of non-equivalent Tait colorings of D*(T) (mod S_3).
A Tait coloring is an edge labelling by the three nonzero elements
of Z_2 x Z_2 with XOR-to-0 at every vertex of D*(T).
Remark 1.16 (octahedron verification): For octahedron tire,
D*(T) is the cube Q_3. Octahedron has 4 vertex-coloring classes;
Q_3 has 24 proper 3-edge-colorings -> 4 Tait-coloring classes.
Empirically verified via Sage:
- chromatic_polynomial(octahedron)(4) = 96
- chromatic_polynomial(L(Q_3))(3) = 24
The partial tire dual definition (Def 1.7) and its corona-graph
structure proposition (Prop 1.8) are unchanged.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds Proposition 1.13: the number of non-equivalent proper 4-vertex-
colorings of a tire graph T (mod S_4) equals the number of non-
equivalent proper 3-edge-colorings of its partial tire dual D(T) (mod
S_3). The map is the classical Tait XOR construction: identifying
the four colors with Z_2 x Z_2, each edge of T receives an edge color
equal to the XOR of its endpoint colors, which lies in the three
nonzero elements of Z_2 x Z_2 -- giving the corresponding edge of
D(T) a 3-edge-color. Annular triangles of T, encoded as degree-3
vertices d_f of D(T), supply the three-distinct-colors constraint.
Adds Remark 1.14 explaining the analogy with Tait's classical
correspondence.
Adds Tait 1880 bibitem (Proceedings of the Royal Society of Edinburgh,
vol. 10).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds fig_partial_tire_dual.png next to Definition 1.7 (Partial tire
dual), illustrating the corona-graph structure C_{n+m} ∘ K_1 from
Proposition 1.8 on a concrete m=6, k=4 spoke-only tire.
Drawing details:
- d_f interior vertices (purple squares) at centroids of annular
triangles; the 10 of them form a 10-cycle (solid purple edges).
- B_out leaves (orange diamonds) placed outside B_out; the leaf edge
is dashed orange.
- B_in leaves placed on the central-hole side of each red edge, at
a fixed small offset past the midpoint of the edge in the
d_f -> midpoint direction. This positions each leaf edge to
cross its red edge exactly at the midpoint while keeping the leaf
vertex itself inside the central hole and off the border.
Generator: experiments/draw_partial_tire_dual.py (also committed).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
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>
didericis