Affine list constraints and simultaneous witnesses for G25 cover extensions

1. Contribution and relation to earlier work

The Earth–Moon problem asks whether every graph whose edges partition into two planar graphs is nine-colorable [1]. Ordinary covers of a ten-chromatic source are a possible construction route: the covering matchings may disperse a geometric obstruction while preserving enough coloring demand. Our results exclude additional classes of such covers by extending a prescribed coloring of their center vertices.

The main tool is an abstract list-coloring theorem. Partition variables into cliques of order at most five. A variable has more permitted real values than the order of its clique, and at most nine values. Each variable occurs in exactly two affine forms, with opposite coefficients $+1$ and $-1$. If each form has at least three variables, all cliques can be colored injectively while every form is nonzero. Neither equal lists within a clique nor zero affine constants are required.

The proof selects a form whose removal leaves the form-incidence multigraph connected. We precolor all but one of its variables so that the form is already safe, then propagate strict list slack through the remaining constraints. The precoloring uses a signed distinct-representative sumset bound. We prove the bounded parameter range needed here by elementary interpolation and 110 exact integer coefficient identities. A variant permits binary forms when a suitable noncut higher form exists. A complementary theorem handles every homogeneous color-multiplicity system with at most one negative occurrence per variable: arbitrary positive witnesses create a pseudoforest, whose union with the clique graph is list-colorable. It allows all binary/higher mixtures without a witness-capacity restriction.

These tools apply to the source $G_{25}$ used in recent cover constructions. Its host $A=K_7$ has ports of sizes $2,2,3$, joined respectively to three mutually anticomplete arms $B_i=K_5$. Its center $C=K_3$ is complete to all arms and anticomplete to the host. Earlier deterministic cover results [2,3,4] establish several nine-color extension mechanisms. Paper 49 [2] handles arbitrary prescribed centers with one split large-port source and gives a conditional two-source theorem. Paper 45 [3] supplies equality reservations, linear row comparisons and private-block absorption. Paper 42 [4] analyzes the limitations of ordinary and fractional coloring bounds inherited from the source. We use and credit those structural ideas. The new contribution is a general affine list theorem, simultaneous histogram witnesses, and an adaptive comparison reduction for three independently moving large-port sources. A new two-head interface treats either small port as the moving port. A structural decomposition then gives arbitrary prescribed-center extension whenever each host has at most one nonfull port, with the moving type allowed to differ between light components. The cover architecture retains host and arm cliques. Combining this with the selected-intact center coordination of [2] gives nine-colorability exactly when no trivial $G_{25}$ component occurs.

The polynomial coefficient argument is an application of the principle underlying the Combinatorial Nullstellensatz [5]. The restricted-sums polynomial method has the direct precedent [6]. Restricted signed sumsets are studied, for example, in [7]; that work considers sums from one underlying integer set, while our local statement uses separate lists and fixed signs. We do not claim that the bounded additive inequality itself is new. We supply its exact finite coefficient proof so that no unverified general sumset theorem is imported. Connected degree-choosability [8] is the only additional coloring theorem used in the complementary binary-core argument.

All results concern restricted cover architectures and hold without assuming biplanarity. The unrestricted Earth–Moon problem remains open. The histogram theorem removes all residual-core restrictions in the one-moving-port architecture. Two further mechanisms extend the architecture. A shared arm vertex repairs the exact Hall obstruction when any two ports move, provided at every host one moving port has a neighbor common to all its heads. A different theorem treats both moving small ports when every individual small head sees a whole arm clique, using graded cycle lists. A local cross-intersection count also handles three coherent moving ports. These are separate cover classes; their hypotheses are not assumed to combine arbitrarily from host to host.

| Cover class | Additional requirement | Prescribed-center conclusion | |---|---|---| | At most one nonfull port per host (Theorem 8) | Moving type may differ between light components | Exact intact uniform obstruction | | Any two moving ports (Theorems 10 and 12) | Other port full; at every host one moving port has a common neighbor of all its heads | Same exact obstruction | | Individual full small-head neighborhoods (Theorem 11) | Large port full; each individual small head sees a whole arm clique, with full and nonfull ports allowed | Same exact obstruction | | Three coherent moving ports (Theorem 13) | Within each port, all head neighborhoods coincide; those neighborhoods may disperse among arms | Same exact obstruction |

In each class, the center coordination of [2] gives nine-colorability exactly when there is no trivial $G_{25}$ component. The cycle-palette reduction develops the cycle-interface viewpoint of [2, Section 5] with a different literal quotient and explicit graded lists.

2. Affine list constraints

Let $X$ be partitioned into cliques $\mathcal C$, with $1\le |C|\le5$. Each $v\in C$ has a finite real list $L(v)$ satisfying

$$ |C|+1\le |L(v)|\le9. $$

Lists in the same clique may differ. Let $\mathcal F$ be a family of affine forms

$$ f_h(x)=\kappa_h+\sum_{v\in S_h}\varepsilon_{hv}x_v, \qquad \varepsilon_{hv}\in\{-1,1\}. $$

Every variable belongs to exactly two distinct supports, and its coefficients in those forms are opposite. The constants $\kappa_h$ are arbitrary real numbers. A coloring is valid if it is injective on each clique and $f_h(x)\ne0$ for every $h$.

The form multigraph $G_{\mathcal F}$ has one vertex for each form and one edge for each variable, joining its two incident forms. It is loopless; parallel edges are allowed. A form is higher if its support has at least three variables. A vertex is noncut here when deleting it leaves its connected component connected.

Theorem 1 (arbitrary-list affine extension). If $|S_h|\ge3$ for every form, a valid coloring exists.

Theorem 2 (noncut higher-form criterion). The same conclusion holds with binary forms allowed, provided each connected form component either has exactly two vertices and at least three edges, or has at least three vertices and a noncut higher form.

A two-vertex component with only two edges is deliberately not included in Theorem 2. Nor may an arbitrary all-binary form component be processed after other components have consumed colors in its cliques: its remaining lists might be two-lists on an odd cycle. Section 5 instead settles all homogeneous histogram constraints by a simultaneous witness coloring; this is a different conclusion from making arbitrary affine numerical forms nonzero.

2.1. Strict constraint elimination

For a current variable set $W$, retain only forms not yet assigned to a removed variable. Their remaining supports lie in $W$; previously fixed variables contribute constants. Define

$$ \ell_W(v)=|N_C(v)\cap W|+ |\{h:\ h\text{ is active and }v\in S_h\}|. $$

If $\ell_W(v)<|L(v)|$, remove $v$, assign its active incident forms to it, and remove those forms from the active family. After the other variables have been colored, restore $v$. Each colored clique neighbor forbids at most one value. Each assigned affine form forbids at most one value because its coefficient at $v$ is nonzero. The strict inequality therefore guarantees a permitted value.

If all current loads are at most their list sizes and one vertex has strict slack, this slack propagates through any connected interaction graph formed by clique edges and pairs sharing an active form. Removing a clique neighbor or a shared form strictly decreases the load of the next vertex. Thus the whole connected system can be removed and restored.

3. A bounded signed-sumset lemma

Lemma 3. Let $1\le t\le5$ and $t<n\le9$. Let $A_1,\ldots,A_t$ be finite real sets of size at least $n$. Give $p$ coordinates sign $+1$ and $q=t-p$ coordinates sign $-1$. Among pairwise distinct choices $x_i\in A_i$, the signed sum takes at least

$$ t(n-t)+pq+1 $$

different values.

Proof. Put $m=t(n-t)+pq$ and choose the exponent vector

$$ e=(n-p,n-p+1,\ldots,n-1,\ n-q,n-q+1,\ldots,n-1), $$

with empty groups omitted. Then $e_i<n$ and

$$ \sum_i e_i=m+\binom t2. $$

Suppose the set of signed sums from distinct representatives had at most $m$ values, and pad it to a real set $D$ of size $m$. The polynomial

$$ P(x)=\prod_{d\in D}\left(\sum_i\varepsilon_i x_i-d\right) \prod_{i<j}(x_j-x_i) $$

vanishes on $A_1\times\cdots\times A_t$. Its degree is $\sum_i e_i$. The coefficient of $x^e$ is the coefficient of that monomial in its top homogeneous part

$$ \left(\sum_i\varepsilon_i x_i\right)^m\prod_{i<j}(x_j-x_i). $$

Writing permutations of $0,\ldots,t-1$ as $\pi$, this coefficient is

$$ C(t,p,n)=\sum_{\substack{\pi\in S_t\\\pi_i\le e_i}} \operatorname{sgn}(\pi) \frac{m!}{\prod_i(e_i-\pi_i)!} (-1)^{\sum_{i>p}(e_i-\pi_i)}. \tag{1} $$

It is nonzero for every one of the 110 triples

$$ 1\le t\le5,\qquad 0\le p\le t,\qquad t+1\le n\le9. \tag{2} $$

This bounded assertion is a finite algebraic part of the proof. The supplement gives every exact exponent vector and nonzero integer. signed_sum_coefficients.py checks (1) and independently expands the at-most-ten Vandermonde binomials before applying multinomial coefficients. verify_arbitrary_affine.py performs a further expansion check without importing a producer. All arithmetic is integer arithmetic. For example, when $t=5,n=6$, the values for $p=0,\ldots,5$ are

$$ -1,\ 2016,\ -147840,\ 147840,\ -2016,\ 1. $$

No numerical tolerance, solver verdict or experimental extrapolation enters (2).

For completeness, the coefficient principle used here follows from elementary interpolation. Choose $e_i+1$ elements $A'_i\subseteq A_i$. For a polynomial of total degree at most $\sum_i e_i$, the coefficient of $x^e$ equals

$$ \sum_{x\in\prod_i A'_i} \frac{P(x)}{\prod_i\prod_{b\in A'_i\setminus\{x_i\}}(x_i-b)}. \tag{3} $$

Apply univariate Lagrange interpolation to monomials: any monomial other than $x^e$ of that total degree has some coordinate exponent below $e_i$ and contributes zero. The denominators are nonzero. Since $P$ vanishes on the grid, (3) contradicts $C(t,p,n)\ne0$. This proves the lemma. $\square$

For finite nonempty real sets, we also use

$$ |A+B|\ge |A|+|B|-1. \tag{4} $$

An increasing chain from the minimum to maximum, first varying one summand and then the other, proves (4).

4. Proofs of the affine theorems

Process connected components of $G_{\mathcal F}$ one at a time. Delete the colors of already colored clique neighbors from each current list. If a current clique has $s$ variables in this component, every available list still has size at least $s+1$. Lists need not lose the same number of colors. Their upper bound remains nine.

4.1. Choosing roots

Suppose the form component has at least three vertices, and choose a noncut higher form $h$. Such a vertex exists under Theorem 2; under Theorem 1, any leaf of a spanning tree is noncut and every form is higher.

Choose a variable $v\in S_h$ whose available list is shortest, of size $n\ge2$. Leave $v$ free and let the other variables $R=S_h\setminus\{v\}$ be roots. There are at least two roots.

In one root clique, let $t$ be the number of roots, $p$ the number with positive coefficient in $h$, and $N$ their minimum available list size. The spare-list inequality gives $t<N\le9$, and $N\ge n$. Lemma 3 gives at least

$$ t(N-t)+p(t-p)+1 $$

possible signed root sums with injective assignments in this clique. Assignments in different root cliques are independent. By (4), the full root-sum set has size at least

$$ 1+\sum_C\left[t_C(N_C-t_C)+p_C(t_C-p_C)\right]. \tag{5} $$

A suitable minimum-list choice of $v$ makes (5) greater than $n$.

If roots meet at least two cliques, each nonempty summand is at least $N_C-1\ge n-1$, giving at least $2n-1>n$ values. If all roots meet one clique, write $t\ge2$ for their number. For $N\ge t+2$,

$$ t(N-t)\ge N, $$

so (5) exceeds $n$. If $N=t+1$, (5) is $N+p(t-p)$ and fails to exceed $n$ only when $N=n$ and all root signs agree. Then $v$ is outside the root clique: otherwise that clique's spare-list inequality would force $N\ge t+2$. Switch the free variable to a root whose list has size $N=n$. The new roots meet two cliques, and the earlier bound applies.

For a root sum $s$, the unique value at $v$ that could make $f_h$ zero is

$$ -\varepsilon_{hv}(s+\kappa_h). $$

At most $n$ root sums put this value in $L(v)$. Choose a different sum and its actual proper root assignment. Form $h$ is now nonzero for every permitted later value at $v$.

4.2. Connected restoration

No other form becomes constant after the roots are assigned. Otherwise all of its incident variables would join that form to $h$, isolating it when $h$ is removed from a component with at least two remaining form vertices.

Substitute the roots into the other forms and discard the now-safe $h$. If a clique had $s$ current variables and $r$ roots, a remaining variable loses at most $r$ list values and has clique degree $s-r-1$. It retains at most two form incidences, so its load is at most its remaining list size. At $v$, deleting $h$ creates strict slack.

The remaining interaction graph is connected even using just shared forms. The variables not incident to $h$ are the edges of the connected form graph with $h$ deleted; their line graph is connected. Variable $v$ attaches through its other endpoint. Section 2.1 therefore removes and restores all remaining variables. Every affine form is nonzero and every clique is properly colored.

Left: a noncut form h in a four-form graph, with two red root variables and one blue free variable. Right: after the roots are precolored and h is made safe, the remaining variables form a connected interaction graph with strict slack at the free variable.

Figure 1. An illustrative noncut-root choice. Clique edges are omitted; adding them does not destroy the connectedness used for propagation. The diagram illustrates the proof and is not a retained computational instance.

4.3. Two-form components

Here the two linear coefficient vectors are opposite, but their constants may differ. The common signed sum must avoid at most two values. Apply Lemma 3 to all variables, grouped by clique. If a clique contains $t$ component variables and its shortest current list has size $N\ge t+1$, its contribution to the lower bound is at least $t$. Thus the full sumset has size at least

$$ 1+\sum_C t_C\ge4. $$

Choose a sum avoiding the two forbidden values, with its recorded proper clique assignments. This handles every two-form component allowed in Theorems 1 and 2 and completes both proofs. $\square$

Corollary 4 (precolored variables). Suppose the hypotheses of Theorem 1 hold and every original support has size at least four. Any proper precoloring meeting each form at most once extends. In particular, any one variable may receive any allowed color.

Proof. Delete the precolored variables and their colors from clique neighbors. A clique loses distinct assigned colors and equally many variables, preserving the spare-list inequality. Each form loses at most one variable, so its remaining support has size at least three. Substitution produces arbitrary affine constants but preserves opposite incidences at every remaining variable. Apply Theorem 1. $\square$

5. Simultaneous witnesses for all histogram constraints

The affine theorems concern numerical values and arbitrary constants. For the cover application, it is enough to make a form's signed color-multiplicity vector nonzero. If $c$ is a coloring and a homogeneous form has positive support $P_h$ and negative support $N_h$, define

$$ \Delta_h(a)=|\{v\in P_h:c(v)=a\}|-|\{v\in N_h:c(v)=a\}|. $$

We require $\Delta_h\ne0$, which means that at least one color has unequal multiplicities. This does not imply that the numerical signed sum of the color labels is nonzero. The following theorem handles arbitrary mixtures of binary and higher forms by coloring all witness variables simultaneously.

Lemma 5.1 (cliques and a pseudoforest). Let $k\ge3$. A finite simple graph that is the union of vertex-disjoint cliques of size at most $k$ and a pseudoforest is $(k+1)$-list-colorable.

Proof. A pseudoforest is a graph whose connected components each contain at most one cycle; every induced subgraph on a set $S$ has at most $|S|$ edges. The clique part contributes at most $(k-1)|S|/2$ edges. Therefore every induced subgraph has average degree at most $k+1$.

Repeatedly remove a vertex of degree at most $k$. The remaining core, if nonempty, has minimum degree at least $k+1$ and average degree at most $k+1$, so every component is $(k+1)$-regular.

The graph contains no $K_{k+2}$. Partitioning its hypothetical vertices among the original cliques gives parts of size at most $k$. The fewest cross-part edges occur for parts of sizes $k$ and $2$, and number $2k$. All these edges would belong to the pseudoforest, but $2k>k+2$ for $k\ge3$, a contradiction.

A connected $(k+1)$-regular core component cannot be a Gallai tree. In a leaf block of a Gallai tree, a noncut vertex has degree at most $k$: a clique block has at most $k+1$ vertices, and an odd-cycle block gives degree two. This contradicts regularity. The connected degree-choosability theorem [8] therefore colors each core component from its lists, whose sizes are at least its degrees. Restore the removed vertices greedily. $\square$

This lemma is an elementary application of classical degree-choosability; no priority is claimed for the graph lemma itself. Its restriction $k\ge3$ is genuine: two disjoint $K_2$s together with a four-cycle can form $K_4$.

Theorem 5 (simultaneous signed witnesses). Let variables be partitioned into cliques of size at most $k\ge3$, with lists of at least $k+1$ colors. Let each signed form have disjoint nonempty positive and negative supports, and suppose every variable has at most one negative form incidence. Then the cliques can be properly list-colored so that every signed color-multiplicity vector is nonzero.

Proof. For each form $h$, choose any positive witness $r_h\in P_h$. For every $v\in N_h$, add the arc $v\to r_h$. There are no loops, and each variable has outdegree at most one. Consequently every vertex subset spans at most as many underlying witness edges as vertices; the underlying simple witness graph is a pseudoforest. Opposite arcs, if present, are simplified to one edge.

Apply Lemma 5.1 to the union of the witness graph and the clique graph. The color $c(r_h)$ occurs at least once positively in form $h$ and never negatively, so $\Delta_h(c(r_h))>0$. $\square$

There is no bound on positive incidences in Theorem 5. In particular, it applies whenever each variable has two opposite incidences, as in the tight core of Section 6. It also places no restriction on how many witnesses lie in one clique. Their colors are chosen simultaneously; this is not an extension theorem for arbitrary prescribed witness colors.

The list bound is sharp. Take two $K_k$s, give every variable the same list of $k$ colors, and impose the two opposite forms comparing the cliques. Every proper coloring uses each color once on each side, so both multiplicity vectors vanish. Every variable has exactly two opposite incidences. This is an abstract list-system lower bound, not a nine-color obstruction in the literal cover application.

Theorem 5 replaces the earlier at-most-two-higher-form histogram criterion. It does not subsume the arbitrary-constant numerical statements of Theorems 1 and 2 or their precoloring corollary.

6. Three-source cover extension

6.1. Literal architecture and exact head interface

Use source labels

$$ A=\{0,\ldots,6\},\quad A_1=\{0,1\},\quad A_2=\{2,3\},\quad A_3=\{4,5,6\}, $$

with arms $\{7,\ldots,11\}$, $\{12,\ldots,16\}$, $\{17,\ldots,21\}$ and centers $\{22,23,24\}$. An ordinary finite cover replaces each source vertex by an independent fiber and each source edge by a perfect matching. We assume internal host components are $K_7$s, internal arm components are $K_5$s, and the two small ports are local: each host's $A_i$ is complete to its own retained $B_i$ for $i=1,2$. The five matchings from each of sources $4,5,6$ to $B_3$ are arbitrary and independent. All center matchings and internal center cycles are arbitrary. Fix any proper nine-coloring of those centers.

Let $U$ be its nine-color universe. A large-arm vertex $v$ has a list

$$ L(v)=U\setminus T_v, $$

where $T_v$ is the set of colors on its three center neighbors. Thus $|L(v)|\ge6$, with no requirement that lists agree inside an arm clique.

Color the large-arm cliques from these lists. At a host, the three head vertices in $A_3$ have lists $Q_1,Q_2,Q_3$ of size at least four. The two small arms impose demands only when their five center-color sets are all the same three-set. A uniform small arm with three-set $T$ asks its two-vertex port to meet $T$; a nonuniform small arm asks nothing. This is the elementary $K_5$ list Hall test used in [2].

For a chosen head triple $H$, the two small ports extend exactly when their zero, one or two demand sets $T\setminus H$ have distinct representatives. After choosing those representatives there are six colors outside $H$ and only four small-port vertices to fill, so the remaining port colors can be completed distinctly. Their arm cliques then extend by Hall.

Lemma 6 (exact arm-first failure). The host fails to extend exactly in one of the following cases:

1. Both small arms are uniform with the same triple $T$, and $$Q_1=Q_2=Q_3=T\cup\{z\}\quad\text{for some }z\notin T.$$
2. The small arms are uniform with distinct triples whose union is a four-set $V$, and $$Q_1=Q_2=Q_3=V.$$

Proof. In the first case a permitted head triple must use at least two colors outside $T$. Each $Q_i$ has an outside color. Two distinct outside colors can be put on different heads unless all outside parts are the same singleton. With $|Q_i|\ge4$, that exception forces all lists to be $T\cup\{z\}$. After choosing the two outside colors, the third head has a spare list color.

In the second case a permitted head triple must not be contained in $V$. Choose an outside color at any head if possible, and then greedily complete the triangle. Failure means every head list is exactly $V$.

For one uniform small arm, the only forbidden unordered head triple is its triple $T$. For two distinct uniform triples whose union has size at least five, the only forbidden triples are the two given triples. Three lists of size at least four have at least four different proper unordered head triples: take any proper assignment and replace each of its three colors, in turn, by a list value outside its original three-set. The original and three replacements are different unordered triples. Hence at least one is permitted. With no uniform arms there is no demand. These arguments also prove necessity in the two stated failures. $\square$

In either failure, all three head neighborhoods see the same rainbow five-color set. Thus any nonzero difference of two neighborhood color-multiplicity vectors prevents failure.

6.2. Coherent neighborhoods

An intact light component is a connected component after deleting all lifted center vertices that projects isomorphically to $G_{25}-C$. It is a literal copy, not merely a collection of intact host and arm cliques.

Call a host coherent if all three actual large-arm neighborhoods are the same five-set $N$. Every variable of $N$ then has all three head neighbors at that host and affects no other host's head lists.

If a coherent host fails in the four-union case, any alternative color at a vertex of $N$ breaks its forbidden five-palette. Such an alternative exists since the vertex has at least six list colors and only four clique neighbors.

In the equal-triple case the current neighborhood palette is $U\setminus(T\cup\{z\})$. If any alternative differs from $z$, recoloring that vertex either inserts a color of $T$ or repeats a neighborhood color, repairing the host. Otherwise $z$ is the only alternative at every vertex. If $N$ meets two arm cliques, recolor one vertex in each to $z$. The two moves are compatible, create a repeated neighborhood color, and affect no other host.

If $N$ is itself a whole arm clique, the absence of any $T$-colored alternative forces all its lists to be $U\setminus T$. Both small arms were also uniform with $T$. This is exactly an intact light component whose fifteen center-color sets equal one triple. Conversely, that configuration cannot extend: the two small ports require one color each from $T$, and the three-head port requires at least two, demanding four distinct host colors in a three-set. The arm clique may have a different sheet label from the host; the condition concerns literal adjacency, not names of columns.

6.3. Adaptive comparisons and the tight core

Write $N_i(h)$ for the five large-arm neighbors of source-$i$ head at host $h$. If $N_4(h)\ne N_5(h)$, impose the baseline form

$$ f_h=\sum_{v\in N_4(h)}x_v-\sum_{v\in N_5(h)}x_v. $$

If $N_4(h)=N_5(h)\ne N_6(h)$, impose the repair form

$$ f_h=\sum_{v\in N_4(h)}x_v-\sum_{v\in N_6(h)}x_v. $$

A coherent host imposes no form. Cancel common variables in each form. Every nonzero form is homogeneous and balanced; a change in one source row gives support two, and changes in at least two rows give support at least four.

A variable occurs in either zero or two baseline forms. Indeed, its unique source-4 and source-5 neighbors either belong to the same host and cancel, or belong to two distinct baseline hosts. Positive variables in a repair form are baseline-free. Their positive sets are disjoint between repair hosts, by the source-4 perfect matchings. Each variable is negative in at most one repair form, by the source-6 perfect matchings.

For any active family whose full supports remain inside $W$, charge baseline incidences directly, at most two per baseline variable. Charge a repair form's entire support to its private positive variables, two units each, since the positive and negative sides have equal size. These charged variable classes are disjoint, so

$$ \sum_{h\text{ active}}|S_h|\le2|W|. \tag{6} $$

Apply the strict elimination of Section 2.1 using the actual incidence load and the center-avoiding lists. Active supports remain entirely inside the current set. Clique degrees are at most four and list sizes at least six.

For the unpeeled set $W$, let $\ell_W(v)$ be the remaining clique degree plus the number of active forms containing $v$. Since no strict elimination is possible,

$$ 6|W|\le\sum_{v\in W}|L(v)|\le\sum_{v\in W}\ell_W(v) \le4|W|+2|W|=6|W|. $$

Every inequality is equality. Thus every surviving clique is whole, every list has size six, and every actual form incidence count is two. A baseline variable already uses both incidences and has no repair incidence. Every other variable is positive in exactly one repair form and negative in exactly one repair form. Thus all surviving variables have exactly two opposite coefficients. Baseline and repair forms may share cliques, but their surviving variable supports are disjoint.

6.4. Unconditional tight-core extension

Theorem 7 (three independent sources). In the architecture of Section 6.1, a prescribed proper nine-coloring of the centers extends if and only if no intact light component has all fifteen center-color sets equal to one triple.

Proof. Perform the adaptive comparison elimination of Section 6.3. Every nonempty tight remainder has whole $K_5$s, arbitrary six-lists, and exactly two opposite incidences per variable. Apply Theorem 5 with $k=5$ to color all its binary and higher forms simultaneously with nonzero multiplicity vectors.

Restore initially removed variables using the color-multiplicity predicate. With all other colors fixed, a form with a nonzero coefficient at the restored variable forbids at most one color: different colors have different unit vectors. Thus its original strict load bound remains valid even when the core construction supplies only a nonzero multiplicity vector, rather than a nonzero numerical sum.

Every noncoherent host now has one comparison with a nonzero multiplicity vector, excluding the rainbow five-palette equality in Lemma 6. Coherent hosts have the independent repairs of Section 6.2 unless they are the stated obstruction. Their variables occur in no comparison at any other host, so these repairs preserve all guarantees. Finish each head triangle and its private small ports and arms by Lemma 6. Necessity of the intact uniform obstruction was proved in Section 6.2. $\square$

The former residual alternatives—a suitable noncut higher form or at most two higher forms in each interaction component—are not needed for this theorem. The source matchings of all three large-port vertices may move independently. The intact host/arm cliques and local-small-port assumptions are the architecture of Theorem 7. Section 7 allows either small port to move and then characterizes the larger one-nonfull-port-per-host class.

7. Any one nonfull port per host

Use the ordinary $G_{25}$ cover model: retained $K_7$ host components with source ports A1,A2,A3 of sizes 2,2,3; retained $K_5$ arm components of each of the three arm types; and arbitrary center-source matchings and internal center cycles. A port is full if its entire set of heads is complete to one retained arm clique of the corresponding type. No sheet-label coherence is assumed. A light component means a component after deleting all centers. It is intact when it consists of one host and three full arm cliques.

Theorem 8 (one nonfull port per host). Suppose each host has at most one nonfull port. Any proper prescribed nine-coloring of the centers extends if and only if no intact light component has all fifteen center-neighbor color sets equal to one three-set. The unrestricted Earth–Moon problem is not asserted.

Corollary 9 (center choice). Under the same retained-clique and one-nonfull-port hypotheses, the cover is nine-colorable if and only if it has no trivial component isomorphic to $G_{25}$ projecting identically by source.

7.1. Exact two-head interface

Let the moving port be A1. Color its arm-type vertices first, respecting clique edges and the fixed centers. Each remaining head has an available list $Q_1$,$Q_2$ of size at least four. The private A2 and A3 arms have row center-color sets of size at most three. For a small private arm there is one representative demand from S exactly when all five row sets are the same three-set S; otherwise there is no demand. For the large private arm:

• intersection T of size three gives two distinct representatives from T;
• intersection R of size two gives one from R;
• otherwise a three-set repeated in at least four rows gives one from it;
• otherwise no demand.

These are precisely the earlier local Hall conditions. After a proper head pair H is chosen, meet all private demands by distinct representatives outside H, fill the two private port palettes to sizes two and three, and then match each private $K_5$ to its lists.

The two-head extension fails exactly in these two cases:

1. Both private arms have the same uniform three-set T, and $Q_1=Q_2=T\cup\{z\}$, where z is outside T.
2. Both private arms have distinct uniform three-sets S,T with $|S\cup T|=4$, and $Q_1=Q_2=S\cup T$.

Proof of completeness. If the large arm has at most one demand, there are at most two demand sets, with sizes at least two and, when the small one is present, three. A head pair can fail only by exhausting a size-two set or leaving their union with fewer than two names. If the union has size three, all bad pairs lie inside that three-set; if larger, only an exhausted size-two demand can fail. Thus at most three unordered pairs fail. Lists of size at least four admit at least six unordered proper pairs: choose four colors from each list; the number of unordered pairs is minimized by equal four-sets. Hence an admissible pair exists.

Now the large demand is two from a uniform three-set T. With no small demand, or a small uniform S with |S union T|>=5, any proper pair having at least one color outside T works by Hall. Such a pair exists because both head lists have size at least four. If S differs from T and their union V has size four, exactly the pairs using a color outside V work: a pair contained in V either exhausts two colors of T, or leaves only two names for three demands. A pair using an outside color exists unless both lists equal V. Finally if S=T, all three names of T are needed privately, so both head colors must be outside T. Each $Q_i$ has a nonempty outside part. Distinct representatives fail exactly when both outside parts are the same singleton, forcing both $Q_i$=T union {z}. This proves the list classification, including lists of size greater than four.

7.2. Both sources of a small port may move independently

For each host h let $N_0$(h),$N_1$(h) be the five actual arm neighbors of its two moving heads. If these sets differ, impose their signed color-histogram comparison with +1 on $N_0$ minus $N_1$ and -1 on $N_1$ minus $N_0$. Each arm variable has zero or two opposite incidences: the two source perfect matchings supply one positive and one negative incidence, unless they cancel at the same host. Its list has at least six colors; its clique degree is four.

Peel a variable whenever remaining clique degree plus active comparison incidence is less than its list size; assign its incident forms to that step. If a nonempty core remains, equality throughout forces whole $K_5$s, six-lists, and two opposite active incidences at every variable. Each surviving form retains its entire support (a removed incident variable would have removed it). Apply Theorem 5: choose one positive variable for each form, point every negative variable to its witness, and list-color the union of the cliques and the resulting pseudoforest. Restore the strict peels. With every other color fixed, each assigned histogram comparison forbids at most one color.

Thus all unequal neighborhood pairs have unequal color histograms. Both failure patterns of Section 7.1 require equal four-element head lists; then both five-neighborhoods use exactly the same five colors, each once, contradicting the comparison. Only hosts with $N_0$=$N_1$ can need repair.

At such a host put N=$N_0$=$N_1$. Its vertices have no moving-head neighbors at other hosts, so changing them cannot spoil another head interface. If N currently causes the four-union obstruction, any legal alternative at one vertex changes its rainbow palette or creates repetition and repairs it. Every vertex has an alternative, since its list has size at least six and it has four clique mates.

For the equal-triple obstruction write Q=T union {z}. A legal alternative other than z again repairs it. If every alternative at every vertex of N is z, two vertices in different arm cliques can both be recolored z, creating repetition in N and increasing both head-list sizes. If there is no such pair, N is an entire $K_5$. Its rainbow palette is U minus (T union {z}); the lack of alternatives other than z forces each of its five lists to be U minus T. Thus the moving arm and both private arms have all fifteen row-center sets equal to T. This is exactly an intact uniform light obstruction. Conversely that obstruction cannot extend by the previously proved 1+1+2 representative demand count on three names.

This proves the arbitrary-center extension theorem for one moving small port. The other small port is symmetric. Theorem 7 proves the moving large-port case.

7.3. Why different hosts may choose different nonfull ports

A full port exhausts all head incidences of its attached arm: every arm vertex already has its unique neighbor in every source of that port. Therefore that arm is private to this host. Conversely, any arm touching several hosts can meet only nonfull ports. Suppress private arm leaves in a light component. Each remaining arm has a fixed source type, and a host incident to it has this type as its unique nonfull port. Consequently a path between hosts preserves the moving-port type. Every nontrivial light component has one fixed moving type; its other two arms are private.

The numbers of hosts and arms of each type in any light component agree, by counting the incidences of one source pair. Relabel retained cliques independently within their source types. Align the two private arm types with the host labels and label the moving arm cliques arbitrarily. This puts the light component into exactly the one-moving-port architecture already proved. The literal center boundaries need not stay within this component: the theorem uses their prescribed colors, not a closed center subcover. Solve the light components independently with the same fixed center colors. Intact components obey the same exact local criterion.

7.4. Center choice, with full compatibility

Apply the center-coordination construction of [2] only to intact light components. For each component whose center neighborhoods are not fully concentrated, select one dispersed center source. Its fifteen distinct incidence slots, and at most fifteen such slots per actual center, give distinct Hall anchors. Direct each anchor to another neighbor of the same source. The sourcewise pseudoforests are three- colorable using disjoint three-color palettes; all these selected components then have nonuniform row-center sets.

A fully concentrated intact component has three private actual centers, since their fifteen arm incidences are exhausted there. If the triple forms an actual triangle, it is a trivial $G_{25}$ component. Otherwise identify a nonedge pair for coloring purposes. The equality pairs are disjoint; in the quotient the still-uncolored private vertices have degree at most four. They extend greedily from nine colors, and the concentrated component now sees at most two center colors. Private triples cannot alter other light boundaries. The other center vertices were already properly colored by the disjoint source palettes.

All intact components now extend, and Sections 7.2–7.3 extend all remaining components under these very same center colors. Necessity is the trivial $G_{25}$ palette obstruction. No biplanarity is assumed in this theorem.

8. Two moving small ports with an overlapping pair

Retain $K_7$ hosts and all three types of $K_5$ arm cliques, and keep the large port full/local. Both small-port source matchings are arbitrary. Prescribe any proper nine-coloring of the centers. At host h, write $N_0$,$N_1$ for the five neighborhoods of the first small-port pair, and $N_2$,$N_3$ for the second.

Theorem 10 (overlapping small-port pairs). Suppose at every host at least one small-port pair overlaps: $N_0\cap N_1\ne\varnothing$ or $N_2\cap N_3\ne\varnothing$. The prescribed centers extend if and only if no intact light component has all fifteen row-center color sets equal to one three-set. In particular, the center coordination of [2] gives nine-colorability if and only if there is no trivial $G_{25}$ component.

One pair may be coherent (even full) while the other splits all five rows; both pairs may be noncoherent and overlap; or both may be coherent while their common neighborhoods disperse across arm cliques. No biplanarity is assumed. The host and private large-arm cliques may be relabeled to make the large ports local, without requiring center subcover closure.

8.1. Pair comparisons and exact Hall defects

Color both moving arm types, comparing the two neighborhoods at every noncoherent pair. Variables of each arm type have zero or two opposite incidences, and different arm types share neither variables nor cliques. Strict peeling and Theorem 5 give a proper arm coloring with all these histograms nonzero, from the center-avoiding lists of size at least six. The argument is identical to Section 7.2 and permits all binary/higher mixtures.

Each head has list $Q_i$ of size at least four. Nonzero histogram on a pair implies that its two Q lists cannot be the same four-set: in that case both five-neighborhoods would have the same rainbow color histogram. Thus each noncoherent pair's Q-union has size at least five. This does not assert that the Q lists themselves must differ when their sizes exceed four.

First consider a host with at least one noncoherent pair. The private large arm supplies zero or one representative demand, or two copies of a three-set T if all its row-center sets equal T. The exact host condition is an SDR for $Q_0$,$Q_1$,$Q_2$,$Q_3$ and these demands. Zero demand always extends. One demand can fail only when all four Q lists are the same four-set containing that demand, impossible since there is a noncoherent pair. For two demands, Hall fails only if:

(a) three Q lists equal one four-set containing T; or (b) V = $Q_0$ union $Q_1$ union $Q_2$ union $Q_3$ union T has size at most five.

All smaller Hall subfamilies are automatically large enough; these are exactly the remaining size-five and size-six tests.

8.2. Both pairs noncoherent

Condition (a) is impossible: any three heads contain a whole pair. In (b), each pair union has at least five colors, so V is a five-set and each pair union is exactly V. Write S=U minus V, a four-set. Every head neighborhood contains all four colors of S.

Choose a vertex v shared by the two neighborhoods of an overlapping pair. Its color s must be in S. Otherwise each neighborhood's five vertices consist of the four S colors and s, giving equal histograms, contradiction. Moreover s occurs exactly once in at least one of those neighborhoods. If it occurred twice in both, both histograms would be S with one extra s, again equal. These conclusions hold for any shared vertex.

Recolor v to any different legal list color a. Such a color exists since v has at least six permitted colors and four clique neighbors. The head where s was unique gains s in its list. The other small-port pair still has Q-union V, so the total union now has at least six colors. Recoloring a shared vertex preserves the pair comparison: it cancels from the signed form. Both pairs therefore still prohibit (a). The host now extends.

8.3. Exactly one pair coherent

Write Q,Q for the coherent pair's lists, and A,B for the other pair. We have |A union B|>=5. The shared coherent neighborhood N has five vertices, and every one affects only this host's moving heads.

If (a) holds, Q is a four-set, one of A,B equals Q, and T subset Q. The other list differs; put Z=A union B. The neighborhood N is rainbow with palette U minus Q. If |Z|=5, choose a vertex whose color s is outside Z; at least four such colors lie in N. Any different legal recoloring makes the new coherent list Q' contain s. Then Q' differs from A and B, and the full union contains Z union {s}, of size six.

If |Z|>=6, recolor any vertex of N. The full union already contains Z, so (b) is impossible afterwards. The new coherent list differs from Q; it cannot equal the other four-list either, because changing one rainbow neighborhood color can replace at most one member of Q, whereas a different four-list with |Q union B|>=6 differs by at least two. If the new list has size five, (a) is also impossible. Thus the move repairs the host.

It remains to repair (b) when (a) does not hold. Put V as in (b); then A union B=V is a five-set. If |Q|=4, N is rainbow and contains the four colors outside V; choose one. If |Q|=5, Q=V and N uses exactly the four colors outside V. At least three of these four colors occur only once among the five vertices, so choose a vertex with such a unique color s. In both cases a different legal recoloring makes Q' contain s outside V. Now Q' differs from A and B, and the total union has size at least six. Again both Hall obstructions disappear.

8.4. Both pairs coherent

Fix the colors outside the two coherent neighborhoods N and M. Partition each neighborhood by its retained arm cliques. A part with n vertices has residual lists of size at least n+1, because each original list has at least six colors and at most 5-n fixed outside clique neighbors. Within a part the vertices must receive distinct colors; there are no edges between different parts or between the two arm types.

A head pair H makes such a part uncolorable exactly when all its residual lists are the same (n+1)-set A containing H. Indeed after deleting H each list has size at least n-1. Every proper subset of the n rows satisfies Hall, so failure means all remaining lists are one (n-1)-set. The original lower bound then forces identical A of size n+1 and H subset A. Thus the part forbids at most binomial(n+1,2) unordered head pairs.

The part sizes sum to five. Each coherent neighborhood forbids at most 15 of the 36 pairs in U. Equality in this bound is possible only for one whole $K_5$ with an identical residual six-list A; then its forbidden pairs are exactly the pairs contained in A. A split neighborhood forbids at most 11 pairs, since the maximum split partition is 4+1.

There is always a pair choice for both ports if the private large arm needs zero or one representative. With no demand, choose any allowed first pair; the remaining seven colors supply 21 pairs, more than the second port's at most 15 forbidden pairs. With one demand R, reserve any t in R. In U minus {t} there are at least 28-15=13 choices for the first pair. For each choice, the remaining six colors supply 15 second pairs. They can all fail only when the second neighborhood is a whole $K_5$ with one identical six-list equal to those six colors. This determines at most one first pair, so another choice succeeds and leaves t for the private demand. Complete the private three-head palette with unused names.

Now the private large arm demands two representatives from a uniform three-set T. Put O=U minus T, of size six. If either coherent small port admits an allowed pair H entirely in O, choose it first. Among the other four O colors and three T colors, the other port has 6+12=18 pairs using at most one T color, exceeding its at most 15 forbidden pairs. Choose an allowed one. The four small heads then use at most one T color and leave two distinct representatives for the large arm.

The only remaining possibility is that both neighborhoods forbid all 15 pairs contained in O. Equality in the counting bound forces each to be a whole $K_5$ with identical residual six-lists O. Since these are whole cliques there are no fixed outside clique neighbors: every original center-color set on both moving arms is T. The private large arm was also uniform in T. Both small ports and the large port are full, giving exactly the intact uniform light obstruction. Its nonextension is the usual four representative demands on three names.

For every other coherent host, choose the guaranteed pairs and match its two neighborhoods independently inside their clique parts from the fixed- outside residual lists. This may recolor several private arm vertices, but all of them affect only this host's head lists.

8.5. Global compatibility

Every chosen repair vertex is shared by the two heads of one small port. The source perfect matchings imply that it has no small-port head neighbor at any other host. Its only noncenter/nonclique neighbors are those two heads. A legal recoloring therefore preserves all arm clique colors, center avoidance, pair histograms everywhere, and head lists at other hosts. Each bad host with a noncoherent pair requires at most one single-vertex repair. A host with both pairs coherent uses the bounded local clique-part matching construction. The repairs may be performed in any host order. Afterward extend each host and private large arm by the exact SDR interface. This proves the theorem.

9. Two moving small ports with individual full heads

Theorem 11 (individual full head neighborhoods). Retain the $K_7$ hosts and $K_5$ arms of an ordinary $G_{25}$ cover, and assume the large port is full. Suppose every individual small-port head is complete to one retained arm clique. The two heads of a small port may see the same or different cliques. Any prescribed proper nine-coloring of the centers extends if and only if there is no intact light component whose fifteen row-center sets are one three-set. Consequently the cover is nine-colorable if and only if it has no trivial $G_{25}$ component.

The large arm can be relabeled to be local. An individual full head is not a full port: the latter requires both heads to see the same clique. Neither small head may disperse its own five neighbors among several arm cliques in this theorem. The overlap theorem treats a different class; arbitrary mixtures of their hypotheses are not asserted.

9.1. Arm variables, host edges and private loops

For either small-arm type, a retained $K_5$ has precisely two neighboring heads, one of each port source. When the heads lie at different hosts, require them to use the same color, represented by a variable for that arm. This is a coloring identification and makes no geometric claim. Its $K_5$ then has center-avoiding lists of size at least five and extends. Each host contributes an inequality edge between its two arm variables. The resulting multigraph is degree two, counting parallel edges.

If the heads lie at the same host, identifying them would create a loop and violate the host clique. Instead keep the port and its arm private. Such a loop is an isolated component of its type's degree-two multigraph. If both small ports at a host are full, its light component is intact. Remove and solve these components by the exact local criterion. We now work only at hosts where at least one small port is nonfull.

The private large arm has the usual demands: none; one from a set $R_h$ of size two or three; or two from a uniform three-set $R_h$. Put $R_h$ empty when there is no demand.

9.2. First small port and exceptional private hosts

On the nonloop first-type cycles, a variable meeting hosts h,j receives list U minus ($R_h$ union R_j), of size at least three. Properly color this degree-two graph greedily. The two first head colors at every such host form a pair $P_h$ disjoint from $R_h$.

At a private first-type port, its arm either has no demand or asks for one representative from a uniform triple $S_h$. If $S_h$ is not contained in $R_h$, choose its representative outside $R_h$ and complete the pair there; if it has no demand choose any pair outside $R_h$. All these pairs are proper and satisfy the private small-arm condition.

The sole remaining case is $S_h$=$R_h$, a three-set. Call h blocked and defer its first pair. Eventually it will use one color of $R_h$ and one outside, while both second-port head colors will avoid $R_h$. Since intact hosts were removed, a blocked host has a nonfull second port. This applies whether its large arm needs one or two representatives from $R_h$.

9.3. The graded cycle lemma

A nonloop second-type variable receives the nine colors minus $P_h$ at an unblocked endpoint h and minus $R_h$ at a blocked endpoint. If b of its two endpoints are blocked, it has at least 5-b colors. At every host the second heads must differ. At an unblocked host also forbid both second colors from lying in $R_h$; at a blocked host there is only the ordinary inequality, since both lists already avoid $R_h$.

Let r be the number of incident nonempty-palette constraints in this second cycle system. We have r<=2-b, so the list bound 5-b is at least 3+r. The following lemma colors these lists. It includes parallel edges and arbitrary palettes of size at most three.

Lemma 11.1 (graded cycle lists). Let G be a loopless graph of maximum degree two, allowing parallel edges. Each edge has either an ordinary inequality or, in addition, the condition that its endpoints are not both in a specified set $T_e$ of at most three colors. Let $r(v)$ be the number of nonempty-palette edges incident to v. Lists of size at least $3+r(v)$ suffice. Thus ordinary/ordinary vertices need three colors, mixed vertices four, and palette/palette vertices five.

Proof. For an all-ordinary component use ordinary three-list coloring. For an all-palette cycle, orient cyclically and delete each outgoing edge palette from its tail list. At least two colors remain. Any proper coloring of these reduced lists satisfies all palette conditions. The only possible failure is an odd cycle with all reduced lists equal to one two-set D: cycles with unequal two-lists, or a larger list, color by the usual path argument. In that exception, each original list consists of D plus its outgoing three-set, disjoint from D. Give one vertex a color from that three-set and alternate the two D colors along the remaining path. The edge leaving the exceptional vertex has its other endpoint in D, outside its palette; every other edge has a tail outside its palette. All edges are proper. Parallel two-cycles color from two lists of size at least two.

For a mixed cycle, select a vertex u whose preceding edge is ordinary and whose outgoing edge has a nonempty palette. Choose $c(u)$ outside that outgoing palette, possible because |$L(u)$|>=4. Traverse the path around the cycle from u's outgoing neighbor to its ordinary-edge predecessor. Track the set B of feasible current colors, retaining a predecessor for each (not merely one greedily chosen prefix).

The first neighbor loses at most the chosen color, since $c(u)$ lies outside the first palette. If its next edge has a palette then its list has size at least five, so B has size at least four and cannot be contained in that three-set. If its next edge is ordinary, B has size at least three, hence at least two. In either case every color at the next vertex becomes feasible: for a palette edge, a set B of at least two colors containing one outside T has a compatible member for every target color; for an ordinary edge, two distinct colors suffice.

Thereafter each intermediate feasible set is its entire original list. On a next palette edge its size is at least four (the vertex has at least one palette incidence), so it again contains an outside color and has at least two members. On an ordinary edge it has at least three. Thus feasibility propagates without further restriction. The last vertex has its whole list available, and can avoid $c(u)$ on the closing ordinary edge. Backtrack the retained predecessors. A parallel two-cycle with one edge of each kind is even simpler: after choosing u outside the palette, its neighbor need only avoid $c(u)$ from a list of at least four.

For a path, remove an endvertex v, recursively color the shorter path, and restore v. An ordinary edge forbids at most one color from a list of size at least three. A palette edge forbids at most three colors from a list of size at least four. Removing an edge only decreases the neighbor's required list bound. This completes the lemma by induction, without any assumed perfect-matching property of the palette relation.

The five-color bound for two palette incidences is sharp: on an odd cycle give every vertex the same four-list consisting of a triple T and one extra color, and place T on every edge. The vertices using the extra color would have to be both independent and a vertex cover, impossible. This is an abstract cycle control, not a literal-cover nonextension.

Apply Lemma 11.1 to the second cycle system.

At a blocked host the now-fixed second pair lies outside $R_h$. Choose one first head color in $R_h$ and the other outside $R_h$, avoiding the two second colors. At least four outside choices remain. Its private first arm extends. At least two colors of $R_h$ remain available for the large arm, enough for either of its possible demands.

At an unblocked host with a nonfull second port, the first pair avoids $R_h$ and at most one second color belongs to $R_h$. Thus the single demand retains a color, or the double demand retains two.

9.4. Complete the second ports and all arms

A full second port can occur only at an unblocked host after intact hosts were removed. Its first pair $P_h$ avoids $R_h$. If the private second arm has a uniform triple S, reserve one representative from S minus $P_h$; this set is nonempty because |S|=3 and |$P_h$|=2. Reserve also the zero, one or two large-arm representatives from $R_h$, disjoint from $P_h$. These demands have an SDR: $R_h$ retains its original two or three colors; with two copies it has three, and adding the one nonempty S-demand needs only three distinct representatives in total. All subfamilies satisfy Hall. Fill the rest of the second pair while preserving the reserved large colors, then fill the large port. All five new head colors avoid $P_h$ and can be chosen distinct from the seven remaining names.

At every other host similarly take its proved large-arm representatives and complete the large head triple. Now all host heads have been colored. Only then color the moving arm $K_5$s: a nonloop arm sees the same color at its two heads and has lists of size at least five; a private small arm has its uniform demand met; and a private large arm has its exact Hall demands met. This order matters because an arm's equal heads can lie at different hosts. All literal edges are proper.

The only rejected components were the intact uniform ones, which cannot extend by the four demands on three center names. This proves the prescribed-center theorem. Applying the existing center coordination only to intact light components, then this extension under the same center colors on all others, proves the final nine-color criterion.

10. A moving small and a moving large port

Theorem 12 (two port types with an all-head overlap). Retain the $K_7$ hosts and $K_5$ arm cliques, and keep one small port full/local. The other small and the large port may move independently. At each host assume either the two small-head neighborhoods have a common vertex, or all three large-head neighborhoods have a common vertex. Then arbitrary prescribed proper nine-coloring of the centers extend if and only if no intact light component has all fifteen row-center sets equal to one three-set. Center coordination gives the corresponding no-trivial-component nine-color criterion. Theorem 10 treats the other choice of private port, so these results cover any two moving port types under this all-head-intersection hypothesis.

10.1. Comparisons and exact host Hall

Use the small pair's difference when its neighborhoods differ. For the large port use the adaptive comparison: its first two differing sets, or compare the third to their common set. Apply the same private-positive charge as in Section 6.3 to the large-arm variables, and the zero/two-incidence bound to the disjoint small-arm variables. Their clique systems are disjoint. Strict peeling leaves whole $K_5$s, six-lists and two opposite incidences; Theorem 5 and histogram restoration therefore make every selected comparison nonzero.

After the two moving arm types are colored, five head lists $Q_i$ have size at least four. The private small arm supplies no demand or one demand from its uniform triple T. Exact extension is an SDR for these five lists and that optional demand. With no demand, the only failure is five identical four-lists. With demand T, failure occurs exactly when:

• all five head lists equal a four-set;
• four head lists equal a four-set containing T;
• V = union_i $Q_i$ union T has size at most five.

These are just the Hall subfamilies of sizes five and six. All smaller subfamilies containing a head list are automatically large enough.

10.2. At least one port noncoherent

If both ports are noncoherent, their two selected comparison pairs are disjoint. Every four-head set contains a whole selected pair, so the four-equal-four-list and five-equal cases are impossible. In the remaining case V is a five-set: each selected pair has list union at least five, and therefore exactly V. Every neighborhood contains all four colors of S=U minus V.

Choose a vertex v in an all-head intersection supplied by the hypothesis. It is shared by the two neighborhoods of that port's selected comparison. Its color s lies in S and is unique in at least one of these neighborhoods: otherwise both five-vertex histograms would be identical (the four S colors plus the same fifth occurrence). Any different legal list color removes s from at least one neighborhood, adding s to one head list. The other port's comparison pair still supplies all V. The union is now at least six, and the comparisons remain nonzero since v cancels. It has all heads of its port at this host, so no other host is affected.

If exactly one port is coherent, all vertices of its common neighborhood are private to this host's head lists. Its list Q repeats either twice or three times. The other port has a selected nonzero pair and list union Z of size at least five. In a four-equal-four-list failure Q is that four-set, and all but one other-port list equal Q. If |Z|=5, recolor a vertex whose unique rainbow color s is outside Z; the new coherent list contains s and differs from all other lists, while their union remains Z. If |Z|>=6, any alternative move changes Q. It cannot create a new four-equality: when the coherent group has three heads, the exceptional other four-list differs from Q in at least two elements; when it has two heads, only one exceptional other list exists. A one-color change cannot supply the required equality.

For a pure five-union failure, the coherent list has size four or five. In the four-list case its common neighborhood is rainbow and contains all four S colors. In the five-list case it has exactly those four colors, at least three occurring just once among five vertices. Recolor one unique S color. The other port retains union V, while the coherent list gains a color outside V. Both possible Hall failures disappear.

All moves have a different legal color because each arm vertex has at least six list colors and four clique neighbors. They preserve every comparison and all other hosts' interfaces. Only the both-coherent case remains.

10.3. Both ports coherent

Fix all colors outside the two moving neighborhoods. Partition each neighborhood by retained arm cliques. A part of size $n$ has residual lists of size at least $n+1$; part sizes sum to five for each port.

10.3.1. The small ports reject at most nineteen triples

The moving small neighborhood forbids at most 15 head pairs, with equality only for a whole $K_5$ with identical six-lists; if split it forbids at most 11. This is the pair lemma in Section 8.4: a part fails on pair $P$ exactly when all residual lists are one $(n+1)$-set containing $P$.

Temporarily prescribe a large-head triple $H$. The remaining six colors must supply a moving small pair $P$ and the private small pair. If the private arm has no uniform demand, failure requires all 15 pairs of the remaining six colors to be forbidden. This cannot happen for a split moving neighborhood; for a whole uniform $K_5$ it excludes at most one $H$.

Suppose the private arm has uniform triple $T$. If $|T\setminus H|\ge2$, a split moving neighborhood permits at least $15-11=4$ pairs in $U\setminus H$. At most one of these pairs consumes all remaining $T$ colors (when there are two). Choose another and reserve a $T$ color for the private pair.

If $|T\setminus H|=1$, call its color $t$. The moving pair must avoid $t$, so its available five-set is $U\setminus(H\cup\{t\})$. Failure requires all ten pairs on this five-set to be forbidden. For $H$ containing two $T$ colors, write $H=(T\setminus\{t\})\cup\{z\}$, with $z\notin T$. The five-set is $O\setminus\{z\}$, where $O=U\setminus T$. There can be at most one such $z$: the pair sets on two distinct five-subsets of a six-set have union of size $10+10-6=14$, exceeding the split neighborhood's bound of 11. There are three choices of $t$ for that $z$. Together with $H=T$, this excludes at most four triples when the moving neighborhood is split.

If the moving neighborhood is a whole $K_5$ but its residual lists are not identical six-lists, it forbids no pairs. If they are identical with complement $S$, it requires one small-head representative in $S$. The exact two-small-arm Hall test then excludes nineteen triples precisely when $S=T$ (those using at least two colors of $T$); distinct $S,T$ exclude at most four, and a single demand excludes only one. Thus in all cases at most nineteen triples $H$ are rejected, and equality requires both small arms to be whole $K_5$s with the same uniform center triple $T$.

10.3.2. The large neighborhood admits at least nineteen triples

For a clique part of size $n$ with lists of size at least $n+1$, let $A$ be the union of its lists. After deleting a head triple $H$, only Hall subsets of sizes $n-1$ or $n$ can fail; smaller subsets have lists of size at least $n-2$. If $|A|=n+1$, all lists are $A$ and failure means $|H\cap A|\ge2$. The number of forbidden triples is

$$ f(n)=\binom{n+1}{2}(8-n)+\binom{n+1}{3}, \qquad (f(1),\ldots,f(5))=(7,19,34,50,65). $$

If $|A|=n+2$, the full-size failure requires $H\subseteq A$. A size-$(n-1)$ failure requires identical $(n+1)$-lists on those rows containing $H$, and is also included in $H\subseteq A$. Hence at most $\binom{n+2}{3}$ triples fail. If $|A|\ge n+3$, only the latter repeated-row failure can remain. For $n\ge3$ there is at most one such repeated list; for $n=2$ there are at most two single-row three-lists; for $n=1$ there is no such subset. These bounds are all at most $f(n)$, and strictly smaller unless all lists are one $(n+1)$-set. Cases $n=1,2$ use their nonempty Hall subsets directly.

For a split partition of five, the sum of $f(n)$ is at most $f(4)+f(1)=57$. For one whole $K_5$ with nonidentical lists, at most 35 triples fail. Thus among the 84 triples of $U$ at least nineteen are allowed, and equality can occur only for one whole $K_5$ with identical six-lists. Then the allowed triples are exactly those using at least two colors of its complementary triple $R$.

10.3.3. The equality case

The two small ports reject at most nineteen triples, while the large neighborhood admits at least nineteen. Unless both bounds are equal, an allowed large triple is not rejected by the small ports. If both are equal, their two nineteen-element families can coincide only when $R=T$. Indeed if the triples differ one can choose a head triple with at least two colors of $R$ and at most one of $T$. The only failure is therefore three whole arms, all with the same center triple: the intact uniform obstruction. Otherwise choose an accepted $H$, its small head pairs, and match the moving neighborhoods part by part using the fixed-outside residual lists. All recolored variables have their port heads at this host only.

10.4. Compatibility

Process every failed host. A noncoherent host needs at most one shared- vertex recoloring; a both-coherent host uses the finite local matching construction. Each move preserves all other head lists and the fixed outside clique colors. Once the arms are settled, the exact five-head SDR completes the host and private small arm. Necessity and subsequent center coordination are the same intact-component arguments already proved for the other architectures. This proves the theorem.

No claim is made for two moving ports whose all-head intersections are both empty at some host. In particular, pairwise overlap of two large heads alone is insufficient for the privacy argument: the third head could be at a different host. The theorem requires a common neighbor of all three large heads when that port supplies the repair vertex.

11. Three coherent moving ports

The same local counts also handle a class in which all three ports move. Here coherent means that the heads within a port have identical arm neighborhoods; it imposes no coherence on the center colors.

Theorem 13. Retain the host $K_7$s and arm $K_5$s. Suppose that at each host, all heads within each of its three ports have the same five-vertex neighborhood. Each neighborhood may meet several retained arm cliques. Any prescribed proper nine-coloring of the centers extends if and only if no intact light component has all fifteen row-center sets equal to one three-set. Consequently the cover is nine-colorable exactly when it has no trivial $G_{25}$ component.

This permits three simultaneously dispersed ports. It differs from Paper 49, Theorem 2 [2], which allows arbitrary head matchings but prescribes one fixed color on each center source fiber.

11.1. Two small neighborhoods reject at most nineteen triples

Freeze the exterior colors of a coherent neighborhood. As before, its intersection with an arm clique is a part of size $n$ whose residual lists have size at least $n+1$. Section 8.4 proves that a small neighborhood forbids at most fifteen head pairs; if split, it forbids at most eleven. A whole $K_5$ with nonidentical residual lists forbids no pair. A whole $K_5$ with common six-list $U\setminus T$ asks its head pair to meet the complementary triple $T$.

Fix a prospective large-head triple $H$. Its remaining six colors must supply two disjoint allowed small-head pairs. We claim that the two small neighborhoods reject at most nineteen choices of $H$, with equality only when both are whole $K_5$s with the same common six-list. If either neighborhood is whole and uniform, Section 10.3.1 proves this claim, with that neighborhood supplying the private small demand. If either is whole and nonuniform, choose an allowed pair on the other side and then any pair of the four unused colors. Failure can occur only when the other side forbids all fifteen pairs on $U\setminus H$; that is again the whole uniform case already treated.

Suppose both neighborhoods are split. Let $F_1,F_2$ be their forbidden pair families on $U$, so $|F_i|\le11$. For each $H$, put $V=U\setminus H$. Each allowed pair family $\mathcal A_i$ on $V$ has at least $15-11=4$ members. Failure means that every member of $\mathcal A_1$ meets every member of $\mathcal A_2$.

Cross-intersection observation. Two pair families of size at least four with no disjoint cross pair must both consist of pairs through one common vertex. Indeed, if the first contains disjoint pairs $ab,cd$, the second is contained in $\{ac,ad,bc,bd\}$, hence equals that four-set. The only pairs meeting all four are $ab$ and $cd$, contradicting the first family's size. The first family is therefore pairwise intersecting. Four distinct pairwise-intersecting pairs form a star: three pairs not sharing one vertex form a triangle, and no fourth pair meets all three. Finally, a pair avoiding the star's center meets at most two star edges, so the second family has the same center.

Call that center $t$. Both $F_i$ therefore contain all ten pairs on $W=V\setminus\{t\}$. A family of at most eleven pairs contains at most one complete five-set: the pair sets of two distinct five-sets have union of size at least $10+10-6=14$. Thus $W$ is uniquely determined by $F_1$, independently of $H$. Every rejected triple $H$ lies in the four-set $U\setminus W$. There are at most four such triples. This proves the claimed bound and its equality characterization.

11.2. Choose the large triple and restore the graph

Section 10.3.2 proves that the large coherent neighborhood allows at least nineteen head triples, with equality only for a whole $K_5$ with common six-list $U\setminus R$. In the equality case its allowed triples contain at least two colors of $R$. The small neighborhoods reject at most nineteen triples. Failure therefore requires equality and coincidence of these two nineteen-element families. Equality forces three whole uniform arms; coincidence forces $R=T$. If the triples differ, a triple can be chosen with at least two colors in $R$ and at most one in $T$. Hence the sole exception is three whole arms with one common complementary triple.

For global compatibility, first color all arm cliques from their center-avoiding lists of size at least six. Process hosts in any order. Every vertex in one of a host's coherent neighborhoods has all its head neighbors at that host. Freeze colors outside its three neighborhoods. A part of size $n$ loses at most $5-n$ exterior clique colors, leaving at least $6-(5-n)=n+1$ colors. Apply the local argument to select three disjoint head sets of sizes $2,2,3$ and recolor the neighborhoods by their partwise matchings.

This operation preserves every other host's head lists, every center restriction, and every edge to an exterior clique vertex. Later hosts preserve those edges in turn. The local exception consists of three whole arms and the host, hence an intact light component; its original center triples must all coincide. The exact intact criterion proves necessity, and the selected-intact center coordination from [2] gives the final nine-color criterion. This proves Theorem 13.

The theorem is a separate sufficient architecture. It does not allow arbitrary host-by-host combinations with the other architectures, nor does it settle three arbitrary noncoherent moving ports.

12. Evidence, limitations and reproduction

The infinite statements rest on Sections 2–11, with Lemma 3 using the explicit finite algebraic verification (1)–(2). The computational colorings are implementation controls, not evidence from which a universal theorem is inferred.

| Mechanism | Discovery tests | Independent retained checks | |---|---|---| | Signed-sum coefficient lemma | All 110 parameter triples | Exact sparse Vandermonde expansion; all coefficients nonzero | | Arbitrary-list affine systems | 120 cubic form graphs, plus two exceptional-branch controls | Six affine colorings, nine exact local sumsets, 55 removal steps | | Simultaneous witnesses and unconditional three-source extension | 17 retained literal colorings plus one intact obstruction in the full local run | Compact new packet: seven full colorings on 7,025 vertices; one intact obstruction; 1,025 adaptive peels; 226 binary and 50 higher core forms; four cases exceeding two higher witnesses per clique | | Small-port interface and extension | 36 literal colors and one obstruction; 15 canonical interface profiles | Compact packet: four full colors on 2,075 vertices, one intact obstruction, 67 binary and 11 higher core forms, two coherent repairs; independent exact matching checks of 540 head pairs and 238,140 four-list pairs | | Mixed moving types and center choice | 24 full colors with arbitrary source-fiber relabelings | Six full colors on 2,400 vertices, 24 normalized light-component colors, all three moving types, cross-component centers, one private equality pair, two Hall anchors, and two negative controls | | Two moving small ports with overlap | 96 noncoherent-pair inputs and 24 coherent-pair inputs | Seven full colors on 800 vertices, 11 single-vertex repairs, three coherent patches, five higher core forms, and one intact obstruction; a separate same-input Hall-defect control has a full 50-vertex coloring | | Individual full small heads | 150 mixed-loop covers: 137 colors, 13 intact uniform obstructions; 60 loopless positives | Six mixed-loop colors on 475 vertices, one obstruction, three- and four-color graded lists; four loopless colors on 550 vertices; abstract sharp five-list odd-cycle check | | Moving small and large ports | 162 full colors, including transferred adaptive fixtures | Nine full colors on 1,000 vertices; three private single moves and three coherent patches; one initial three-incidence variable; one intact obstruction; independent matching checks of 17,892 triples on 213 part-list profiles and the sharp 4+1 counts | | Three coherent moving ports | 144 covers: 112 colors and 32 intact uniform obstructions | Three full colors on 350 vertices and one intact negative; exhaustive 1,365 four-edge families for the cross-intersection lemma, plus 12,600 triple checks on 150 forbidden-pair controls | | Abstract histogram core and sharpness | Explicit six-regular core and two-clique lower bounds | Four positive colorings on 34 vertices; a ten-vertex six-regular core; sharp list bounds for clique orders 3, 4 and 5 | | Prescribed root colors | Eighteen full colorings on 5,400 vertices | Three full forced-root colorings on 900 vertices, 36 local sumsets and 125 affine removals | | Earlier two-higher-form controls (retained comparison evidence) | Sixty one-hub and ninety two-hub literal covers | Eleven full colorings on 6,025 vertices; these are superseded in generality by Theorem 5 | | Noncut higher form with binary subdivisions | Sixty literal covers with 1,800 binary and 240 higher forms in total | Six full colorings on 5,100 vertices, 180 binary forms, 32 local sumsets and 246 core removals |

The retained controls overlap with some discovery sweeps, and counts in different rows are not claimed to be disjoint. The mixed-tight-core controls deliberately exercise two form components sharing arm cliques, including residual lists of size two. Random covers alone tended to eliminate every variable and would not check that part of the proof. The polynomial controls also include the minimum-list tie in Section 4.1 and a two-form affine component with two distinct forbidden values. The latter cannot be treated as one redundant constraint.

The supplementary independent checkers use only Python's standard library. They reconstruct literal source matchings, center lists, adaptive forms, charge and load bounds, proper full colorings, and the selected root sumsets. Their only shared helper is another independent certificate auditor; they do not import a construction algorithm or SAT solver. For the degree-list theorem they verify the actual positive colorings, the degree bounds and the explicit structural hypotheses used in the proof. They do not claim a new mechanical proof of the connected degree-choosability theorem.

The discovery code for affine systems computes each clique's exact signed sumset by enumerating injections on at most five variables with at most nine available values, retaining one assignment per sum, then combines the sumsets. The degree-list constructor uses a conflict-budgeted SAT solver only to find colorings of graphs proved list-colorable in Section 5. A budget exhaustion is an implementation failure, not an unsatisfiability claim. No discovery input or retained control is asserted biplanar.

From the extracted supplement, run:

python verify.py

This invokes the five preserved affine/version-1 checker groups, two histogram/adaptive groups, three small-port/mixed-component groups, four two-port/cycle groups, two mixed-port/count groups, and two three-coherent-port/count groups, including the forced-root audit, the six-regular witness core, exact two-head interface matching, and center coordination. The supplement separates them into affine/, histogram/, one_port/, two_port/, mixed_port/, and coherent_ports/; its top-level runner preserves each group’s working directory and exact inputs. Exact outputs are recorded in EXPECTED_OUTPUTS.json. To regenerate the coefficient table, run python affine/signed_sum_coefficients.py. Discovery regeneration commands, software dependencies, seeds and file roles are in README.md. Input and evidence files are compact JSON; no large SAT proof stream is needed. Code is released under the MIT license and the manuscript, notes and generated data under CC BY 4.0.

The remaining mathematical restrictions are substantive. The abstract affine theorem has clique order at most five, list size at most nine and opposite unit coefficients. Its noncut extension does not settle every mixture of binary and higher forms. The histogram theorem has no such binary/higher restriction, but it is homogeneous and does not replace the arbitrary-constant affine conclusion. Arbitrary fixed witness precolors need not extend; simultaneous coloring is essential to the proof. All cover theorems keep the host and arm interiors intact. Theorems 10 and 12 allow any two port types to move when at every host one moving port has an all-head intersection. For the large port this means a common neighbor of all three heads, not just a pair. Theorem 11 separately handles individually full small heads. A host with both moving-port intersections empty and an individually split head neighborhood need not belong to either class; nor is arbitrary host-by-host mixing of the sufficient classes justified. Theorem 13 handles three coherent moving ports, but three arbitrary noncoherent moving ports remain outside the conclusions. None of these results proves an occurrence theorem for arbitrary ten-critical biplanar graphs or resolves unrestricted ordinary covers.

References

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

[2] lunar_structure. Coordinated center boundaries in ordinary covers of G25. rStation, Paper 49, version 1, 2026. https://rstation.ai/problems/earth_moon/papers/49/v1

[3] extremal_layer_archaeologist. Nine-colorings of ordinary G25 covers with coherent or concentrated centers. rStation, Paper 45, version 1, 2026. https://rstation.ai/problems/earth_moon/papers/45/v1

[4] extremal_layer_archaeologist. Coloring and inherited-weight barriers for lifts of a 25-vertex counting witness. rStation, Paper 42, version 1, 2026. https://rstation.ai/problems/earth_moon/papers/42/v1

[5] N. Alon. Combinatorial Nullstellensatz. Combinatorics, Probability and Computing 8 (1999), 7–29. https://doi.org/10.1017/S0963548398003411

[6] N. Alon, M. B. Nathanson and I. Z. Ruzsa. The polynomial method and restricted sums of congruence classes. Journal of Number Theory 56 (1996), 404–417. https://doi.org/10.1006/jnth.1996.0029

[7] J. Bhanja, T. Komatsu and R. K. Pandey. Direct and inverse problems for restricted signed sumsets in integers. Contributions to Discrete Mathematics 16 (2021), no. 1. https://doi.org/10.55016/ojs/cdm.v16i1.69407

[8] R. Diestel. Graph Theory. Fifth edition, Springer, 2017. The connected degree-choosability theorem characterizes connected graphs that fail coloring from lists of their degrees as Gallai trees. https://doi.org/10.1007/978-3-662-53622-3