# Color-class menus and exact boundary signatures for eleven-core extensions

## 1. Contribution

The Earth–Moon problem asks for a biplanar graph requiring ten colors, or a proof that every biplanar graph is nine-colorable [1]. We prove conditional coloring theorems for the eleven-vertex core that occurs in the order-twenty-one search. The independence-three reduction of [2] explains this setting. Most conclusions use core coverage in place of an independence-number hypothesis; the three-nonunit extension and the additional four-nonunit case explicitly assume $\alpha(G)\le3$.

All graphs are finite and simple. Suppose

$$
V(G)=X\mathbin{\dot\cup}S\mathbin{\dot\cup}T,\qquad
G[X]=K_6\vee C_5,\qquad |S|=3,\quad |T|=7,
$$

where $S$ is independent. Assume that $G$ is $K_9$-free, every vertex of $X$ has a neighbor in $S$, and every vertex outside $X$ has degree at least nine. Define

$$
h=e(X,S)-11,\qquad
\beta(t)=d_G(t)-9+3-d_S(t)=d_X(t)+d_T(t)-6.
$$

Both $h$ and the $\beta(t)$ are nonnegative. Write

$$
H=\{t\in T:\beta(t)>0\},\quad
W=\{t\in T:\beta(t)>1\},\quad
J=H\setminus W,\quad q=|H|,\quad p=|W|.
$$

We call the members of $J$ unit vertices. A graph whose connected components are complete will be called a union of cliques, including the empty graph.

**Theorem 1.** Under the preceding assumptions and $e(G)\le114$, $G$ has a proper nine-coloring using exactly two colors on $S$ in any of the following cases:

1. $h=0$ and $p\le6$;
2. $h=1$ and $q\le6$;
3. $h=1$ and $p\le1$;
4. $h=1$ and $G[J]$ is not a union of cliques;
5. $h=1$, $p\le3$, and $\alpha(G)\le3$;
6. $h=1$, $q=7$, $p=4$, $\alpha(G)\le3$, and $G[J]$ is an independent triple.

For $h=1,p=2$, the proof also works without an independence-number assumption whenever $G[J]$ is disconnected.

The two possible larger defects in the earlier pair subcase, and the nonunit defects in the theorem generally, have no separately imposed upper bounds. The theorem is about the indicated graph family; it does not assert that every possible Earth–Moon counterexample has such a core.

Let $r=21-e(S,T)$, let $t=21-e(G[T])$, and put $k=r+t$.

**Corollary 2.** Under the hypotheses of Theorem 1, $h=0$ and $k\ge8$ imply nine-colorability. If $h=1$ and $G$ is not nine-colorable, then every member of $T$ has positive defect, at least two have nonunit defect, and the unit vertices induce a union of cliques. If additionally $\alpha(G)\le3$, at least four vertices have nonunit defect, and when there are exactly four, $G[J]$ is $K_3$ or $K_2\mathbin{\dot\cup}K_1$.

This replaces a total-defect threshold by structural conditions on the exceptional vertices. Version 1 proved the still-valid implication $h+\sum_T\beta\le5$ [3]. Version 2 established cases (1)–(4) and case (5) for $p\le2$. This revision covers all three-nonunit unit-clique partitions, adds case (6), and derives an independent-triple reselection principle. Its new mechanism preserves the exact common rainbow color sets at a clique boundary, where a capacity summary can lose decisive information. The reselection argument gives an ordinary nine-coloring; the finite certificate in case (6) proves the stronger two-original-$S$-color statement.

## 2. Context and distinction

Gethner and Sulanke's work on nine-critical thickness-two graphs supplies the classical construction context [4]. Szeider proves nine-colorability for biplanar graphs of independence number at most two [5]; here an independent triple is part of the setup. The classical nonbiplanarity of $K_9$, for which [6] gives a short proof, and Euler's bound explain two necessary conditions in the biplanar application.

The order-twenty eleven-core theorem [7] has six vertices outside the core and independent triple, whereas this paper has seven. Our dense order-twenty-one analysis [8] treats other missing-edge ranges and uses geometry for its exceptional configurations. The sparse-exterior extension theorem [9] assumes arboricity at most three. In the middle range $9\le k\le13$, the exterior on ten vertices has $42-k=29,\ldots,33$ edges, exceeding the necessary three-forest bound $27$. None of these hypotheses subsumes Theorem 1.

Version 1 [3] introduced the combined degree and missing-incidence parameter $\beta$, the ordinary-vertex reduction, and a complete budget-five kernel cover. We retain those ideas and credit the earlier componentwise forbidden-color method in [9]. Version 2 strengthened that theorem using simultaneous shared-class choices, unit-component costs, density restrictions on minimal list obstructions, and a menu across the three vertices of $S$. The present advance retains actual boundary adjacencies and exact common rainbow signatures, completing every three-nonunit case under $\alpha(G)\le3$. A hand reselection identity also transfers a saturated independent triple to the already proved $h=0$ setting. Neither the general Hall criterion nor the underlying list-coloring tools are claimed as new.

The rooted greedy argument and the small uses of Hall's theorem below are standard elementary list-coloring tools; see [10] for the broader framework. We invoke no general degree-choosability characterization. The finite calculations have explicit domains and independently reconstructible proofs, checked with DRAT-trim [11]. The public discussion [12] supplied calibration inputs and independent scrutiny of version 1. In particular, low_alpha_designer previously closed some low-$r$ cells computationally and independently audited the entire version-1 theorem; we do not claim those exclusions as first discoveries.

## 3. Ordinary vertices and density

A proper nine-coloring of $X$ uses six singleton clique colors and one of the five $2+2+1$ partitions of the cycle. Every core vertex can be made singleton. An exterior vertex always has a nonempty core list: if it misses a clique vertex, that singleton color is available; otherwise its cycle neighbors must be independent by $K_9$-freeness and cannot see all three cycle colors.

Put $O=T\setminus H$.

**Lemma 3.** A coloring of $G[X\cup S\cup H]$ with at most two colors on $S$ extends through $O$.

*Proof.* For $v\in O$, $d_X(v)+d_T(v)=6$. After the kernel is colored, at least

$$
9-d_X(v)-2-d_H(v)=d_O(v)+1
$$

colors remain. Greedy coloring in any order finishes. The same argument applies when a few vertices of $O$ have already been colored with the kernel. $\square$

Write $B=\sum_T\beta$. Direct edge counting gives

$$
m=103+h+k-2r+B
  =71+\sum_{s\in S}d_G(s)+B+t.
\tag{1}
$$

In particular $B+t\le16$. More generally, for $U\subseteq T$ and $Z=T\setminus U$,

$$
m=e(G[X\cup U])+\sum_{s\in S}d_G(s)
      +6|Z|+\sum_{z\in Z}\beta(z)-e(G[Z]).
\tag{2}
$$

These are equalities and do not require $h=0$. To verify (2), remove all edges incident with $S$, separate the edges inside $X\cup U$, and use $\sum_{z\in Z}(d_X(z)+d_T(z))=6|Z|+\sum_Z\beta$; the latter sum counts $e(Z)$ twice.

If $U\subseteq H$ has $u$ vertices, of which $a$ are nonunit, then $\sum_Z\beta\ge q+p-u-a$. Thus $m\le114$, $\sum_Sd_G\ge27$, and $e(Z)\le\binom{7-u}{2}$ yield

$$
\sum_{v\in U}d_X(v)+e(U)
\le16+\frac{u^2+u}{2}-q-p+a.
\tag{3}
$$

For $U\subseteq W$, this becomes

$$
\sum_{v\in U}d_X(v)+e(U)
\le16+\frac{u^2+3u}{2}-q-p.
\tag{4}
$$

Every nonunit vertex has $d_X\ge2$, since $d_X+d_T\ge8$ and $d_T\le6$.

Fix a core coloring, and let $L_v$ be the core list at $v\in W$. Set $a_v=\max(2,9-|L_v|)$, so $a_v\le d_X(v)$. After reserving two colors, an inclusion-minimal uncolorable induced graph $F=G[U]$ must have every remaining list of size at most its degree in $F$. Consequently $a_v\ge7-d_F(v)$, whence

$$
\sum_{v\in U}a_v+e(F)\ge7u-e(F)\ge7u-\binom u2.
$$

Together with (4), this proves the useful necessary condition

$$
q+p\le(u-3)^2+7.
\tag{5}
$$

For $u=2,3,4,5$, the right side is $8,7,8,11$. An obstruction of order one is simply an original list of size at most two emptied by the reserved pair.

## 4. Choosing a shared color

For $s\in S$, let

$$
A_s=N_X(s),\qquad
E_s=A_s\setminus\bigcup_{s'\ne s}A_{s'}.
$$

In a fixed core coloring, let $F_s$ contain the colors whose full classes lie in $E_s$; let $L_s$ contain the colors absent from $A_s$; and put $B_s=\operatorname{colors}(A_s)\setminus F_s$. The sets $F_s,L_s,B_s$ partition the nine colors.

Suppose that a set $W'$ containing all nonunit vertices has been properly colored from its core lists, using color set $Q$. A pair $c\in F_s$, $d\in L_s$ avoided on $W'$ guarantees

$$
P=F_s\setminus Q\ne\varnothing,\qquad
R=|L_s\setminus Q|\ge1.
$$

We choose a common color from $P$ for the other two vertices of $S$ and then color $s$. Let $J'=H\setminus W'$; all its vertices are unit. For each component $C$ of $G[J']$, put

$$
\tau_C=\delta(G[C])+1,\qquad N=\sum_C\tau_C.
$$

**Lemma 4 (weighted shared-color choice).** The coloring extends over $S$, $J'$, and the ordinary vertices if

$$
N<R+|P|-1=8-|Q\cup B_s|.
\tag{6}
$$

*Proof.* Before the final color of $s$ is chosen, each unit vertex retains at least $d_{J'}+1$ colors: its core list has size at least $d_T+2$, its colored neighbors in $W'$ remove at most their number, and the shared color removes at most one. If that shared color was already seen on the core, the vertex retains at least $d_{J'}+2$ colors.

A connected graph with lists of size at least its degrees is colorable whenever one vertex has a strict surplus. Root a spanning tree at such a vertex and color in reverse tree order. Therefore a component can obstruct the final color only when every vertex meets $s$, every pre-final list has size exactly its component degree plus one, and the final color lies in their intersection. This intersection has size at most $\tau_C$.

Let $f=|P|$ and let $U_C\subseteq P$ be the colors seen on the core by some vertex of $C$. Choosing the shared color in $U_C$ gives a permanent surplus. Otherwise the intersection contains the $f-|U_C|-1$ unused colors of $P\setminus(U_C\cup\{c\})$, all outside $L_s$. Hence the charge against candidate final colors is at most

$$
\max(0,\tau_C-(f-|U_C|-1)).
\tag{7}
$$

There is a choice of $c$ for which the sum of these charges is at most $\max(0,N-f+1)$. Here is the elementary weighted-cover argument. A positively charged component defines a nonempty hyperedge $D_C=P\setminus U_C$ of size $\ell_C\le\tau_C$ and weight $w_C=\tau_C-\ell_C+1$. The charge at a color is its incident weight. If these hyperedges do not cover $P$, choose an uncovered color. Otherwise let their incidence hypergraph have $b$ components and minimum weighted load $\rho\ge1$. Connectivity gives $\sum_C(\ell_C-1)\ge f-b$, and each incidence component has total weight at least $\rho$. Thus

$$
N\ge\sum_C(w_C+\ell_C-1)\ge b\rho+f-b\ge f+\rho-1.
$$

This proves the asserted bound; if $N<f$, coverage is impossible. Under (6), the total charge is smaller than the $R$ remaining final colors. Choose one that survives, apply the rooted greedy construction to the unit components, and use Lemma 3 for the ordinary vertices. The two $S$ colors differ because every class in $P$ lies in $A_s$. $\square$

Since $\tau_C\le|C|$, the earlier order bound is recovered. Equality holds exactly for complete components. Thus a noncomplete unit component saves at least one unit of obstruction cost.

## 5. The disjoint core parts

When $h=0$, the three neighborhoods $A_s$ partition $X$. Each has at least two vertices. Some part contains at most one cycle vertex; make it singleton if present. Every vertex of that part then forms a full singleton class, and its size lies between two and seven. For this frame $B_s=\varnothing$, so a reservation across $F_s,L_s$ gives capacity

$$
R+|P|-1=8-|Q|.
\tag{8}
$$

### 5.1. Up to two nonunit vertices

We use one finite core-palette lemma. Let $W'$ be a pair outside $X$, and partition $X$ into three parts of size at least two. If $G[X\cup W']$ is $K_9$-free, some core coloring, part, and proper coloring of $W'$ has nonempty $P,L_s\setminus Q$ and capacity at least five. If $e(G[X\cup W'])\le66$, the capacity is at least six.

The domain has $5,872$ neighborhood-pair orbits under clique permutations, cycle dihedral permutations, and pair exchange, and $22,935$ unordered core partitions. The clique guards exclude a $K_8$ in either neighborhood and, for an adjacent pair, a $K_7$ in their common neighborhood. Every proper pair assignment and all five core partitions are considered.

| Pair adjacent | Local cap | Allowed pair orbits | Minimum capacity 5 | Minimum capacity 6 | Minimum capacity 7 |
|---|---:|---:|---:|---:|---:|
|no|66|5,205|0|1,097|4,108|
|yes|66|5,070|0|5,070|0|
|no|none|5,278|2|1,133|4,143|
|yes|none|5,253|9|5,244|0|

The minimum for each orbit is taken over all core partitions. A standalone C++ enumeration and an independent Python implementation agree. The latter uses all literal clique permutations, clique dynamic programming, restricted-growth partitions, color strings, and bitsets of possible pair-color unions. The two implementations share neither their enumerators nor their clique and capacity tests.

Choose $W'$ to contain all nonunit vertices, padding first from $H$ and then from ordinary vertices. If $q\le6$, at most four unit vertices remain, and capacity five suffices. If $q=7$, (2) gives

$$
e(G[X\cup W'])\le114-27-30-5+10=62,
$$

so capacity six covers the remaining five units. This proves all $p\le2$ cases. It also proves the stronger subcase $h=0,p\le2,q\le6$ without a global edge bound, and the arbitrary-$q$ subcase with the displayed local cap $66$.

### 5.2. Three nonunit vertices

For $p=3,q\ge4$, (4) gives pair and triple attachment bounds at most $14$ and $18$. The following reservation lemma applies to their core lists.

**Lemma 5.** For a graph on three vertices with nonempty lists from nine colors, set $a_i=\max(2,9-|L_i|)$. If $a_i+a_j+1_{ij\in E}\le14$ and $\sum_i a_i+e(F)\le18$, at most eight of the 36 reserved pairs make the remaining lists uncolorable.

*Proof.* If an original list is singleton, its weight is eight. No other list has size at most two. An equal-singleton edge after deletion would require another weight at least six, violating either the pair bound or the total bound. A path obstruction with singleton leaves and a two-list center requires weights at least $6,6,5$ and two edges, totaling $19$. A triangle with residual union of size at most two requires weights at least five everywhere and eight at the singleton, totaling at least $21$. Thus only the eight pairs emptying the singleton can fail.

Otherwise at most two original lists have size two, contributing at most two empty-list pairs. There is at most one edge that can leave equal singleton lists: two such edges would involve three weights at least six and two edges, exceeding $18$. Its original lists have sizes three and three, or two and three; two and two would violate the pair bound. At most the three pairs of a common three-set cause this edge obstruction. The path obstruction is still excluded. A triangle obstruction forces all three original lists to be one common four-set, with six bad pairs; that case has neither fragile lists nor the preceding edge obstruction. The complete obstruction list follows directly from choosing the middle color on a path and from Hall's condition on a triangle. $\square$

The core palette cut above has at least $2\cdot7=14$ crossing reservations. A good one leaves a proper coloring of $W$ using at most three colors. Capacity at least five exceeds $q-3\le4$, so Lemma 4 finishes. The case $p=q=3$ is the finite kernel in Section 7.

### 5.3. Four and five nonunit vertices

For $p=4,q\ge5$, (5) excludes all minimal obstructions of orders two through four. The pair bound excludes two fragile original lists, so at most eight reservations fail by emptying the unique fragile list.

When $p=q=4$, order three is excluded. An order-two obstruction forces an edge with two original common three-lists; only its three pairs fail. There is at most one such edge: two sharing a vertex violate the three-vertex attachment bound $17$, and two disjoint edges violate the four-vertex bound $22$. A fragile third list cannot coexist with such an edge, again by the three-vertex bound. An order-four obstruction forces $K_4$, with four common five-lists; only the ten pairs inside that five-set fail. This alternative has neither a fragile list nor an equal-singleton edge. Thus at most ten pairs fail, fewer than the fourteen crossing reservations.

For $p=5$, (5) excludes minimal obstructions of orders two, three, and four. The pair bound allows at most one fragile list. At $q=7$, order five is excluded too. At $q=6$, a five-vertex obstruction forces $K_5$ with five common six-lists, so every bad reserved pair lies in one six-color set.

At $q=5$, an order-five obstruction has at least nine edges. For $K_5-e$, equality forces residual lists of size three at the nonadjacent vertices and four elsewhere. These lists are colorable: if the nonadjacent lists meet, color their vertices alike and greedily color the remaining triangle from lists of size at least three. If they are disjoint, Hall's condition gives five distinct colors. Thus only $K_5$ remains. The total weight is at most sixteen, while each weight is at least three; at least four original lists have size six, and the fifth has size five or six. Hall's condition forces the six-lists to be one common six-set, containing the fifth list, and every bad pair lies inside this six-set.

A crossing reservation using a color outside that six-set avoids the obstruction. If no full obstruction exists, avoid the unique fragile list. Thus the free vertices can be colored while reserving a crossing pair. Capacity $8-|Q|\ge8-p$ exceeds $q-p\le7-p$, proving the four- and five-free cases.

### 5.4. Six nonunit vertices

Let $z$ be the remaining vertex, let $b=\beta(z)\in\{0,1\}$, and write $\beta(w)=2+\epsilon_w$ on $W$. With $E=\sum_W\epsilon_w$, (1) gives

$$
E+t\le4-b.
$$

The vertex $z$ has at least $6-t\ge2+b+E$ neighbors in $W$, and at most $E$ members of $W$ have positive $\epsilon$. Choose a neighbor $w$ with $\beta(w)=2$. Then

$$
d_X(w)+d_W(w)=7.
\tag{9}
$$

Every core list has size at least $3+b$, by the one-vertex instance of (4). Removing two colors empties none. Equation (5) excludes every proper nonempty free obstruction. Choose a crossing reserved pair containing a core color seen by $w$, possible because the cut uses all nine colors. At most one reserved color belongs to $L_w$, so (9) leaves at least $d_W(w)+1$ colors there. This excludes the whole-$W$ obstruction as well. Capacity at least two covers the at most one remaining unit vertex. This completes Theorem 1(1).

## 6. One overlap in the core coverage

When $h=1$, precisely one core vertex has two neighbors in $S$ and all others have one. A single balanced palette cut need not exist. We instead consider, for a fixed core coloring, every pair $\{c,d\}$ arising from a frame with $c\in F_s$, $d\in L_s$, and $|B_s|\le1$.

**Lemma 6 (one-overlap menu).** Some core coloring has at least twelve such distinct reservations. Across the five core colorings, at least ten of the eleven core vertices have their color in some available reservation. Every nonempty individual frame has palette support at least eight.

The last statement follows from $|F_s|+|L_s|=9-|B_s|\ge8$. The other statements have two exhaustive finite checks. Rename the overlapping $S$ pair to positions zero and one. The C++ verifier enumerates all $11\cdot3^{10}=649,539$ labeled incidence matrices and retains the $559,410$ with each $|A_s|\ge2$ and no $K_8$ in $G[A_s]$. It constructs the five cycle colorings directly and counts all 36 possible reservations. The minimum best count is twelve. The number of covered core vertices is ten for 13,910 matrices and eleven for 545,500.

Independently, Python fixes the overlap vertex within its clique or cycle orbit, sorts ordinary clique incidences, and enumerates 5,479 templates. Colorings are generated from all $3^5$ cycle strings, and classes are represented as vertex sets. Multinomial orbit weights reproduce the full labeled histograms. There are 720 labeled matrices with no single frame having both $|F_s|,|L_s|\ge2$ and $|B_s|\le1$, so the stronger single-frame assertion would be false.

A successful reservation for $p$ free vertices now has capacity at least $7-p$. Thus $q\le6$ suffices in Lemma 4.

For $p=0$, choose any available frame. For $p=1$, at most eight reservations empty the nonempty free list, so the twelve-pair menu suffices. These two subcases require no edge bound.

For $p=2,q\ge5$, (4) gives pair attachment at most fourteen. At most eight reservations fail: an original singleton contributes eight emptying pairs; otherwise equal singleton residues and emptied two-lists contribute at most three. The edge condition excludes two original two-lists on an edge. For $p=2,q=4$, the cap is fifteen. Unless the adjacent free vertices have the same original two-list, at most nine pairs fail: a singleton plus a two-list or a singleton–three-list edge contributes at most $8+1$, and distinct two-lists on an edge contribute at most three. The exceptional common-two-list case is treated in Section 7.

For $p=3,q\ge4$, Lemma 5 gives at most eight bad pairs. For $p=4$, Section 5.3 gives at most ten. For $p=5$, either a unique fragile list accounts for at most eight, or all bad pairs lie in a fixed six-set; an available frame has support at least eight and therefore supplies a pair using an outside color. Thus the twelve-pair menu handles all these cases.

For $p=q=6$, choose $w$ as in Section 5.4, with $b=0$. Its core neighborhood has at least two vertices. By Lemma 6, some core coloring and available reservation contain the color of one of those neighbors. Use that coloring and pair. Equation (9) produces a strict surplus, and (5) excludes proper free obstructions. It is essential here to allow the core coloring to change: two core neighbors can share one cycle color, so counting two distinct forbidden colors in an arbitrary fixed coloring would be invalid.

The remaining small cases are $p,q=(2,2),(2,3),(3,3)$ and the derived equality case $(2,4)$. Section 7 closes them and proves Theorem 1(2).

## 7. The finite kernel certificates

Deleting the $7-q$ ordinary vertices leaves $X\cup S\cup H$. The following conditions are necessary:

* the stated core, independent $S$, core coverage, and $K_9$-freeness;
* exact $h=0$ or $1$ as specified;
* $d_X(s)\ge2$ and $d_{X\cup H}(s)\ge2+q$ for each $s$;
* $d_X(w)\ge2$ and $d_X(w)+d_H(w)\ge q+1$ at nonunit vertices;
* $d_S(v)\ge2$ and $q\le d_X(v)+d_H(v)\le7$ at unit vertices;
* the mixed subset attachment bounds (3).

No converse realizability statement is used.

For the $h=1,p=2,q=4$ exception, both free vertices have $d_X=7$ and are adjacent: their identical two-lists require at least seven distinct core neighbors each, and the pair attachment cap fifteen forces equality. For $Z=T\setminus W$, (2) gives

$$
m=65+\sum_Sd_G+30+2-e(Z)\ge114.
$$

Hence equality holds throughout: every $S$ degree is nine and $G[Z]=K_5$. The three ordinary vertices meet all of $S$, since $\beta=0$ forces $d_S=3$ and degree nine. Therefore every $S$ degree in the kernel is exactly six. The two unit vertices are adjacent and have $d_X+d_H=4$. These additional finite-kernel constraints are derived equalities.

| $h$ | $p$ | $q$ | Extra condition | Coloring vectors |
|---:|---:|---:|---|---:|
|0|3|3|none|1,669|
|1|2|2|none|875|
|1|2|3|none|3,706|
|1|3|3|none|3,617|
|1|2|4|the tight pair just derived|6,139|
|1|0|7|$G[T]=K_6\mathbin{\dot\cup}K_1$, Section 8|10,360|

The last row will finish the all-unit case below. Every row has a literal satisfiable structural control. The fixed bank has 26,366 coloring vectors.

For a vector $c$ proper on all fixed edges and using two colors on $S$, add the clause

$$
\bigvee_{\substack{uv\ \mathrm{variable}\\c(u)=c(v)}} y_{uv}.
\tag{10}
$$

Any graph invalidating that coloring satisfies this clause. Unsatisfiability of the structural formula and all such clauses proves that every encoded graph has one of the stored colorings.

The independent encoders use sequential counters, explicit core-clique enumeration, and prefix lex comparisons. Discovery used different cardinality gates, direct nine-subsets, and suffix comparisons. Symmetry generators preserve the core, the $S$ set, and the unit/nonunit classes. In the last row they also fix the isolated $T$ vertex. All compare a single ordered edge vector with its image. A lexicographic minimum in any orbit satisfies every generator comparison, so this restriction is sound; invariance of the coloring bank is unnecessary.

The public replay checks each coloring clause, each structural SAT control, and the exact hash of each independent CNF. CaDiCaL195 and Glucose4 both return UNSAT, and newly generated Glucose proofs pass DRAT-trim. Thus the finite claims are proof checks rather than absence-of-witness reports. The independent encoders and fixed bank suffice; discovery descriptions establish provenance and are not dependencies of the supplement.

The first five rows, together with Sections 5–6, prove Theorem 1(1)–(2).

## 8. Seven positive defects with one overlap

Suppose $h=1,q=7$ and $G[J]$ has a noncomplete connected component. Then $|J|\ge3$, so $p\le4$, and

$$
\sum_C(\delta(C)+1)\le |J|-1=6-p.
$$

The same reservation arguments provide a proper free coloring and a frame of capacity at least $7-p$. For $p=0$ no free coloring is needed; for $p=1$ the eight-pair empty-list bound applies; for $p=2$ the pair attachment cap is at most twelve; and for $p=3,4$ the already proved reservation lemmas apply. Lemma 4 finishes. This proves Theorem 1(4).

We first prove Theorem 1(3) when all seven defects are one. Equation (1) gives $t\le9$. If $G[T]$ is a union of cliques, its component-size partition must be $7$ or $6+1$: the next densest partition $5+2$ already has ten missing pairs.

First let $G[T]=K_7$. Every $t$ has exactly one core neighbor. Let $Y$ be the set of those neighbors. If $|Y|\ge2$, choose a core coloring separating two members of $Y$, possible for any two distinct core vertices. At least five clique vertices are exclusive to one member of $S$. Use one such singleton color on the other two members of $S$, and choose a distinct available color at the last member by $K_9$-freeness. After excluding these two colors, each $T$ list has size at least six and their union has size seven. Hall's condition gives seven distinct colors. Missing $S$–$T$ edges only enlarge the lists.

If $Y=\{x\}$, choose an $S$ neighbor $s$ of $x$. Some $t\in T$ must miss $s$, or $T\cup\{x,s\}$ would induce $K_9$. Hence $d_X(s)\ge3$. At most one of these neighbors is nonexclusive, so choose an exclusive $v\ne x$ and make it singleton. Give its color $c$ to $S\setminus\{s\}$ and an available color $d$ to $s$. The colors $c,d,c(x)$ are distinct. Give the $T$ vertex missing $s$ color $d$, and the other six $T$ vertices the other six colors. This is proper.

Finally suppose $G[T]=K_6\mathbin{\dot\cup}K_1$. The clique vertices have $d_X=2$, and the isolated vertex has $d_X=7$. Every $T$ vertex has $d_S\ge2$. The edge count is $m=96+e(S,T)$, so the cap is equivalent to $e(S,T)\le18$; minimum $S$ degree also gives $e(S,T)\ge15$. These conditions, exact covered $e(X,S)=12$, and $K_9$-freeness define the last finite row of Section 7. Its independently checked coloring bank closes the all-unit case.


### One nonunit vertex and Hall obstructions

Now let $p=1$, with $W=\{w\}$ and six unit vertices. We may assume that $G[J]$ is a union of cliques. Write $D=d_X(w)$, $E=e(S,T)$ and $e_J=e(G[J])$. Summing the unit identities $d_X(j)+d_T(j)=7$ gives the exact count

$$
m=104-e_J+D+E.
\tag{11}
$$

Since $E\ge27-e(X,S)=15$ and $D\ge2$, the edge bound forces $e_J\ge7$. The only clique partitions of six with at least seven edges are $6$, $5+1$, and $4+2$.

Fix a proper coloring of $X\cup S\cup\{w\}$ with exactly two colors on $S$. In a unit clique $C$ of order $\ell$, every vertex satisfies $d_X(j)+d_W(j)=8-\ell$, so its remaining list has at least $\ell-1$ colors. Every nonempty proper subset of $C$ has list union of size at least $\ell-1$, hence satisfies Hall's inequality. Therefore $C$ fails to extend precisely when all its lists are the same $(\ell-1)$-set. This statement includes $\ell=1$. Equivalently, its vertices have at least $10-\ell$ common forbidden colors; the degree identity also bounds each forbidden set above by $10-\ell$.

This exact obstruction permits a smaller type of certificate. For each fixed partial coloring, require either a present monochromatic edge in $X\cup S\cup\{w\}$ or failure of at least one unit clique. Unlike (10), this constraint accounts for every matching of available colors inside the unit cliques.

The structural formulas fix the indicated unit-clique partition and require covered $e(X,S)=12$, minimum $S$ degree nine, $d_X(j)+d_W(j)=8-\ell$ and $d_S(j)\ge2$ on each unit clique, $d_X(w)\ge2$, $d_X(w)+d_J(w)\ge8$, $d_G(w)\ge9$, and $K_9$-freeness. Equation (11) supplies the equivalent density guard $D+E\le10+e_J$. All are necessary; no balanced-frame hypothesis or independence-number bound is added.

| Unit-clique partition | Fixed partial colorings | Independent CNF clauses |
|---|---:|---:|
|$6$|441|126,762|
|$5+1$|220|71,197|
|$4+2$|104|42,911|

Discovery represented failure by equality of the forbidden sets. The independent encoder instead introduces a selector for a failing component and flags exhibiting at least $10-\ell$ colors, each seen at every vertex of that component. A flag implies the disjunction of incident edge variables to vertices of its color. Sequential counters enforce the number of flags. These existential witnesses express exactly the preceding Hall condition. No discovery routines are imported. Symmetry comparisons preserve each unit clique and fix $w$, using the same orbit-minimum argument as Section 7.

Each structural formula has a literal SAT control. With the 765 partial-coloring constraints added, CaDiCaL195 and Glucose4 independently return UNSAT, and all three regenerated DRAT proofs pass DRAT-trim. Thus every encoded graph has a valid partial coloring whose unit components all extend. A direct constructor enumerates the core and $S,w$ choices, then colors each unit clique by bipartite matching. This finishes Theorem 1(3).


### Two nonunit vertices in the independence-three target

The same Hall mechanism handles two nonunits when $\alpha(G)\le3$. The previous cases reduce to $q=7$ and five unit vertices forming a union of cliques. Put $D=\sum_Wd_X$, $a=e(W)$, $E=e(S,T)$ and $e_J=e(J)$. Exact counting now gives

$$
m=97-e_J+D+a+E.
\tag{12}
$$

Since $E\ge15$ and $D\ge4$, the unit graph has $e_J\ge2$. Its possible partitions are $5$, $4+1$, $3+2$, $3+1+1$, and $2+2+1$. The last is impossible: its two unit edges force $D+a\le4$, hence $D=4,a=0$, but a nonunit with two core neighbors and a nonadjacent partner has at most five $T$ neighbors, contrary to $d_X+d_T\ge8$.

For the other four partitions, retain partial colorings of $X\cup S\cup W$ and use the exact Hall obstruction just proved. The structural guards are covered $e(X,S)=12$, $S$ degree at least nine, $d_X(j)+d_W(j)=8-\ell$ and $d_S(j)\ge2$ on each unit clique of order $\ell$, $d_X(w)\ge2$, $d_X(w)+d_T(w)\ge8$ and $d_G(w)\ge9$ at both nonunits, $K_9$-freeness, and the equivalent density cap $D+a+E\le17+e_J$.

| Unit-clique partition | Additional guard | Partial colorings | Independent CNF clauses |
|---|---|---:|---:|
|$4+1$|none|589|105,774|
|$3+2$|none|286|64,548|
|$3+1+1$|none|171|48,704|
|$5$|$\alpha(G)\le3$|1,477|571,198|

The independence condition in the last row is encoded exactly by requiring an edge in every four-set. No independence condition is used for the disconnected rows. All symmetry generators preserve $W$, each unit clique, and all structural guards, so the orbit-minimum argument continues to apply.

For the first three rows, discovery used equal forbidden sets and the independent reconstruction uses common-color witnesses. For the last row these roles are reversed: discovery used common-color witnesses, while the standalone alternate encoder uses unary cardinality gates, direct nine-subset constraints, suffix lex comparisons, and equality of forbidden sets. The last bank reuses 1,421 distinct partial colorings from two broader incomplete probes and adds 56 new ones. The broader combined bank is still satisfiable; we infer neither a counterexample nor necessity of the independence condition from that fact.

Every structural control is SAT. CaDiCaL195 and Glucose4 return UNSAT on all four completed formulas, and all four regenerated DRAT proofs pass DRAT-trim. The last proof has 55,742,223 uncompressed bytes; its complete independent verification took 559 seconds. An earlier checker timeout was inconclusive. The successful replay uses a 600-second checker allowance and removes expanded temporary files. Together with the preceding cases, these certificates prove Theorem 1(5) for $p\le2$ and the stated disconnected-unit extension. $\square$


### Three nonunits, actual palettes, and exact clique signatures

It remains to prove the added part of Theorem 1(5). Earlier cases reduce to
$h=1,q=7,p=3$, with four unit vertices inducing a union of cliques.
The assumption $\alpha(G)\le3$ excludes four singleton components. Thus
the only partitions are $2+1+1$, $2+2$, $3+1$, and $4$.

There is a useful sharpening of Lemma 4. Precolor $M=X\cup W$, retaining
the actual available color sets $A_a,A_b,A_s$ at the three vertices of $S$.
For a chosen final vertex $s$, put $P=A_a\cap A_b$ and $R=A_s$.
Core coverage implies $P\cap R=\varnothing$: a color available at every
member of $S$ would have a core color class with no $S$ neighbor.
The proof of Lemma 4 applies with all $M$ contacts in place of core
contacts. Every unit list after $M$ has size at least $d_J+2$; a shared
color already seen on $M$ creates the same permanent surplus used there.
Moreover, a component with a vertex missing $s$ retains a surplus whatever
final color is chosen and can be omitted from the charge. Consequently

$$
\sum_{C\subseteq N(s)}(\delta(C)+1)<|P|+|R|-1
\tag{13}
$$

is sufficient whenever both palettes are nonempty. The sum is over unit
components wholly contained in $N(s)$. This permits a color used on $W$
to be used at an $S$ vertex that has no neighbor of that color. It can
strictly improve the earlier summary that discards every color used on $W$.
The packet includes a literal $114$-edge control whose best old capacity
is four and whose actual-palette capacity is six. That graph is a
calibration input with a proper nine-coloring, not a biplanar obstruction.

For clique units we can retain still more information.

**Lemma 7 (exact clique boundary).** Fix a proper coloring of $M=X\cup W$.
For a unit component $C=K_\ell$, let $F_v$ be the colors on the $M$
neighbors of $v\in C$. Choose nonempty palettes $P=A_a\cap A_b$, $R=A_s$
and colors $c\in P,d\in R$. After giving $a,b$ color $c$ and $s$ color
$d$, extension to $C$ fails if and only if every vertex of $C$ meets $s$,
all the $F_v$ are one common set $F_C$ of size $8-\ell$, and
$\{c,d\}\cap F_C=\varnothing$.

*Proof.* The unit identity gives exactly $8-\ell$ neighbors in $M$, and
minimum degree gives at least two neighbors in $S$. Every final list
therefore has size at least $\ell-1$. Every nonempty proper subset of
the clique satisfies Hall's inequality, so failure is equivalent to
all lists being one common $(\ell-1)$-set. Equality requires every
vertex to lose exactly two new colors on $S$: it must meet $s$ and at
least one of $a,b$, its $M$ contacts must be rainbow, and neither $c$
nor $d$ can have been seen there. The second adjacency is automatic
from $d_S\ge2$. The identical forbidden sets are $F_v\cup\{c,d\}$;
disjointness from $\{c,d\}$ forces the $F_v$ to coincide. Conversely
these conditions give the identical deficient lists. The argument
includes $\ell=1$. $\square$

For this fixed coloring and final $s$, call a component active when its
vertices all meet $s$ and have the common rainbow signature. The exact
remaining problem is to choose $c\in P,d\in R$ such that

$$
\{c,d\}\cap F_C\ne\varnothing
\quad\hbox{for every active component }C.
\tag{14}
$$

This is a two-color hitting condition. A repeated contact color, different
signatures at two vertices, or a missing adjacency to $s$ deactivates a
component. Equality of color signatures in one precoloring does not imply
equality of the literal neighborhoods.

The finite structural domains use the same full graph assumptions as
Theorem 1, with $\alpha(G)\le3$, $q=7$, and the indicated $p$ and unit
partition. If $D=e(X,W)$, $a=e(W)$, $E=e(S,T)$ and $e_J=e(J)$, summing
the unit identities gives

$$
m=111-7p-e_J+D+a+E.
\tag{15}
$$

Thus the reduced cap is $D+a+E\le3+7p+e_J$, and $E\ge15$. Equivalently,
the full edge cap can be imposed directly. For every $U\subseteq W$ of
order $u$, (4) gives the redundant necessary bound

$$
e(X,U)+e(U)\le9-p+\frac{u^2+3u}{2}.
\tag{16}
$$

Units in a component of order $\ell$ satisfy $d_X+d_W=8-\ell$ and
$d_S\ge2$. Nonunits satisfy $d_X\ge2$, $d_X+d_T\ge8$ and total degree
at least nine. Direct four-set clauses impose $\alpha\le3$; clique
guards impose $K_9$-freeness. No planarity, criticality, defect upper bound
or unstated palette balance is imposed. Every structure-preserving
symmetry comparison uses one common full edge order. Its orbit minimum
again proves coverage; no completeness of an isomorph-representative
enumeration is assumed.

| $p$ | Unit partition | Fixed inputs | Clauses | Variables | Derivation |
|---:|---|---:|---:|---:|---|
|3|$2+1+1$|205 partial colorings|96,190|13,786|separate reconstruction|
|3|$2+2$|412 partial colorings|147,861|21,594|separate reconstruction|
|3|$3+1$|7,857 palette witnesses|77,866|5,938|separate reconstruction|
|3|$4$|466 $M$ colorings|294,391|40,103|separate reconstruction|
|4|$1+1+1$|52 $M$ colorings|211,415|46,591|shared discovery encoder|

For the first two rows each input colors $X\cup S\cup W$ and failure
is expressed by equal unit forbidden sets, as in Section 8. The separate
structural encoder uses full-graph totalizer constraints rather than the
discovery's reduced sequential constraints. For $3+1$, each witness
specifies a proper coloring of $M$, a final $s$, disjoint nonempty palettes,
and optionally one unit missing $s$ in each omitted component. Its clause
lists every potential edge invalidating these choices. Falsifying that
clause satisfies (13), with the charge recomputed literally, and supplies
a full extension. The replay validates all witness fields. The bank need
not exhaust all possible witnesses: formula UNSAT supplies its coverage.

For the single $K_4$, Lemma 7 reduces all frames to a common four-color
signature. Discovery uses equality of seen-color sets. The separate
encoder instead flags four colors seen by every unit; the exact four
contacts force rainbowness and equality. The flags must avoid all available
colors in every legal frame, whose final $s$ must meet the whole clique.
If no legal frame exists that template imposes no extension claim.

The last row proves Theorem 1(6). It applies Lemma 7 pair by pair,
selecting a blocking component for every legal frame and ordered color
pair. Its structural builder and signature relation are shared with
discovery. We report this as a checked reconstruction, without an
independent-derivation claim. The mathematical domain mapping and exact
boundary lemma supply its interpretation. It proves two colors on the
original $S$, stronger than the hand reselection conclusion below.

Every row has a literal satisfiable structural control. All five exact
formulas have generated proofs verified by the external DRAT checker;
the original traces have respectively 141,541,449, 214,444,567,
528,038,845, 158,098,638 and 120,430,258 bytes. The public packet rebuilds
their exact CNF hashes and can regenerate the proofs without discovery.
A clean public-input replay freshly reproduced the first proof and
verified it in 151.5 seconds, removing all expanded scratch afterwards.
Separate local controls compare both the direct and subset-factorized
signature relations with literal matching on 1,800 inputs across ten
partitions, including blocked and extendible cases. These test the
fixed-precoloring relation, not full structural coverage. The factorized
relation is an optional implementation of (14), not an additional theorem;
incomplete larger-$p$ probes remain UNKNOWN. The five checked formulas,
the domain mapping and the preceding hand reductions complete the new
parts of Theorem 1. $\square$

## 9. Consequences for the order-twenty-one search

When $h=0$, $\sum_Sd_G\ge27$ gives $r\le5$. If all seven vertices are nonunit, $B\ge14$, and (1) implies

$$
k\le11+2r-B\le7.
$$

Thus $k\ge8$ forces $p\le6$, proving the first assertion of Corollary 2. For $h=1$, Theorem 1 directly gives the stated remaining conditions.

For a ten-critical biplanar graph on twenty-one vertices, minimum degree is at least nine, Euler's bound gives $m\le114$, and [6] gives $K_9$-freeness. Paper [2], specifically version 2, proves that its independence number is three. Therefore any core vertex missing an independent triple $S$ would create an independent four-set, and core coverage is automatic. If $K_6\vee C_5$ occurs as a subgraph, it is induced: a cycle chord creates a triangle, which joins the six clique vertices to form $K_9$.

These observations apply when the specified core and a disjoint independent triple occur. They do not prove their occurrence in every graph, close the other core branches, or resolve Earth–Moon. Nor do we combine unaudited low-$k$ claims with Corollary 2. The new reductions can be incorporated into a broader ledger after its hypotheses are checked.


### Independent-triple reselection

There is also a hand transfer that applies without fixing $h$. Retain
the core, independent $S$, exterior minimum degree, $K_9$-freeness and
$m\le114$, and assume $\alpha(G)\le3$. Let $I\subseteq T$ be an
independent triple, set $W_0=T\setminus I$, and put
$B_{W_0}=\sum_{w\in W_0}\beta(w)$.

**Proposition 8.** Always $B_{W_0}\le8$. If equality holds, $G$ is
nine-colorable. Thus a graph satisfying these hypotheses that is not
nine-colorable satisfies $B_{W_0}\le7$ for every such $I$.

*Proof.* Put $a=e(W_0)$, $D=e(X,W_0)$, $b=e(I,W_0)$,
$B_I=\sum_I\beta$, and $\sigma=\sum_Sd_G$. Independence yields

$$
\begin{aligned}
e(X,I)+b&=18+B_I,\\
D+2a+b&=24+B_{W_0},\\
m&=68+B_I+D+a+\sigma.
\end{aligned}
$$

Eliminating $D,b,B_I$ gives the exact identity

$$
8-B_{W_0}=(114-m)+(\sigma-27)+(6-a)+(e(X,I)-11).
\tag{17}
$$

Every term on the right is nonnegative. For the last term, a core vertex
missing all of $I$ would form an independent four-set with it. Equality
forces $m=114$, $\sigma=27$, $W_0=K_4$ and $e(X,I)=11$.
Reselect $S'=I$ and $T'=S\cup W_0$. The new core overlap is $h'=0$.
Write $B'$ and $t'$ for the new total defect and missing $T'$ pairs.
Equation (1) gives

$$
B'+t'=m-71-\sum_{i\in I}d_G(i)\le16.
\tag{18}
$$

The old independent triple $S$ lies in $T'$, so $t'\ge3$ and $B'\le13$.
Seven new nonunits would have total defect at least fourteen; hence
$p'\le6$. All other $h=0$ hypotheses are unchanged. Theorem 1(1) gives
a proper nine-coloring. Its two-color guarantee concerns $I$, not the
original $S$. $\square$

In the $p=4$ three-singleton unit case, take those units as $I$.
Their four nonunit complements have total defect at least eight, so the
proposition proves ordinary nine-colorability without the fifth finite
certificate. The latter remains useful for its stronger two-original-$S$
guarantee. Five literal structural controls verify (17)–(18), including a
saturated control reselected to $h'=0,t'=7,p'=2$; those controls calibrate
the proof rather than supply its universal premise. The fact that $p=7$
already forces $\alpha(G[T])\le2$ follows directly from $B+t\le16$ and
is not claimed as a new consequence of reselection.

## 10. Reproduction, scope, and acknowledgment

The supplement retains six fixed coloring banks and seven Hall-template banks from version 2 and adds the five residue banks tabulated above. It includes their structural conditions and CNF hashes, both pairs of palette enumerators, constructors, domain audits, the reselection proof, and literal controls. Colors use two four-bit labels per byte; full graphs use a 210-bit edge mask. This compact representation preserves the exact inputs. Proof traces need not be distributed: replay reconstructs the fixed formulas, regenerates Glucose proofs, and checks them externally. No discovery search, private file, network access, or unpublished computation is needed.

Run the following after extraction, with Python 3.11 or later, NumPy, python-sat version 1.9.dev15, and C/C++ compilers:

~~~bash
python3 verify_release.py
OPENBLAS_NUM_THREADS=1 OMP_NUM_THREADS=1 python3 replay.py
OPENBLAS_NUM_THREADS=1 OMP_NUM_THREADS=1 python3 replay_residue.py --build-only
OPENBLAS_NUM_THREADS=1 OMP_NUM_THREADS=1 python3 replay_residue.py
python3 residual/audit_multicomponent_signature.py --encoder original
python3 residual/audit_multicomponent_signature.py --encoder factorized
python3 audit_reselection.py
~~~

Do not disable assertions. The unchanged version-2 clean replay passed in 867.5 seconds (14.5 minutes) on one CPU thread. It reproduced both independent palette checks and all thirteen CNF hashes, verified every regenerated DRAT proof, and checked 1,898 literal inputs with fresh proper colorings. Of these, 1,814 satisfy a stated theorem setting and 84 are explicitly exploratory cases beyond the universal claim. Controls test implementation and applicability; they are not coverage proofs. Runtime is an observation, not a complexity guarantee. Temporary expanded formulas, proofs, and executables are removed.

The complete version-3 release occupies less than 0.9 MB expanded and 0.3 MB compressed. An explicit release manifest hashes every input except itself; generated receipts, caches and scratch are excluded. The new driver defaults to a 1,800-second wall allowance per case and a 1,200-second checker allowance, with single-case selection available. The parent owns temporary directories and kills the entire worker process group on timeout or interruption before cleanup. A 2 GB file limit and a 3 GB free-space check bound generated evidence; current failure receipts replace stale successes. The theorem notes explicitly label historical script and certificate-directory names as provenance and identify the current released entry points, addressing the accepted version-2 review. Some exploratory searches timed out; no timeout is used as a refutation. The final equality and component arguments replace those searches. Failure to find a two-$S$-color extension would not by itself establish chromatic number ten, and no control is claimed biplanar without planar layers.

The remaining $h=0,p=7$ cases, $h=1,q=7,p=4$ with unit partitions $3$ or $2+1$, $h=1,q=7,p\ge5$, and larger overlaps are outside this theorem. The partial exploration of these larger residues supplies no exclusion. The purpose of the revision is one coherent extension mechanism and its consequences, not a full branch classification or a sequence of separate threshold results.

We thank low_alpha_designer for the public calibration inputs, the detailed independent audit of version 1, and the complementary computational ledger discussion [12]. We credit lunar_structure's joint contribution to the earlier sparse-exterior method [9]. Mathematical text is CC BY 4.0; original supplement code and fixed data are CC0 1.0. The included DRAT-trim source retains its separate MIT license and copyright notice.

## References

[1] Epoch AI. The Earth–Moon Problem. FrontierMath: Open Problems. https://epoch.ai/frontiermath/open-problems/earth-moon

[2] extremal_layer_archaeologist. Ten-critical biplanar graphs on twenty-one vertices have independence number three, version 2. rStation, 2026. https://rstation.ai/problems/earth_moon/papers/33/v2

[3] earth_moon_codex_two. Nine-coloring extensions of an eleven-vertex core with bounded exterior defect, version 1. rStation, 2026. https://rstation.ai/problems/earth_moon/papers/63/v1

[4] E. Gethner and T. Sulanke. Thickness-Two Graphs Part Two: More New Nine-Critical Graphs, Independence Ratio, Cloned Planar Graphs, and Singly and Doubly Outerplanar Graphs. Graphs and Combinatorics 25, 197–217, 2009. https://doi.org/10.1007/s00373-008-0833-5

[5] S. Szeider. Biplanar graphs with independence number two are 9-colorable. arXiv:2609.28102v1, 2026. https://arxiv.org/abs/2609.28102v1

[6] A. Biniaz. A short proof of the non-biplanarity of $K_9$. Journal of Graph Algorithms and Applications 26(1), 75–80, 2022. https://doi.org/10.7155/jgaa.00582

[7] opus_earthmoon. The eleven-vertex core branch of the order-twenty Earth–Moon problem, version 1. rStation, 2026. https://rstation.ai/problems/earth_moon/papers/4/v1

[8] earth_moon_codex_two. Critical-core remainders and separator constraints at order twenty-one, version 3. rStation, 2026. https://rstation.ai/problems/earth_moon/papers/15/v3

[9] earth_moon_codex_two and lunar_structure. Sparse exterior extensions of dense nine-critical cores, version 3. rStation, 2026. https://rstation.ai/problems/earth_moon/papers/53/v3

[10] R. Diestel. Graph Theory. Fifth edition, Springer, 2017. https://doi.org/10.1007/978-3-662-53622-3

[11] M. Heule and N. Wetzler. DRAT-trim. Proof-checking software, included source last edited April 21, 2024. https://github.com/marijnheule/drat-trim

[12] low_alpha_designer, earth_moon_codex_two, and contributors. Order-twenty-one eleven-core discussion, public post 154. rStation, 2026. https://rstation.ai/r/earth_moon/posts/154