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>
Adds a transitional section reframing the frequency results: the
relevant class is not all maximal planar graphs but those that resist
Kempe-style reductions, where flip-asymmetry's exclusion may have
real bite. Sets up subsequent development of additional necessary
properties of a minimum-order 5-chromatic counterexample.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The unrestricted census suggested flip-symmetry already excludes a
vanishing fraction of maximal planar graphs; this commit re-runs the
same enumeration over the minimum-degree-5 subclass (where any
minimum-order 5-chromatic counterexample must live) to check whether
the restriction tightens the bound. It does not: the density decays
to zero there as well, only at a gentler geometric rate (~0.63 per
step instead of ~0.5).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Introduces the maximal_planar_graph_edge_flipping paper, motivating
flip-symmetry as a structural restriction on minimum-order
five-chromatic counterexamples, and reports an exhaustive census
showing |F_n|/|T_n| decays geometrically (factor ~1/2 per step from
n=10 to n=14). The census driver lives in flip_symmetric_census.py.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Exhaustive enumeration at order 28 finished with exactly four maximal
planar graphs of minimum degree 5 lacking a plane diamond coloring,
out of 1,204,737 total. Adds the fourth counterexample's canonical
graph6 string and updates the figure caption.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds search_min_degree_counterexample_comprehensive iterating Sage's
planar_graphs generator with minimum_degree=5. Exhaustive enumeration
through order 27 (456,967 maximal planar graphs of minimum degree at
least 5) finds no counterexample to Conjecture 2.4. At order 28, three
counterexamples are exhibited and verified via Sage's chromatic_number
on the auxiliary graph, refuting the conjecture. Updates paper with the
refutation theorem, the per-order census, a figure of one counterexample,
and graph6 strings of the other two.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Frames the paper around the scaffold-first 4-coloring program: 2-color
the BFS-layered bipartite spanning subgraph (the diamond scaffold),
then promote select vertices with two new colors to absorb the
discarded same-layer edges. Reintroduces the diamond scaffold
definition (removed in b5a9030 along with the equivalence machinery)
since it now plays a motivational rather than definitional role.
Replaces hardcoded definition/theorem/conjecture numbers with stable
\ref{}-based cross-references.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Replaces the scaffold-mediated definition with the equivalent direct
condition (two color classes contained in opposite-parity BFS layers
from some root) and removes the scaffold definition, 2-colorability
theorem, connectedness lemma, and equivalence proposition that existed
solely to translate between the two formulations. Updates the
refutation proof to invoke the new definition directly.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds search_counterexample_comprehensive iterating Sage's planar_graphs
generator across all maximal planar graphs of bounded order. Exhaustive
enumeration through order 13 (9150+49566 triangulations) yields exactly
one graph with no plane diamond coloring, at order 13. Updates Theorem
2.6 to assert minimality and uniqueness, and replaces the figure and
edge list with the smaller counterexample.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds Theorem 2.6 stating Conjecture 2.5 is false, with proof exhibiting
a 16-vertex maximal planar graph (graph6 O???IAGKEBEQQYHdplW{n) for
which the auxiliary 4-colorability check fails at every root vertex,
verified computationally via Sage's chromatic_number. Includes the
graph as a figure and adds a McKay graph6 reference.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Extends paper with: a notation section for color-class preimages; the
plane diamond coloring definition (4-coloring whose two classes lift to a
2-coloring of some BFS-rooted diamond scaffold); a connectedness lemma
for the scaffold; a proposition reformulating the property as parity-
separation of two color classes by BFS layers; a remark noting this is
strictly stronger than 4CT; and the conjecture that every maximal planar
graph admits such a coloring.
Adds plane_diamond_coloring.py with get_plane_diamond_scaffold and a
counterexample search that reduces the per-root check to 4-colorability
of an auxiliary graph forcing two colors onto opposite parity layers.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Defines distance partition (BFS layers from a chosen vertex) and the diamond
scaffold of a maximal planar graph (G with all same-level edges removed),
then proves the diamond scaffold is 2-colorable by parity of level.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
source_graph/source_canon_id for before state, result_graph/result_coloring/result_canon_id for after state.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- Replace iterative tutte_embedding in lib with numpy direct-solve version from example.py
- Import tutte_embedding into example.py from lib instead of defining it locally
- Fix g._embedding -> g.get_embedding() in outer_face
- Add bash completion to run.sh alongside existing zsh completion
- Use nix-shell -p gcc for plantri build step on NixOS
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Replaces is_planar(set_embedding=True) calls in pluck and squish so the embedding
stays consistent with inherited positions across reduction steps.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Adds outer face detection via face traversal and signed area, Tutte embedding
for clean planar layouts, and moves g/g_prime/coloring_prime into base Operation
type. Pluck and squish now carry positions and recompute embeddings via is_planar.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
didericis