Record the partition sweep on the n=24 Fig 2.10 dual. New subsection +
experiments/bridge_partition_sweep.py.
Findings:
- A bridge switch is a constrained diagonal flip; bridge-derived via L
means lying in an Even-Level-Graph component of the restricted flip
graph. So the question is which flip-components contain an ELG.
- Identity: every 4-coloring of a triangulation has e_cross = 2n-4 (each
face has one within-pair edge), so total parity-subgraph Betti =
(c_A+c_B)-2; intertwining trees are the Betti-0 case.
- Of T's 333 valid partitions, total Betti splits 288/42/3 over 1/2/3;
min is 1 (T not intertwining). All 27 partitions found bridge-derived
(depth 2-3) have the minimum Betti 1 -> necessary.
- But not sufficient: only 27 of 288 Betti-1 partitions yield a witness;
the rest have flip-orbits >1.5e5 with no ELG, and a 12x budget increase
found none. The discriminator is flip-component structure (sharp
orbit-size dichotomy), not a numerical invariant. Characterizing which
Betti-minimal partitions sit in an ELG component is left open.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
New paper introducing the dual (inner/weak dual) of a maximal planar graph,
dual depth (BFS-derived min level over a face's vertices), and a Tait-based
framing of a minimal 4CT counterexample via nested level duals. Includes a
dual-depth figure and its generator. Shelved per closing note in favour of an
alternative approach.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Retitle to "Even Level Graph Generators: a constructive conjecture
stronger than the Four Color Theorem" and state explicitly in the
abstract and introduction that the conjecture implies the four color
theorem but is strictly stronger: a 4-coloring grouped {1,2}|{3,4} is
exactly a partition into two bipartite-inducing parts, so 4CT is the bare
existence of such a partition, whereas the conjecture demands it be
realized constructively (bridge-switch level parity, or two induced
trees). Hence a proof is a new constructive proof of 4CT, and the
conjecture is at least as hard -- very likely harder.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add the n=24 result to the Even Level Graph Generators paper: the dual of
the unique 44-vertex non-Hamiltonian cyclically-5-connected cubic planar
graph (Holton-McKay Fig. 2.10) -- a 24-vertex 5-connected triangulation,
the first conjecture test outside the 3-cut family -- is a bridge-derived
level graph, two verified bridge switches from an Even Level Graph
(source 19).
- Generate the graph rather than transcribe it: plantri -c5 lists all 6833
5-connected 24-vertex triangulations; exactly one has a non-Hamiltonian
dual, which also settles the uniqueness Holton-McKay left open at 44
vertices (cyclically-5-connected triangulation <=> dual cubic graph).
- New abstract sentence + "cyclically-5-connected case: n=24" subsection,
noting the classic 46-vertex Tutte graph is only cyclically 3-connected.
- Figure 6 (figures/fig210_dual.png): the dual T, parity-coloured, with the
two introduced bridge edges {6,19} and {20,22} in green (style of Fig. 5).
- Experiments: test_fig210_dual_bridge.py (generate->filter->test pipeline),
verify_fig210_witness.py (step-verifies the witness), draw_fig210_dual.py
(figure), fig210_dual.g6 (the unique graph). paper.pdf rebuilt (10 pages).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Records, for 4<=n<=11, triangulation iso classes, how many admit an ELG
source, ELG iso classes, and the automorphism-free flag-rooted count
sum_G 4E/|Aut(G)| * s(G). Computed by experiments/count_elgs.py.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
count_elgs.py enumerates triangulation iso-classes and counts Even Level
Graphs (G,v) per n: iso-classes (sources up to Aut) and flag-rooted
(4E/|Aut| * s, an exact integer since Aut acts freely on flags).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
experiments/test_tutte_bridge.py: bridge-derivability test for the dual of
the 46-vertex Tutte graph (a 25-vertex non-intertwining triangulation,
since the Tutte graph is non-Hamiltonian) -- the conjecture's first case
beyond the n=21 Holton-McKay duals. Reuses the fast integer-state bridge
engine: per source labelling with bipartite parity subgraphs, run a
backward bridge-orbit BFS for an Even Level Graph witness.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The smallest non-Hamiltonian 3-connected cubic planar graphs have 38
vertices (J. Combin. Theory Ser. B 45:305-319). Reference for the
even_level_graph_generators conjecture: via the intertwining-tree =
Hamiltonian-dual equivalence, the duals of the non-Hamiltonian C3CPs
classified here are exactly the triangulations the conjecture must
reach through the bridge-derived-level-graph disjunct.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Frame the paper's purpose: ask whether two constructive families of
4-colorable triangulations -- bridge-derived level graphs (parity
2-coloring) and intertwining trees (two trees, disjoint color pairs) --
suffice to generate every maximal planar graph on n vertices. An
affirmative answer would be a constructive proof of the four color theorem
for triangulations. State the duality bridge to Tait/Holton-McKay and the
n=21 confirmation.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Drop the n<=9 bridge-derived classification table and its surrounding
discussion; the n=21 boundary case now follows directly from the
trivial-below-21 observation.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Remove the witness-ELG figure (former Fig. 5); keep the six resulting duals
with their introduced green bridge edges. Fix the dangling cross-reference
in the caption.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Replace the radial (crossing-heavy) figure with two crossing-free planar
drawings (networkx planar_layout / Chrobak-Payne):
fig:n21-elgs -- the six witness Even Level Graphs, parity-coloured, with
the bridge-switch-flipped edges dashed red;
fig:n21-duals -- the six resulting duals, with the introduced bridge edges
solid green.
ELG and dual are drawn with independent planar layouts so neither has any
edge crossing (a flip diagonal would otherwise cross other edges when its
quadrilateral is non-convex, which happens for duals 0 and 3). Drop forced
equal aspect so panels fill and labels separate.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Figure fig:n21-witnesses: each of the six Holton-McKay duals drawn as its
witness Even Level Graph in a radial-by-level layout (source centre,
level-k vertices on ring k), coloured by parity. Dashed red edges are the
flipped same-parity edges and solid green edges the introduced bridges;
applying the switches yields the dual. Duals 1,2 are ELGs outright.
draw_witnesses.py generates the combined 2x3 figure and per-dual PNGs from
the verified witness JSONs.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Table tab:n21 records, for each of the six duals: not an intertwining tree;
Even Level Graph source (duals 1,2 only); and bridge-switch path length to
an ELG (0,0 for the two ELG-outright cases; 3,1,2,4 for the rest). All six
are bridge-derived; all witnesses step-verified.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Tested duals 1 and 2: both are Even Level Graphs directly (dual 1 for
source 10, dual 2 for source 9), so bridge-derived with a zero-length
switch sequence. All six Holton-McKay duals are confirmed non-intertwining
(consistent with the dual-Hamiltonian theorem, since all six HM graphs are
non-Hamiltonian) and all six are bridge-derived. Saved witness files
dual_1.json, dual_2.json (0 switches) to complete the archive for all six.
Updated the n=21 subsection accordingly.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Conjecture now reads "bridge-derived level graph ... an intertwining tree,
or both" -- the stronger form the evidence actually supports (a bridge-
derived level graph is automatically a valid derived level graph).
- Empirical table recomputed for bridge-derivability, exhaustively for n<=9
(every backward bridge-orbit fully enumerable there):
n=7: 1 inter-only; n=8: 2 inter-only; n=9: 14 inter-only; missing=0.
Added prose: below n=21 every class is intertwining, so the table shows
how far the bridge-derived disjunct reaches on its own (36/50 at n=9) and
that the two disjuncts complement each other; "bridge only" is 0 in range.
- n=21 subsection notes the four witnesses are explicit, short (path lengths
3,1,2,4), archived, and step-verified.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The hunt only logged partition indices; the actual witness ELGs were lost.
Re-extract them (deterministic) with full bridge-switch paths and verify
every step independently. Saved as experiments/witnesses/dual_<i>.json
(labels, ELG source, ELG + dual graph6 and edge lists, the explicit
remove/add bridge-switch sequence, verified flag). All four verify:
dual 0: ELG source 18, 3 bridge switches to dual
dual 3: ELG source 16, 1 bridge switch to dual
dual 4: ELG source 20, 2 bridge switches to dual
dual 5: ELG source 1, 4 bridge switches to dual
So each dual is only a handful of bridge switches from an Even Level Graph,
and the witnesses are now reproducible and human-checkable.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Add the figures for the n=7, idx=2 missing-isomorphism case
(missing_iso_n7_idx2.png is included in paper.tex), plus its
4-coloring and level-decomposition companions and the G-for-T
preimage graph. Rebuild paper.pdf and its LaTeX aux/log/out.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Backward bridge-switch search (sharded over valid parity partitions) found
an Even Level Graph witness for each of the four previously-open duals:
dual 0: partition 12, witness orbit 9458
dual 3: partition 9, witness orbit 388
dual 4: partition 23, witness orbit 3842
dual 5: partition 12, witness orbit 165668
So all four are bridge-derived level graphs, hence valid derived level
graphs. Combined with the two duals that are Even Level Graphs outright,
the disjunction is now confirmed for ALL SIX critical iso classes at n=21
-- the first nontrivial test of the conjecture passes.
Why it worked where exhaustion failed: a witness, when it exists, tends to
sit in a SMALL orbit (here a few hundred to ~1.7e5 states) reachable
quickly, while other parity partitions of the same triangulation have
orbits >1e6. We only need one good partition. The bridge restriction both
shrinks orbits ~100x and guarantees validity, so any ELG found in a
backward orbit is an immediate witness.
- Update paper n=21 subsection to report the resolution.
- Add shard_hunt.py (partition-sharded parallel witness hunt).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Relocate the standalone Python scripts from the repo root into the
experiments/ folder of the paper each one belongs to:
plane_depth_sequencing/experiments/
plane_depth_sequencing.py, draw_quad_sequence.py,
draw_quad_sequence_diagram.py, extract_sequence.py,
plane_depth_sequencing_figure.py, quad_sequence_coloring_check.py
colored_edge_flip_classes/experiments/ colored_edge_flip_class_survey.py
colored_pentagon_contractions/experiments/ colored_pentagon_contractions.py
plane_diamond_coloring/experiments/ plane_diamond_coloring.py
Each file that imports lib.* (still in the repo root) or the sibling
plane_depth_sequencing module gets a sys.path shim that prepends the
repo root (computed three levels up) and, where needed, its own dir.
Imports verified to resolve from a neutral working directory.
flip_symmetric_census.py is intentionally left in the root.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Findings at n=9 (50 triangulations, orbits fully exhaustible):
- 36 bridge-derived, 14 NOT bridge-derived. So bridge-derived is a PROPER
subclass of derived (49 derived at n=9). All 14 non-bridge graphs are
intertwining trees -- as are all 50, necessarily: intertwining tree
<=> dual Hamiltonian, and the smallest non-Hamiltonian 3-connected cubic
planar graph has 38 vertices, i.e. dual on 2n-4=38 => n=21. Hence every
triangulation with n<=20 is an intertwining tree, and the disjunction
"bridge-derived OR intertwining" is trivially true below n=21. The 4
Holton-McKay duals are the first non-intertwining triangulations.
- Static parity-subgraph invariants (Betti numbers, component counts,
cross-edge count, existence of an all-forest partition) do NOT separate
bridge-derived from non-bridge-derived -- both classes realize beta=0
partitions and identical ranges. Bridge-derivability is dynamical, not a
simple static invariant; no easy obstruction.
- Side lemma: every valid parity partition of an n-vertex triangulation has
exactly 2n-4 cross edges (intra-edges = n-2). Holds for all n=9 graphs.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- fast_bridge.py: states as 210-bit integer edge-bitmasks (compact memory,
O(1) set ops); build a NetworkX graph only once per state for the planar
embedding; parity-subgraph bridges via one iterative DFS per state instead
of per-edge subgraph copies. Validated identical orbits to the slow version;
throughput ~5170 states/s vs ~1100 (graph.copy was 66% of old runtime).
- fast_decide.py: integrated, gated ELG-witness check (only even-class
sources with all-opposite-class neighbourhoods are tested with the
ground-truth is_even_level_graph, then parity match). Witness detection
validated (ELGs -> True, T*_9 -> False).
- Feasibility finding: bridge orbits are ~100x smaller than full E/O orbits
but still 1e5-1e6 states per labelling (partitions 0,1 of dual 0 exceed
310k and 685k without exhausting), x ~150 valid parity partitions per dual.
Exhausting every orbit -- required for a conclusive NEGATIVE -- is
computationally infeasible. A conclusive POSITIVE (witness ELG) remains
reachable; none found so far.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Update abstract and coverage table: computational evidence now includes n=12
(previously n=6..11). All iso-classes remain reachable.
- Correct conjecture statement: minimum degree ≥5 (not ≥4).
- Add graphicx package (for potential figure support).
- Add exploratory experiment files for exception characterization, preimage
search, and visualization (directed toward understanding the full orbit
of the T*_9 case and related structural questions).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Define bridge switch (E/O switch whose new same-parity edge is a bridge
in its parity subgraph) and bridge-derived level graph in the paper.
Note that bridge switches preserve bipartite parity subgraphs, so every
bridge-derived level graph is automatically valid.
- Discover the E/O-switch relation is directed (irreversible when a switch
produces a cross-parity edge); T*_9 reaches an ELG forward but no ELG
reaches it, explaining why it is not derived. This rules out a simple
switch-invariant characterization.
- Bridge orbits are far smaller than full E/O orbits (~10^4 vs ~10^8 for
some labellings), making exhaustive search feasible. Each of the 4 open
duals has ~150 valid parity partitions; exhaustive bridge-orbit search
per partition can decide bridge-derivability conclusively.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Add Theorem: maximal planar G is an intertwining tree iff its dual
G* is Hamiltonian (Tait-style Jordan-curve argument). Consequence:
smallest non-intertwining-tree triangulations are the 6 duals of the
38-vertex Holton-McKay graphs, at n=21.
- Load the 6 graphs from McKay's authoritative planar_code file
(nonham38m4.pc), verified: 38 vertices, cubic, planar, non-Hamiltonian.
- All 6 duals confirmed not intertwining trees (exhaustive 2^20 check).
- 2 of 6 duals are themselves Even Level Graphs (sources 9, 10), hence
derived level graphs -- first cases where the derived disjunct does
work the intertwining-tree disjunct cannot.
- Remaining 4: bounded E/O-orbit search inconclusive; status open. This
is the first genuinely undetermined instance of the conjecture.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Disjunction (every maximal planar graph is a derived level graph or
intertwining tree) holds through n=12. New intertwining-only iso class
at n=12 (analog of T*_9 at n=9) brings the count of derived-resistant
iso classes to 2 in this range. Per the intertwining-tree ⟺
Hamiltonian-dual equivalence, intertwining-tree failures cannot occur
until n=21 (dual of the 38-vertex Holton-McKay minimum Tait
counterexample).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- New paper papers/even_level_graph_generators/: defines Even Level
Graph (every level cycle even), derived level graphs, intertwining
trees, and the disjunction conjecture (every maximal planar graph is
a derived level graph or intertwining tree). Empirically tested
through n=11: every iso class is at least an intertwining tree, so
the disjunction holds trivially in this range. The intertwining tree
disjunct fails at the Tutte graph dual (n=25), so the disjunction
becomes non-trivial past some unknown threshold.
- Level Switching paper: adds Section 4 (Reachability via edge
switches) with the two-step argument (Sleator-Tarjan-Thurston for
Case 1; face-merges for Case 2) and Theorem 4.1 (O(n) edge switches
suffice to reach all-depth-0).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Stress-tests the iterated preprocessing algorithm on random
maximal-outerplanar triangulations: terminates on n<=60 within bounded
steps, occasionally hits step cap at n=80 with random edge choice.
Scaffolds the user-proposed v_c-rotation algorithm and documents the
monovariant findings (lexicographic depth signature is weakly but not
strictly decreasing under preprocessing).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Add 21-vertex and 24-vertex examples showing recursive lopsidedness
at d=2. Empirically confirm that the iterated algorithm (balanced
switch when available, preprocess otherwise) drives every face to
depth 0 on all tested configurations. Frame the remaining open
question as identifying a strictly-decreasing monovariant under
unbalanced preprocessing switches.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Defines level cycles, edge switches, surface switches, and facial depth
on level components of plane triangulations. Proves outerplanarity of
level components and a depth-descent lemma. Introduces balanced surface
switches and proves they remove a depth-d level cycle while creating
1-2 new depth-(d-1) cycles. Documents the 9-vertex counterexample where
no balanced switch exists and sketches preprocessing toward
balancedness, leaving general termination open.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Section 5.6 sketches an inductive route to the simple-resolution md4
surjectivity conjecture:
- Lemma 5.8 (good contraction): every md4 triangulation on n >= 7
vertices has a degree-4 vertex with an md4-preserving diagonal
contraction. Empirically true at n=7..11; proof obligation called
out.
- Lemma 5.9 (lift): given a labelled preimage of the contracted
triangulation, reinserting the contracted vertex at the
diagonal-bounded quadrilateral yields a preimage of the original
triangulation. Proof obligation called out.
- Inductive scheme paragraph chains the two lemmas with the octahedron
at n=6 as the base case, citing the n=7 hand-verification (already
scripted in experiments/inductive_lift_check.py).
Lemmas are stated without proof; the three remaining proof
obligations are explicit.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Generalize Phase 1 to include even interior faces as optional flip
candidates and allow the source-triangle break in $L_0$ to be skipped;
generalize Phase 2 so even outer-incident cycles may have at most one
outer-face edge flipped (odd cycles still must have one).
- Define "simple level resolution" as a triangulation $G'$ obtained from
some $(G, S)$ via the algorithm with bipartite parity subgraphs
(Definition 5.4).
- Add Conjecture 5.7 (simple-resolution md4 surjectivity) and
Observation 5.6: every minimum-degree-4 plane triangulation iso-class
on $n \in \{6, ..., 11\}$ vertices is reached as a simple level
resolution. Counts: 1, 1, 2, 5, 12, 34. The md4 restriction is
necessary -- specific non-md4 iso-classes (iso 5 at n=8; iso 25, 183
at n=10) are not reachable.
- Add experiments/simple_level_resolution_coverage.py implementing the
branched algorithm and coverage check, plus supporting scripts for
Phase 1 cycling debugging, Phase 2 gap diagnosis, inductive-lift
scaffolding (inductive_lift_check.py for the route-1 proof strategy),
and visualizations of the unreached n=10 iso-classes and the original
Phase 2 gap example.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- Promote Prop 3.1 (outerplanarity of level subgraphs) to Theorem 3.1
with a proof by contradiction via a BFS-path argument; drop the
$n \leq 10$ caveat and the now-resolved open question.
- Add Section 5 "An edge-flip resolution algorithm": apex classification
of $L_k$-edges, bridge lemma, cross-level flip pass, definition of
tricky-everywhere odd cycles and facial depth (seeded from inner
faces with $\geq 2$ outer-face edges), and the depth-guided flip
procedure. Observation 5.5 records empirical termination at
$n = 9, 10, 11$; Question 5.6 asks if it holds in general.
- Add experiments/depth_monovariant_check.py (sanity check over
triangulation iso-classes, confirms the count-of-tricky-faces
monovariant strictly decreases per flip on all 1400 tricky configs
at $n \leq 11$), viz_cycling.py and debug_cycling.py, and
cycling_visualization.png illustrating the depth-definition fix.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Embed a worked example of the canonical quadrilateral sequencing into the
paper. The new figure shows the deep embedding of a 9-vertex triangulation
with each quadrilateral filled by type (shallow diamond, deep diamond, S
quad) and annotated with its sequence index and move code. The generator
script renders the figure from a fixed Sage RNG seed for reproducibility.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds a Motivation section to paper.tex explaining that the
quadrilateral sequencing is intended to support an inductive 4-coloring
of the underlying maximal planar graph, with ring completion as the
suspected obstacle.
Adds commentary.tex recording (a) why a pure pigeonhole argument is
unlikely to close the conjecture, (b) the observation that under any
strictly local online rule every G'-edge constraint is enforced when
its second endpoint is colored (so ring completions cannot fail at the
moment they fire), and (c) the empirical finding that pure greedy
fails at non-ring-completion moves on every 3-connected triangulation
of order 5-7.
Adds quad_sequence_coloring_check.py, an enumeration check over small
triangulations via Sage's planar_graphs that runs greedy online
4-coloring under the canonical sequence and classifies failures.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds extended_deep_embedding (subdividing the outer face with an outer-cap
vertex), quadrilateral_decomposition (pairing faces across level edges),
and quadrilateral_sequencing which runs the anchor drop / level add /
join / ring completion precedence with bottommost-on-the-canonical-
boundary-walk tiebreaks and a lex-smallest move-code-string choice for
the initial quad.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Extend the deep embedding to include the outer face, decompose into
quadrilaterals via level-edge pairing on the sphere, and define a
deterministic sequence built from four moves (anchor drop, level add,
join, ring completion) with a recursive lex-smallest tiebreak on the
initial quadrilateral. Attempt the termination theorem and the per-move
case analyses.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Iterates min-degree-5 maximal planar graphs and, for each one G, looks
for any flip-neighbor H and proper 4-coloring phi of H satisfying the
Kempe-locked structure of Lemma 4.3 (phi(u)=phi(v) plus an {a,b}-Kempe
chain for every other color b). For each such (H, phi), BFS the
colored edge flip class with a 50,000-graph cap and test reached
graphs for isomorphism to G. Saves the first G for which no such (H,
phi) has G in its colored class.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Remove the flip-symmetric definition, the class $\mathcal{F}$, and
all references to flip-symmetry from the abstract, motivation, and
section 3 title. Section 3 is renamed to reflect what remains: the
flip neighborhood and the colored edge flip class. The principal
theorem's label is renamed to thm:flip-neighborhood-4colorable to
match its statement.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The original framing presented flip-symmetry as the principal
property and the stronger statement (every flip-neighbor of $G_0$ is
4-colorable) as a parenthetical. Reverse the emphasis: lead with the
stronger claim, derive flip-asymmetry as a corollary, then introduce
the colored edge flip class and Theorem 4.5 to preview the
fine-grained per-coloring version of the same rigidity.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
"A minimal four-colorable counterexample" reads as "a minimal
counterexample that is itself 4-colorable", which contradicts the
section's standing hypothesis $\chi(G_0) \geq 5$. The section's
content is the structure of the flip neighborhood (and the colored
flip classes of its members) under that hypothesis, so name it that.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The original proof appealed to minimality of $G_0$ to 4-color
$G_0/uv$, but $G_0/uv$ is not in general a triangulation, so it is
not directly covered by the minimality hypothesis (which is over
maximal planar graphs). Triangulate $G_0/uv$ into a maximal planar
$T$ on the same vertex set: $|V(T)| < |V(G_0)|$, so minimality gives
$T$ a 4-coloring, which restricts to $G_0/uv$.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Defines the flip neighborhood N(G) and recasts the colored edge flip
class as a transitive closure rather than a single-step set, then
states Theorem 4.5: no colored flip class of a flip-neighbor of a
minimum-order 5-chromatic G contains G itself. The proof is one
inductive line from the definition; the theorem is intended as the
contradiction target for a future argument that some other condition
would force G into such a class.
Renames the paper (and its directory) to reflect the shift in
emphasis toward the colored edge flip class introduced last commit,
and removes the flip-symmetry frequency section: the unsigned-flip
census was a digression that the new framing no longer needs, and its
prose conclusion was at odds with the direction the paper is heading.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Removes the "Further necessary properties of a minimal counterexample"
framing section and the "Edge-deletion subgraphs" section (definition,
4-colorability theorem, Kempe-chain structure theorem). The intended
empirical follow-up on this material did not produce a useful
discriminator, so the development is being shelved.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
For G_0 a minimum-order 5-chromatic maximal planar graph and any
4-coloring of G_0 - uv, the endpoints u, v must share a color, and the
color classes pairing that color with each of two other colors must
each induce a u-v path. The Kempe-chain parts follow from a standard
swap-on-component contradiction against the shared-color claim.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Defines D(G) as the family of single-edge-deletion spanning subgraphs
of a maximal planar graph G, and shows that when G_0 is a minimum-order
5-chromatic maximal planar graph every member of D(G_0) is 4-colorable,
via a coloring pulled back from the smaller minor G_0/uv.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
didericis