1. Problem, Context, and Main Contributions

Let $\mathcal{R}(5,5,N)$ denote the set of simple graphs on $N$ vertices with clique number $\omega(G) \leq 4$ and independence number $\alpha(G) \leq 4$ (where edges are called red and non-edges are called blue). Exoo [1] constructed $(5,5,42)$-graphs establishing $R(5,5) \geq 43$, McKay and Radziszowski [2] extended the known $(5,5,42)$ catalogue to $656$ graphs ($328$ complementary pairs, all with $|\operatorname{Aut}(G)| \in \{1,2\}$) and proved $R(5,5) \leq 49$, and Angeltveit and McKay [3, 4] established $R(5,5) \leq 46$. In our companion papers [5, 6] (incorporating the $43$-vertex circulant exclusion recorded by Radziszowski [7], citing Harborth and Krause [8]), we excluded all prime-order automorphisms $p \geq 7$ across $N \in \{42,43,44,45\}$ and excluded $p = 5$ across $N \in \{42,43,44\}$, proving that every graph $G \in \bigcup_{N=42}^{44} \mathcal{R}(5,5,N)$ satisfies $|\operatorname{Aut}(G)| = 2^a 3^b$ and has a solvable automorphism group [9]. Alongside recent rStation analyses of hypothetical $(5,5,45)$ graphs [10, 11], this focuses the nontrivial symmetry frontier at $N \in \{42,43\}$ on automorphisms of orders $2$ and $3$.

Suppose $G \in \mathcal{R}(5,5,N)$ ($N \in \{42,43\}$) admits an order-$3$ automorphism $\sigma \in \operatorname{Aut}(G)$:

• At Order $43$ ($43 = 1 + n_A + n_B$, Apex-Neighbourhood Gluing): If $\sigma$ fixes an apex vertex $v_\infty \in V(G)$ and acts semi-regularly on $V(G) \setminus \{v_\infty\}$, then $\sigma$ preserves the red neighbourhood $A = G[N_R(v_\infty)]$ ($n_A = 3 r_A$ vertices partitioned into $r_A$ regular $C_3$-orbits $O_0^A, \dots, O_{r_A-1}^A$) and the blue neighbourhood $B = G[N_B(v_\infty)]$ ($n_B = 3 r_B$ vertices partitioned into $r_B$ regular $C_3$-orbits $O_0^B, \dots, O_{r_B-1}^B$). Because $v_\infty$ is red-adjacent to all of $A$ and blue-nonadjacent to all of $B$, $A$ must be $(K_4, I_5)$-free ($\omega(A) \leq 3$, $\alpha(A) \leq 4$) and $B$ must be $(K_5, I_4)$-free ($\omega(B) \leq 4$, $\alpha(B) \leq 3$) [12].
• At Order $42$ ($42 = n_A + n_B$, Two-Block Gluing): Deleting the apex $v_\infty$ leaves $V(G) = V(A) \sqcup V(B)$ on $42 = n_A + n_B$ vertices, where $A$ is a fixed $\sigma$-invariant $(K_4, I_5)$-free marked source on $r_A$ regular $C_3$-orbits and $B$ is an unknown $\sigma$-invariant $(K_5, I_5)$-free partner graph on $r_B$ regular $C_3$-orbits ($\omega(B) \leq 4$, $\alpha(B) \leq 4$).

In both regimes, the cross-adjacency matrix $M \in \{0,1\}^{V(A) \times V(B)}$ decomposes into $3 \times 3$ circulant blocks $M_{p,q}$ with row and column sums $w_{p,q} \in \{0,1,2,3\}$. Why focus on the two specific marked sources $\mathrm{H24\_306763}$ and $A_{21} = \operatorname{Cay}(\mathbb{Z}_{21}, \pm\{2,3,5,6\})$? Across the complete $(4,5,24)$ catalogue r45_24.g6 ($352{,}366$ graphs), there are $70$ graphs ($73$ marked regular-$C_3$ actions on $8$ regular triples) admitting a fixed-point-free order-$3$ automorphism: $30$ are pure-$K_3$-orbit actions ($8$ red $K_3$-orbits, $0$ blue $I_3$-orbits), $43$ are mixed $K_3/I_3$-orbit actions, and $0$ are pure-$I_3$-orbit actions (an observed property of the $24$-vertex catalogue). Thus, studying $\mathrm{H24\_306763}$ ($n_A = 24, n_B = 18$) and $A_{21}$ ($n_A = 21, n_B = 21$) isolates the two opposite pure-orbit regimes of $C_3$-equivariant gluing:

• Dense Pure-$K_3$ Regime ($\mathrm{H24\_306763}$, $r_A = 8, r_B = 6, t(A) = 164$): Among the $30$ pure-$K_3$ actions at $n_A = 24$, $\mathrm{H24\_306763}$ ($129$ edges, $164$ red triangles) is a dense non-circulant benchmark where every row is a red triangle ($O_p^A \cong K_3$). Here the high triangle count $t(A) = 164$ makes marginal triangle counting slack ($\lfloor 164\,\alpha(B)/3 \rfloor = 164$ at Order $43$), but the pure-$K_3$ row structure activates the occupied-row full-join restriction $v_3(w_{\cdot,q}) \geq 1 \implies \operatorname{adm}_{K_3}(w_{\cdot,q}) = 0$ (Corollary 2.2(1)) and immediate $11$- and $12$-clause unit-propagation refutations whenever a row contains two weight-$3$ blocks.
• Balanced Pure-$I_3$ Regime ($A_{21}$, $r_A = 7, r_B = 7, t(A_{21}) = 63$): Conversely, in the balanced $21 + 21$ split, $A_{21} = \operatorname{Cay}(\mathbb{Z}_{21}, \pm\{2,3,5,6\})$ ($84$ edges, $t(A_{21}) = 63$ red triangles, $147$ independent $4$-sets) is the minimum-density vertex-transitive $(K_4, I_5)$-free circulant with $7$ regular $I_3$-orbits ($O_p^A \cong I_3$). Here every row is a blue independent triple, activating the dual zero-join restriction $v_0(w_{\cdot,q}) \geq 1 \implies \operatorname{adm}_{I_3}(w_{\cdot,q}) = 0$ (Corollary 2.2(2)), while the low triangle count $t(A_{21}) = 63$ makes the triangle double count $\sum_{q=0}^6 t_A(S_q) \leq 21\,\alpha(B)$ (Lemma 2.3) tightly constraining ($63$ at Order $43$, $84$ at Order $42$).

In this paper, we establish complete and partial exclusions for these two extremal marked sources and isolate the transferable single-column cone, polarity, and triangle conservation arguments that govern them:

1. Theorem 3.1 and Theorem 3.2 (Dual-Certified Exclusions of Marked $\mathrm{H24\_306763}$ at Orders $43$ and $42$): For the marked $(K_4, I_5)$-free graph $\mathrm{H24\_306763}$ on $n_A = 24$ vertices ($8$ regular $K_3$-orbits, $129$ edges, $t(A) = 164$ red triangles, explicitly related to its raw graph6 catalogue entry by the vertex bijection $\pi$ in Section 3.1) glued against an unknown $18$-vertex partner $B_{18}$ on $6$ regular $C_3$-orbits:

   • Order $43$ ($84 / 84$ unsplit Row-$0$ cubes): Normalizing Row $0$ ($O_0^A$) under the partner wreath group $W_6 = S_6 \ltimes C_3^6$ (order $524{,}880$) partitions all $2^{18} = 262{,}144$ Row-$0$ patterns into $\binom{6+4-1}{6} = 84$ non-decreasing Row-$0$ weight multisets $w_0 \in \{0,1,2,3\}^6$. All $84$ unsplit cubes are certified UNSAT both locally (PicoSAT 965 + StandaloneTraceCheckVerifier) and by independent external validation (u/teichmuller_lift, CaDiCaL --lrat + lrat-check [13]).
   • Order $42$ ($644 / 644$ canonical cases across an unconditional tautology cover): Deleting $v_\infty$ ($42 = 24 + 18$ vertices), we partition the partner space unconditionally according to whether $B_{18}$ contains an orbit-aligned type-$(3,1)$ blue $I_4$ witness (three vertices forming a blue $I_3$-orbit $O_{q_1}^B$ together with one vertex in another regular orbit $O_{q_2}^B$ completely blue-joined to $O_{q_1}^B$): Family A ($560$ canonical Row-$0$ cases under the stabilizer $H_{(3,1)} = (\{0\} \times \{1\} \times S_{\{2,3,4,5\}}) \ltimes C_3^6$ of order $17{,}496$ of the four-unit witness constraint) and Family B ($84$ canonical Row-$0$ cubes with all $30$ orbit-level type-$(3,1)$ $I_4$ clauses adjoined, invariant under $W_6$). All $644$ cases were certified UNSAT locally ($631$ unsplit cases $+ 13$ cases split into $132$ Row-$1$ truth-table leaves $= 763$ original jobs via PicoSAT 965 + StandaloneTraceCheckVerifier) and independently externally validated by u/teichmuller_lift ($759$ direct checks $+ 32$ sign-cube leaves on variables $28, 29, 30$ replacing the $4$ capped Family A parents id 237, 366, 376, 520 via CaDiCaL --lrat + lrat-check).

2. Theorem 4.1 (Dual-Certified Complete Order-$43$ Exclusion of Marked $A_{21}$) and Proposition 4.3 (Locally Proof-Checked Conditional Order-$42$ Family P Exclusion of Marked $A_{21}$): For the vertex-transitive $(K_4, I_5)$-free circulant $A_{21} = \operatorname{Cay}(\mathbb{Z}_{21}, \pm\{2,3,5,6\})$ on $n_A = 21$ vertices ($7$ regular $I_3$-orbits, $84$ edges, $t(A_{21}) = 63$ red triangles, $147$ independent $4$-sets) glued against an unknown $21$-vertex partner $B_{21}$ on $7$ regular $C_3$-orbits:

   • Order $43$ ($392$ local leaves / $399$ external terminal leaves across $105$ canonical Row-$0$ cubes #0..#104 — Dual-Certified): We prove complete exclusion via three components, certified both locally (PicoSAT 965 + StandaloneTraceCheckVerifier) and by independent external validation (u/teichmuller_lift, CaDiCaL 1.9.5 --lrat + lrat-check): (I) Family Z ($84 / 84$ cubes #0..#83, $168$ local leaves) eliminates every completion containing a weight-$0$ block ($w_{p,q} = 0$), restricting any putative completion to strictly positive weights $\mathcal{M}_+ = \{1,2,3\}^{7 \times 7}$; (II) a Positive-Weight Conservation Bound combining the triangle double count $3 \sum_{q=0}^6 t_A(S_q) \leq \alpha(B_{21})\,t(A_{21})$ ($\sum_{q=0}^6 t_A(S_q) \leq 63$ at Order $43$) with the computed $2{,}186$-profile positive cone table of $A_{21}$ proves that any positive completion satisfies $U(M) = \sum_{p,q} \mathbf{1}_{w_{p,q}=1} \geq 10$ and $U(M) - W_3(M) \geq 6$, forcing some row to have $\geq 2$ ones; and (III) the 21-Row Maximum-Ones Cover ($21 / 21$ cubes #84..#104, $224$ leaves) refutes all $21$ canonical positive-weight Row-$0$ multisets with $n_{w_0}(1) \geq 2$ without any $W_3(M) = 0$ restriction.
   • Order $42$ ($8 / 8$ canonical Family P Row-$0$ cubes: $56$ locally verified leaves across $7$ cubes #84, #85, #87, #90, #94, #99, #105 + analytical exclusion of #112_2222222 — Locally Proof-Checked Only): Under the conditional hypothesis $M \in \{1,2\}^{7 \times 7}$ (Family P), we exclude all $8$ canonical Row-$0$ multisets at Order $42$ via local PicoSAT 965 + StandaloneTraceCheckVerifier refutations. Outside Family P, the full Order-$42$ question for $A_{21}$ remains open.

Positive-profile triangle envelope of A21 and 7-column conservation relaxation feasible region at Orders 43 and 42

Figure 1. (a) Lower red-cone triangle envelope $\underline{t}_+(v_1, v_3)$ across the $2{,}186$ locally admissible positive column weight profiles $w \in \{1,2,3\}^7$ of $A_{21}$ as a function of $v_1(w) = n_w(1) \in \{0,\dots,6\}$ for $v_3(w) = n_w(3) \in \{0,1,2,3\}$, together with the marginal envelope $\underline{t}_+(v_1) = (14,10,7,6,7,8,9)$ (note the non-monotonicity in $v_3$ at $v_1 = 4$, where $\underline{t}_+(4,0) = 8 > \underline{t}_+(4,2) = 7$; profile 1111111 at $v_1 = 7$ is inadmissible). (b) Exact feasible region of the $7$-column triangle-budget relaxation $\sum_{q=0}^6 \underline{t}_+(v_{1,q}, v_{3,q}) \leq 21\,\alpha(B_{21})$ in the $(U(M), W_3(M))$ plane at Order $43$ ($\leq 63$, blue circles: $U(M) \geq 10$ and $U(M) - W_3(M) \geq 6$, forcing $\max_p n_{w_p}(1) \geq \lceil 10/7 \rceil = 2$) and at Order $42$ ($\leq 84$, orange squares: $U(M) \geq 4$ and $U(M) - W_3(M) \geq 0$). Plotted points represent 7-column budget-relaxation feasibility over locally admissible column profiles, not demonstrated $(5,5)$-free graph completions (Theorem 4.1 refutes all Order-$43$ completions and Proposition 4.3 refutes all Order-$42$ $W_3(M)=0$ completions). Exact values appear in Table 1.

---

2. Related Work, Encoding, and General vs. Source-Specific Counting Principles

2.1 Methodological Precedents and Verification Attribution

Neighbourhood gluing, subgraph double-counting identities, wreath-group coordinate normalization, and cube-and-conquer SAT refutations follow the established methodology of McKay and Radziszowski [2, 12], Angeltveit and McKay [3, 4], and Heule, Kullmann, and Marek [13]. Throughout this paper, we maintain an explicit distinction between:

• Independently Externally Validated (Dual-Certified) Results: Theorems 3.1 and 3.2 on $\mathrm{H24\_306763}$ at Orders $43$ and $42$, and Theorem 4.1 on $A_{21}$ at Order $43$, each of which was solved and verified locally using PicoSAT 965 (picosat_write_extended_trace) + StandaloneTraceCheckVerifier and independently reconstructed from first principles and verified with CaDiCaL --lrat + lrat-check by u/teichmuller_lift (r/ramsey_5_5/post/6, Comments fWvd3d3LP0AUrUzA, 1v_JBt6OH_SIY0Pe, and V7OQlV_mh49Uivo5, archived in supplement/external_validation/).
• Locally Proof-Checked Results: Proposition 4.3 on $A_{21}$ in the conditional Order-$42$ Family P regime ($M \in \{1,2\}^{7 \times 7}$, $56$ leaves across $7$ cubes #84, #85, #87, #90, #94, #99, #105 + analytic exclusion of #112_2222222), which lay outside u/teichmuller_lift's Priority Order-$43$ validation scope and was verified locally using PicoSAT 965 + StandaloneTraceCheckVerifier (supplement/verify_dimacs_picosat_tracecheck.cpp) together with the internal formula, symmetry, cone-table, partition, and SHA-256 checks in generate_a21_order43_and_famP42_handoff.cpp.

Acknowledgments. We thank u/teichmuller_lift for his independent clean-room reconstructions and CaDiCaL --lrat + lrat-check external validations of the Order-$43$ and Order-$42$ exclusions of $\mathrm{H24\_306763}$ and the complete Order-$43$ exclusion of $A_{21}$, and u/vesper_ash for research supervision and technical review of the conservation argument, stabilizer reductions, and verification audit trail.

2.2 Equivariant Propositional Encoding (base42 and base43)

Label the vertices of each regular $A$-orbit $O_p^A$ as $(p, x)$ ($p \in \{0,\dots,r_A-1\},\, x \in \mathbb{Z}_3$) and those of each regular $B$-orbit $O_q^B$ as $(q, y)$ ($q \in \{0,\dots,r_B-1\},\, y \in \mathbb{Z}_3$), with $\sigma(p, x) = (p, x+1 \bmod 3)$ and $\sigma(q, y) = (q, y+1 \bmod 3)$:

1. Cross-edges $M \in \{0,1\}^{V(A) \times V(B)}$: Each $3 \times 3$ block $M_{p,q}$ between $O_p^A$ and $O_q^B$ is a circulant matrix determined by three boolean variables $m(p, q, d) \in \{0,1\}$ ($d \in \{0,1,2\}$), where the cross-edge between $(p, x) \in O_p^A$ and $(q, y) \in O_q^B$ has value $m(p, q, (y - x) \bmod 3)$ ($3 r_A r_B$ cross-edge variables: $144$ for $8 \times 6$ and $147$ for $7 \times 7$). Its block weight is$$ w_{p,q} := m(p,q,0) + m(p,q,1) + m(p,q,2) \in \{0,1,2,3\}. $$Up to cyclic shift of $O_q^B$, each weight $w \in \{0,1,2,3\}$ has a unique canonical bit-pattern $(m(p,q,0), m(p,q,1), m(p,q,2)) = (\mathbf{1}_{d \geq 3-w})_{d=0,1,2}$, namely $(0,0,0)$, $(0,0,1)$, $(0,1,1)$, and $(1,1,1)$.
2. Partner edges on $B$: Each regular orbit $O_q^B$ is either a red triangle ($B[O_q^B] \cong K_3$, $b_{\mathrm{intra}}(q) = 1$) or a blue independent triple ($B[O_q^B] \cong I_3$, $b_{\mathrm{intra}}(q) = 0$) ($r_B$ intra-orbit variables), and each pair of distinct orbits $q < q'$ has a $3 \times 3$ circulant adjacency block parameterized by $b_{\mathrm{inter}}(q, q', d) \in \{0,1\}$ for $d \in \{0,1,2\}$ ($3 \binom{r_B}{2}$ inter-orbit variables). The total number of primary boolean variables is $144 + 45 + 6 = 195$ for $\mathrm{H24\_306763}$ ($8 \times 6$) and $147 + 63 + 7 = 217$ for $A_{21}$ ($7 \times 7$).

For a fixed $(K_4, I_5)$-free source $A$, the glued graph $G$ is $(5,5)$-free if and only if $(B, M)$ satisfies:

• At Order $42$ (base42): Pure-$B$ $K_5$-freeness (set_BK5) and $I_5$-freeness (set_BI5), mixed red $K_5$ avoidance across $K_r \subseteq A$ and $K_{5-r} \subseteq B$ for $r \in \{1,2,3\}$ (set_r14, set_r23, set_r32, since $\omega(A) \leq 3$), and mixed blue $I_5$ avoidance across $I_r \subseteq A$ and $I_{5-r} \subseteq B$ for $r \in \{1,2,3,4\}$ (set_b14, set_b23, set_b32, set_b41, since $\alpha(A) \leq 4$).
• At Order $43$ (base43): Adjoining the apex $v_\infty$ (red to $A$, blue to $B$) adds pure-$B$ $I_4$-freeness (set_BI4, since $B = N_B(v_\infty)$ cannot contain a blue $I_4$), which subsumes set_BI5 and set_b14 (while $A = N_R(v_\infty)$ is already $K_4$-free).

2.3 General Single-Column Cone, Polarity, and Triangle Double-Count Lemmas

Let $A$ be any $\sigma$-invariant $(K_4, I_5)$-free graph on $r_A$ regular $C_3$-orbits $O_0^A, \dots, O_{r_A-1}^A$, glued to a $\sigma$-invariant partner $B$ on $r_B$ regular $C_3$-orbits $O_0^B, \dots, O_{r_B-1}^B$. Fix a partner column $O_q^B$ and let $b = (q, 0) \in O_q^B$. Let

$$ S = N_R(b) \cap V(A), \qquad T = V(A) \setminus S = N_B(b) \cap V(A) $$

be the red and blue cones of $b$ in $A$. By $\sigma$-equivariance, the three vertices $(q,0), (q,1), (q,2)$ of $O_q^B$ have red cones $S, \sigma(S), \sigma^2(S)$ and blue cones $T, \sigma(T), \sigma^2(T)$, and the block weight on row $p$ is $w_{p,q} = |S \cap O_p^A| \in \{0,1,2,3\}$.

Lemma 2.1 (Single-Column Local Admissibility Conditions). In any $(5,5)$-free gluing of $(A, B)$:

1. Single-vertex condition (Mixed $(4,1)$): Because $\omega(A) \leq 3$, $S$ automatically contains no red $K_4$. To avoid a mixed $(4,1)$ blue $I_5 = I_4 \cup \{b\}$, the blue cone $T = V(A) \setminus S$ must be $I_4$-free.
2. Red partner orbit condition (ok_K3, when $B[O_q^B] \cong K_3$):
   • To avoid a mixed $(3,2)$ red $K_5$ formed by a red triangle in $A$ and a red edge $\{(q,0), (q,1)\} \in E(B)$, the pairwise red-cone intersection $S \cap \sigma(S)$ must be $K_3$-free.
   • To avoid a mixed $(2,3)$ red $K_5$ formed by a red edge in $A$ and the red triangle $O_q^B \cong K_3$, the triple red-cone intersection$$ S \cap \sigma(S) \cap \sigma^2(S) = \bigcup_{p : w_{p,q} = 3} O_p^A $$must be $K_2$-free (an independent set in $A$).
3. Blue partner orbit condition (ok_I3, when $B[O_q^B] \cong I_3$):
   • To avoid a mixed $(3,2)$ blue $I_5$ formed by a blue $I_3 \subseteq A$ and a blue non-edge $\{(q,0), (q,1)\}$ in $O_q^B$, the pairwise blue-cone intersection $T \cap \sigma(T)$ must be $I_3$-free.
   • To avoid a mixed $(2,3)$ blue $I_5$ formed by a blue non-edge in $A$ and the blue independent triple $O_q^B \cong I_3$, the triple blue-cone intersection$$ T \cap \sigma(T) \cap \sigma^2(T) = \bigcup_{p : w_{p,q} = 0} O_p^A $$must be $I_2$-free (a red clique in $A$).

A weight profile $w_{\cdot,q} \in \{0,1,2,3\}^{r_A}$ is locally admissible if there exists $S \subseteq V(A)$ with $|S \cap O_p^A| = w_{p,q}$ satisfying (1) and at least one of (2) ($\operatorname{adm}_{K_3}(w_{\cdot,q}) = 1$) or (3) ($\operatorname{adm}_{I_3}(w_{\cdot,q}) = 1$).

Corollary 2.2 (General Full-Join and Zero-Join Orbit Polarity Restrictions). Let $v_k(w_{\cdot,q}) := |\{p : w_{p,q} = k\}|$ for $k \in \{0,1,2,3\}$.

1. Red-orbit restrictions on $w_{p,q} = 3$: By Lemma 2.1(2), if $B[O_q^B] \cong K_3$, then $\bigcup_{p : w_{p,q}=3} O_p^A$ is an independent set of size $3\,v_3(w_{\cdot,q})$ in $A$.
   • Occupied-row restriction: If a specific row $p$ satisfies $O_p^A \cong K_3$ in $A$ and $w_{p,q} = 3$, then $O_p^A \subseteq \bigcup_{p' : w_{p',q}=3} O_{p'}^A$ contains red edges, which is impossible when $B[O_q^B] \cong K_3$. Thus $w_{p,q} = 3$ on a $K_3$-row $p$ forbids a red partner orbit ($\operatorname{adm}_{K_3}(w_{\cdot,q}) = 0$). In particular, if every row of $A$ is a $K_3$-orbit (as in $\mathrm{H24\_306763}$), then $v_3(w_{\cdot,q}) \geq 1 \implies \operatorname{adm}_{K_3}(w_{\cdot,q}) = 0$.
   • Unrestricted two-row restriction: For any $(K_4, I_5)$-free graph $A$, $\alpha(A) \leq 4 < 6$, so two full orbits ($6$ vertices) cannot be independent in $A$. Hence for every $(K_4, I_5)$-free source $A$, $v_3(w_{\cdot,q}) \geq 2 \implies \operatorname{adm}_{K_3}(w_{\cdot,q}) = 0$.
2. Blue-orbit restrictions on $w_{p,q} = 0$: Dually, by Lemma 2.1(3), if $B[O_q^B] \cong I_3$, then $\bigcup_{p : w_{p,q}=0} O_p^A$ is a clique of size $3\,v_0(w_{\cdot,q})$ in $A$.
   • Occupied-row restriction: If a specific row $p$ satisfies $O_p^A \cong I_3$ in $A$ and $w_{p,q} = 0$, then $O_p^A \subseteq \bigcup_{p' : w_{p',q}=0} O_{p'}^A$ contains blue non-edges, which is impossible when $B[O_q^B] \cong I_3$. Thus $w_{p,q} = 0$ on an $I_3$-row $p$ forbids a blue partner orbit ($\operatorname{adm}_{I_3}(w_{\cdot,q}) = 0$). In particular, if every row of $A$ is an $I_3$-orbit (as in $A_{21}$), then $v_0(w_{\cdot,q}) \geq 1 \implies \operatorname{adm}_{I_3}(w_{\cdot,q}) = 0$.
   • Unrestricted two-row restriction: For any $(K_4, I_5)$-free graph $A$, $\omega(A) \leq 3 < 6$, so for every $(K_4, I_5)$-free source $A$, $v_0(w_{\cdot,q}) \geq 2 \implies \operatorname{adm}_{I_3}(w_{\cdot,q}) = 0$.

Lemma 2.3 (Triangle Budget Double Count). Let $A$ be any $\sigma$-invariant $(K_4, I_5)$-free graph with $t(A)$ red triangles, glued to a $\sigma$-invariant partner $B$ on $r_B$ regular $C_3$-orbits $O_0^B, \dots, O_{r_B-1}^B$ with independence number $\alpha(B)$. For each column $q \in \{0, \dots, r_B-1\}$, let $S_q = N_R(q, 0) \cap V(A)$ and let $t_A(S_q)$ denote the number of red triangles of $A$ contained in $S_q$. Then in any $(5,5)$-free completion:

$$ 3 \sum_{q=0}^{r_B-1} t_A(S_q) \leq \alpha(B) \cdot t(A). $$

Proof. For each red triangle $\Delta \subseteq A$, let $C_B(\Delta) := \{b \in V(B) : \Delta \subseteq N_R(b)\}$ be the set of common red neighbours of $\Delta$ in $B$. If $C_B(\Delta)$ contained a red edge $\{b_1, b_2\} \in E(B)$, then $\Delta \cup \{b_1, b_2\}$ would form a mixed $(3,2)$ red $K_5$. Therefore, $C_B(\Delta)$ is an independent set in $B$, so $|C_B(\Delta)| \leq \alpha(B)$. Since the three vertices of $O_q^B$ have $\sigma$-congruent cones $S_q, \sigma(S_q), \sigma^2(S_q)$ in $A$ and $\sigma \in \operatorname{Aut}(A)$, each vertex of $O_q^B$ contains $t_A(S_q)$ triangles of $A$ in its red cone. Double-counting pairs $(\Delta, b) \in \mathcal{T}(A) \times V(B)$ with $\Delta \subseteq N_R(b)$ yields

$$ 3 \sum_{q=0}^{r_B-1} t_A(S_q) = \sum_{b \in V(B)} t_A(N_R(b) \cap V(A)) = \sum_{\Delta \in \mathcal{T}(A)} |C_B(\Delta)| \leq \alpha(B) \cdot t(A). \quad \square $$

When $t(A) = 63$ (as for $A = A_{21}$), dividing by $3$ gives:

$$ \sum_{q=0}^{r_B-1} t_A(S_q) \leq 21\,\alpha(B) = \begin{cases} 63 & \text{at Order } 43 \text{ } (\alpha(B) \leq 3), \\ 84 & \text{at Order } 42 \text{ } (\alpha(B) \leq 4). \end{cases} $$

2.4 Computed Cone Profile Table for $A_{21}$ (a21_admissible_column_wcodes.tsv)

For the specific source $A_{21} = \operatorname{Cay}(\mathbb{Z}_{21}, \pm\{2,3,5,6\})$ ($21$ vertices, $84$ edges, $t(A_{21}) = 63$ triangles, $147$ independent $4$-sets, $7$ regular $I_3$-orbits $O_p^A = \{p, p+7, p+14\}$), converting Lemma 2.3 into a lower bound on the number of weight-$1$ entries $U(M) = \sum_{p,q} \mathbf{1}_{w_{p,q}=1}$ relies on the exhaustive enumeration of all $2^{21} = 2{,}097{,}152$ subsets $S \subseteq V(A_{21})$ under Lemma 2.1 (generate_a21_order43_and_famP42_handoff.cpp, archived in a21_admissible_column_wcodes.tsv and independently reproduced by both the referee and u/teichmuller_lift):

1. Admissible Profile Counts: Out of all $4^7 = 16{,}384$ weight vectors $w \in \{0,1,2,3\}^7$, $2{,}914$ profiles are locally admissible. Out of the $3^7 = 2{,}187$ strictly positive weight vectors $w \in \{1,2,3\}^7$, $2{,}186$ profiles are locally admissible: the unique inadmissible positive profile is 1111111 ($v_1(w) = 7$, for which every complement $T = A_{21} \setminus S$ of size $14$ contains a blue $I_4$). By contrast, $S = V(A_{21})$ with profile 3333333 is locally admissible for a blue partner orbit (adm_flags = 2, min_tA = 63, since $T = \emptyset$). Out of the $2^7 = 128$ pure-$\{1,2\}$ vectors $w \in \{1,2\}^7$, $127$ profiles are admissible (all except 1111111).
2. Table-Verified Polarity Property $\operatorname{adm}_{K_3}(v_1 = 0) = 0$: While $\operatorname{adm}_{K_3}(v_3 \geq 2) = 0$ holds universally by Corollary 2.2(1), the fact that all $128$ positive profiles with $v_1(w) = 0$ ($w \in \{2,3\}^7$) satisfy $\operatorname{adm}_{K_3}(w) = 0$ (adm_flags = 2) is a specific property of $A_{21}$ established by the enumeration.
3. Exact 2D Lower Triangle Table $\underline{t}_+(v_1, v_3)$ and Marginal Envelope $\underline{t}_+(v_1)$: Grouping the $2{,}186$ admissible positive profiles by $(v_1, v_3) = (n_w(1), n_w(3))$ gives the exact 2D minimum table $\underline{t}_+(v_1, v_3)$ and marginal minimum $\underline{t}_+(v_1) = \min_{v_3} \underline{t}_+(v_1, v_3)$ in Table 1.

| $v_1(w)$ | Positive Profiles | $\operatorname{adm}_{K_3}$ Profiles | Marginal $\underline{t}_+(v_1)$ | Exact 2D Minimum $\underline{t}_+(v_1, v_3)$ from a21_admissible_column_wcodes.tsv | |---:|---:|---:|---:|---| | $0$ | $128$ | $0$ | $14$ | $(0,0): 14,\; (0,1): 17,\; (0,2): 22,\; (0,3): 29,\; (0,4): 36,\; (0,5): 45,\; (0,6): 54,\; (0,7): 63$ | | $1$ | $448$ | $35$ | $10$ | $(1,0): 10,\; (1,1): 12,\; (1,2): 16,\; (1,3): 22,\; (1,4): 28,\; (1,5): 36,\; (1,6): 45$ | | $2$ | $672$ | $119$ | $7$ | $(2,0): 7,\; (2,1): 8,\; (2,2): 12,\; (2,3): 16,\; (2,4): 20,\; (2,5): 28$ | | $3$ | $560$ | $175$ | $6$ | $(3,0): 6,\; (3,1): 7,\; (3,2): 8,\; (3,3): 12,\; (3,4): 17$ | | $4$ | $280$ | $140$ | $7$ | $(4,0): 8,\; (4,1): 8,\; (4,2): 7,\; (4,3): 11$ (not monotone in $v_3$) | | $5$ | $84$ | $63$ | $8$ | $(5,0): 8,\; (5,1): 8,\; (5,2): 10$ | | $6$ | $14$ | $14$ | $9$ | $(6,0): 9,\; (6,1): 9$ | | $7$ | $0$ | $0$ | $\infty$ | 1111111 is inadmissible |

Table 1. Exact positive-profile counts, $\operatorname{adm}_{K_3}$ counts, marginal lower triangle envelope $\underline{t}_+(v_1)$, and 2D minimum red-cone triangle table $\underline{t}_+(v_1, v_3)$ across all $2{,}186$ locally admissible positive column profiles of $A_{21}$.

---

3. Dual-Certified Exclusions of Marked $\mathrm{H24\_306763}$ at Orders $43$ and $42$

3.1 Explicit Relabeling Between the Raw graph6 Entry and H24_306763_MARKED_ADJ

Let $G_{\mathrm{raw}}$ be the $24$-vertex $(K_4, I_5)$-free graph ($129$ edges, $164$ red triangles) decoded in standard upper-triangle column-major order from line $306{,}763$ ($0$-indexed) of the $(4,5,24)$ catalogue r45_24.g6:

WtTk?KQOxF@NdpwdP{ESoiFmXdo|MbS^@dhULUTahtQmMTK

In raw graph6 vertex coordinates $v \in \{0,\dots,23\}$, vertices $\{0,1,2\}$ do not form a triangle; rather, the marked order-$3$ automorphism $\sigma_{\mathrm{raw}} \in \operatorname{Aut}(G_{\mathrm{raw}})$ (sA in selected_noncirculant_A24_for_teichmuller.json) is the permutation

$$ \sigma_{\mathrm{raw}} = [2, 5, 3, 0, 1, 4, 10, 11, 6, 7, 8, 9, 16, 21, 19, 20, 23, 13, 15, 22, 18, 17, 14, 12]. $$

To obtain contiguous orbit-phase coordinates $i = 3p + x \in \{0,\dots,23\}$ ($p \in \{0,\dots,7\},\, x \in \{0,1,2\}$) on which the marked action is $\sigma_A(3p + x) = 3p + ((x + 1) \bmod 3)$, extract_k3_8_order3_blocks_from_sg partitions $\{0,\dots,23\}$ by increasing vertex-invariant bucket $(\deg(v), \operatorname{tri}(v))$—namely $(10,17): \{0,1,2,3,4,5\}$, $(11,21): \{12,14,16,19,22,23\}$, and $(11,22): \{6,7,8,9,10,11,13,15,17,18,20,21\}$—and orders the $8$ directed $3$-cycles of $\sigma_{\mathrm{raw}}$ as:

$$ \begin{aligned} O_0^A &= (0, 2, 3), & O_1^A &= (1, 5, 4), & O_2^A &= (12, 16, 23), & O_3^A &= (14, 19, 22), \\ O_4^A &= (6, 10, 8), & O_5^A &= (7, 11, 9), & O_6^A &= (13, 21, 17), & O_7^A &= (15, 20, 18). \end{aligned} $$

This defines the explicit relabeling bijection $\pi : \{0,\dots,23\}_{\mathrm{marked}} \to \{0,\dots,23\}_{\mathrm{raw}}$:

$$ \pi = [0, 2, 3,\; 1, 5, 4,\; 12, 16, 23,\; 14, 19, 22,\; 6, 10, 8,\; 7, 11, 9,\; 13, 21, 17,\; 15, 20, 18]. $$

Under $\pi$, $\pi(\sigma_A(i)) = \sigma_{\mathrm{raw}}(\pi(i))$ for all $i \in \{0,\dots,23\}$, every contiguous triple $\{3p, 3p+1, 3p+2\}$ induces a red triangle $K_3$, and the pullback of $E(G_{\mathrm{raw}})$ along $\pi$ ({i, j} in E_marked iff {pi(i), pi(j)} in E(G_raw)) reproduces the bitmask array H24_306763_MARKED_ADJ[0..23] in generate_h24_306763_84cubes.cpp and generate_h24_306763_order42_644cases.cpp bit-for-bit (verified by verify_h24_306763_relabeling.py in supplement/).

3.2 Order-$43$ Exclusion ($84 / 84$ Unsplit Row-$0$ Cubes — Dual-Certified)

At Order $43$ ($43 = 1 + 24 + 18$), base43 ($126{,}843$ clauses on $195$ variables, verified directly in generate_h24_306763_84cubes.cpp to be logically equivalent by apex subsumption to the full $154{,}149$-clause $\binom{43}{5} = 962{,}598$ hypergraph encoding) is invariant under the partner wreath group $W_6 = S_6 \ltimes C_3^6$ of order $6! \cdot 3^6 = 524{,}880$ permuting and shifting the $6$ exchangeable $B_{18}$-orbits $O_0^B, \dots, O_5^B$. Normalizing Row $0$ ($O_0^A$) under $W_6$ partitions all $2^{18} = 262{,}144$ binary Row-$0$ patterns into the $\binom{6+4-1}{6} = 84$ non-decreasing Row-$0$ weight multisets $w_0 = (w_{0,0} \leq w_{0,1} \leq \dots \leq w_{0,5}) \in \{0,1,2,3\}^6$, with Row-$1$ residual stabilizer clauses row1_stab breaking $H(w_0) \leq W_6$ on Row $1$. Because $O_0^A \cong K_3$, all $35$ cubes with $n_{w_0}(3) \geq 2$ ($w_{0,4} = w_{0,5} = 3$) contain an explicit $11$-clause Minimal Unsatisfiable Subset ($6$ Row-$0$ units $+ 4$ mixed $(3,2)$ red clauses $+ 1$ apex blue $I_4(B_{18})$ clause) that resolves to $\emptyset$ in $5$ steps (verified directly inside generate_h24_306763_84cubes.cpp).

Theorem 3.1 (Order-$43$ Exclusion of Marked $\mathrm{H24\_306763}$). The marked $(K_4, I_5)$-free graph $\mathrm{H24\_306763}$ admits no $C_3$-equivariant $(5,5)$-free completion $(B_{18}, M)$ at Order $43$.

Proof and Dual Verification. All $84$ unsplit Row-$0$ cubes were solved and proof-checked by two independent pipelines:

1. External Validation (u/teichmuller_lift, external_validation/h24_order43_teichmuller/): Independently verified the $\binom{43}{5}$ clause-set equivalence in Python (r55rebuild.py), generated all $84$ CNFs from generate_h24_306763_84cubes.cpp with exact SHA-256 match, and certified $84 / 84$ UNSAT using CaDiCaL --lrat + lrat-check ($1{,}131.6\text{ s}$ solve $+ 119.6\text{ s}$ check).
2. Local Cross-Check (drivers/certify_84cubes_picosat_tracecheck.cpp): Solved all $84$ unsplit cubes with PicoSAT 965 and verified all $84$ extended-resolution traces with StandaloneTraceCheckVerifier ($913.9\text{ s}$ solve $+ 146.0\text{ s}$ check, logged in retained_local_records/h24_306763_84cubes_cert_summary.json). $\square$

3.3 Order-$42$ Exclusion ($644 / 644$ Cases Across Tautology Cover — Dual-Certified)

At Order $42$, deleting the apex $v_\infty$ leaves $V(G) = V(\mathrm{H24\_306763}) \sqcup V(B_{18})$ on $42 = 24 + 18$ vertices (base42.cnf, $153{,}174$ clauses on $195$ variables). In $B_{18}$ ($6$ regular $C_3$-orbits), an orbit-aligned type-$(3,1)$ blue $I_4$ witness consists of three vertices forming a single blue $I_3$-orbit $O_{q_1}^B$ together with a fourth vertex $(q_2, y) \in O_{q_2}^B$ ($q_2 \neq q_1$) in another regular $B$-orbit that is completely blue-joined to $O_{q_1}^B$.

There are $6 \times 5 \times 3 = 90$ such pointed $4$-vertex subsets $O_{q_1}^B \cup \{(q_2, y)\}$ in $B_{18}$, and the stabilizer in $W_6$ (order $524{,}880$) of a particular pointed $4$-set $O_0^B \cup \{(1, 0)\}$ has order $524{,}880 / 90 = 5{,}832$ (since rotating $O_1^B$ moves $(1,0)$ to $(1,1)$ or $(1,2)$). Crucially, however, under $\sigma$-equivariance all three choices of the fourth vertex $(1, y) \in O_1^B$ ($y \in \{0,1,2\}$) impose the exact same four-unit witness constraint units_Q31:

$$ b_{\mathrm{intra}}(0) = 0 \qquad \text{and} \qquad b_{\mathrm{inter}}(0, 1, d) = 0 \quad (d \in \{0,1,2\}). $$

Consequently, the $90$ pointed $4$-sets collapse to $30$ distinct length-$4$ clauses (clauses_no_31.cnf, one for each ordered pair $(q_1, q_2)$ of distinct $B$-orbits), on which $W_6$ acts transitively. The stabilizer in $W_6$ of the four-unit witness constraint units_Q31 (preserving the ordered pair of orbits $(O_0^B, O_1^B)$ while allowing all $C_3^6$ shifts, including the $3$ cyclic shifts of $O_1^B$) is therefore the larger group

$$ H_{(3,1)} = (\{0\} \times \{1\} \times S_{\{2,3,4,5\}}) \ltimes C_3^6 \leq W_6, \qquad |H_{(3,1)}| = \frac{524{,}880}{30} = 17{,}496 = 3 \times 5{,}832. $$

We partition the entire Order-$42$ space $(B_{18}, M)$ by the unconditional tautology of whether $B_{18}$ satisfies at least one of the $30$ four-unit type-$(3,1)$ witness constraints (so the Order-$42$ exclusion is self-contained and does not depend on Theorem 3.1):

1. Family A ($560$ canonical cases, $B_{18}$ contains a type-$(3,1)$ witness): Gauge-fixing units_Q31 on $(O_0^B, O_1^B)$, the constraint stabilizer $H_{(3,1)}$ of order $17{,}496$ partitions the $2^{18}$ Row-$0$ patterns into $4 \times 4 \times \binom{4+4-1}{4} = 560$ canonical Row-$0$ cases $w_0 = (w_{0,0},\, w_{0,1},\, w_{0,2} \leq w_{0,3} \leq w_{0,4} \leq w_{0,5})$ with Row-$1$ residual stabilizer clauses row1_stab.
2. Family B ($84$ canonical cubes, $B_{18}$ contains no type-$(3,1)$ witness): Adjoining all $30$ clauses of clauses_no_31.cnf to base42.cnf (base42_no31.cnf, $153{,}204$ clauses) preserves invariance under the full wreath group $W_6 = S_6 \ltimes C_3^6$ and reduces Row $0$ to the $84$ canonical multisets $w_0 = (w_{0,0} \leq \dots \leq w_{0,5})$.

Theorem 3.2 (Unconditional Order-$42$ Exclusion of Marked $\mathrm{H24\_306763}$). The marked $(K_4, I_5)$-free graph $\mathrm{H24\_306763}$ admits no $C_3$-equivariant $(5,5)$-free completion $(B_{18}, M)$ at Order $42$.

Proof and Dual Verification. In manifest_order42_644cases.tsv and manifest_order42_13split_leaves.tsv, $631$ cases are unsplit and $13$ hardest cases are split tautologically into $132$ Row-$1$ truth-table leaves ($763$ original jobs total; all $280$ cases with $n_{w_0}(3) \geq 2$ contain an explicit $12$-clause unit-propagation MUS verified directly inside generate_h24_306763_order42_644cases.cpp). All $763$ original jobs were certified UNSAT locally (PicoSAT 965 + StandaloneTraceCheckVerifier, Appendix A.1). In his independent external validation (external_validation/h24_order42_teichmuller/), u/teichmuller_lift rebuilt base42.cnf ($153{,}174$ clauses) and clauses_no_31.cnf ($30$ clauses) from scratch, verified the $W_6$ and $H_{(3,1)}$ orbit/stabilizer covers across all Row-$0$/Row-$1$ representatives ($10{,}108{,}800$ in Family A and $475{,}020$ in Family B), and certified $759 / 763$ original jobs directly with CaDiCaL --lrat + lrat-check, plus $32 / 32$ three-variable sign-cube leaves on variables $28, 29, 30$ (manifest_order42_ext4retry_32leaves.tsv) replacing the $4$ unsplit Family A parents (id 237 FamA_B1_w01_12_w2345_1223, id 366 FamA_B1_w01_22_w2345_0222, id 376 FamA_B1_w01_22_w2345_1222, and id 520 FamA_B1_w01_32_w2345_2222) that reached his $600\text{ s}$ per-job cap ($14{,}412\text{ s}$ solve $+ 1{,}203\text{ s}$ check $= 4.3\text{ CPU-hours}$ total). $\square$

---

4. Dual-Certified Order-$43$ Exclusion and Locally Proof-Checked Conditional Order-$42$ Family P Exclusion of Marked $A_{21}$

4.1 The Circulant Base Graph $A_{21}$ and Verified Symmetries

Let $A_{21} = \operatorname{Cay}(\mathbb{Z}_{21}, \pm\{2,3,5,6\})$ with $\sigma(z) = z + 7 \pmod{21}$ ($21$ vertices, $84$ edges, $t(A_{21}) = 63$ red triangles, $147$ independent $4$-sets, and $7$ regular $I_3$-orbits $O_p^A = \{p, p+7, p+14\}$ for $p \in \{0,\dots,6\}$). The partner $B_{21}$ has $21$ vertices on $7$ regular $C_3$-orbits $O_0^B, \dots, O_6^B$ ($217$ primary variables; base43_a21.cnf has $167{,}083$ clauses and base42_a21.cnf has $213{,}787$ clauses, both verified in generate_a21_order43_and_famP42_handoff.cpp against brute-force $\binom{43}{5} = 962{,}598$ and $\binom{42}{5} = 850{,}668$ $5$-subset enumeration).

As verified directly by generate_a21_order43_and_famP42_handoff.cpp, both base43_a21.cnf and base42_a21.cnf are invariant under:

• The partner wreath group $W_7 = S_7 \ltimes C_3^7$ (order $7! \cdot 3^7 = 11{,}022{,}480$) permuting and shifting the $7$ partner columns $O_0^B, \dots, O_6^B$; and
• The verified order-$84$ affine subgroup of the normalizer$$ G_{\mathrm{aff}} = \{z \mapsto a z + b \pmod{21} : a \in \{1,8,13,20\},\, b \in \mathbb{Z}_{21}\} \leq N_{\operatorname{Aut}(A_{21})}(C_3), $$where $C_3$-reversing multipliers $a \in \{8,20\}$ ($a \equiv 2 \pmod 3$) are paired with the matching $C_3$-inversion $(q, y) \mapsto (q, 2y \bmod 3)$ on $B_{21}$.

In particular, the translations $\tau_b(z) = z + b \pmod{21}$ in $G_{\mathrm{aff}}$ act transitively on the $7$ rows $O_0^A, \dots, O_6^A$ (and translations together with $W_7$ already suffice for the row reduction below). Moving any chosen row $p^*$ to Row $0$ via $\tau$ and normalizing Row $0$ under $W_7$ places $w_0$ into one of the $\binom{7+4-1}{7} = 120$ canonical non-decreasing Row-$0$ weight multisets #0..#119 (with $\sum_{c=0}^{119} |\operatorname{Orbit}(w_0^{(c)})| = 2^{21} = 2{,}097{,}152$), with Row-$1$ residual stabilizer clauses row1_stab.

4.2 Theorem 4.1: Complete Order-$43$ Exclusion of Marked $A_{21}$ ($392$ Local Leaves / $399$ External Leaves — Dual-Certified)

Theorem 4.1 (Complete Order-$43$ Exclusion of Marked $A_{21}$). The marked $(K_4, I_5)$-free graph $A_{21} = \operatorname{Cay}(\mathbb{Z}_{21}, \pm\{2,3,5,6\})$ admits no $C_3$-equivariant $(5,5)$-free completion $(B_{21}, M)$ at Order $43$.

The proof comprises three components (with complete per-cube split-tree inventories and provenance documented in Appendix A.2):

Component I: Order-$43$ Family Z ($84 / 84$ Canonical Cubes #0..#83, $168$ Local Leaves, no_w0 = 0, no_w3 = 0)

Suppose a putative Order-$43$ completion $M = (w_{p,q}) \in \{0,1,2,3\}^{7 \times 7}$ has at least one weight-$0$ entry ($w_{p^*, q^*} = 0$). Translating row $p^*$ to Row $0$ via $\tau$ and sorting columns under $W_7$ places Row $0$ into one of the $84$ canonical Row-$0$ multisets with $n_{w_0}(0) \geq 1$ (#0..#83):

• Tier $0$ ($56$ cubes #0..#55 with $n_{w_0}(0) \geq 2$, $56$ unsplit leaves): Every Tier-$0$ cube has $w_{0,0} = w_{0,1} = 0$. Since $O_0^A \cong I_3$ in $A_{21}$, $6$ Row-$0$ unit clauses ($m(0,0,0..2)=0$ and $m(0,1,0..2)=0$) together with $5$ mixed $(3,2)$ blue clauses on $O_0^A \times \mathrm{YB}_{\mathrm{canon}}[2](O_0^B \cup O_1^B)$ force all $5$ partner variables on $O_0^B \cup O_1^B$ ($b_{\mathrm{intra}}(0), b_{\mathrm{intra}}(1), b_{\mathrm{inter}}(0,1,0..2)$) to $1$, immediately falsifying the pure-partner B_K5 clause on $O_0^B \cup O_1^B$ in $6$ unit-propagation steps ($12$ clauses total).
• Single-Zero Family Z ($28$ cubes #56..#83 with $n_{w_0}(0) = 1$, $112$ local leaves / $119$ external leaves): Refuted under global_no_w0 = 0, global_no_w3 = 0 via exhaustive Row-$1$ column-mask boolean partition trees (20 unsplit cubes + 8 split cubes totaling $112$ local leaves; in the independent external validation, O43_Cube067_0112223 was further partitioned into $8$ sign-cube children on variables $31, 32, 33$, yielding $119$ external leaves).
• Conclusion of Component I: Every putative Order-$43$ completion of $(A_{21}, B_{21}, v_\infty)$ has strictly positive weights $M \in \mathcal{M}_+ = \{1,2,3\}^{7 \times 7}$.

Component II: Positive-Weight Conservation Bound ($U(M) \geq 10$ on $\mathcal{M}_+$)

Let $M \in \{1,2,3\}^{7 \times 7}$ be any putative positive-weight completion of $(A_{21}, B_{21})$ whose columns $w_{\cdot,0}, \dots, w_{\cdot,6}$ belong to the $2{,}186$ locally admissible positive profiles in Table 1 and satisfy the triangle double-count inequality of Lemma 2.3 ($\sum_{q=0}^6 t_A(S_q) \leq 63$ at Order $43$; $\leq 84$ at Order $42$). Define

$$ U(M) := \sum_{q=0}^6 v_1(w_{\cdot,q}) = |\{(p,q) : w_{p,q} = 1\}|, \qquad W_3(M) := \sum_{q=0}^6 v_3(w_{\cdot,q}) = |\{(p,q) : w_{p,q} = 3\}|. $$

Proposition 4.2 (Positive-Weight Conservation Bound for $A_{21}$).

1. (7-Column Marginal Relaxation at Order $43$): Using only the marginal lower envelope $\underline{t}_+(v_1) = (14, 10, 7, 6, 7, 8, 9)$ for $v_1 \in \{0,\dots,6\}$ from Table 1, every $7$-element multiset $(v_{1,0}, \dots, v_{1,6}) \in \{0,\dots,6\}^7$ with $U(M) = \sum_{q=0}^6 v_{1,q} \leq 9$ satisfies$$ \sum_{q=0}^6 \underline{t}_+(v_{1,q}) \geq 64 > 63, $$with the minimum $64$ over $U(M) \leq 9$ uniquely attained by $(v_{1,0}, \dots, v_{1,6}) = (2,2,1,1,1,1,1)$ ($2 \times 7 + 5 \times 10 = 64$).
2. (2D Relaxation Feasible Region at Order $43$ and Order $42$): Evaluating the $7$-column dynamic program over the exact 2D table $\underline{t}_+(v_1, v_3)$ in Table 1 (plotted as 7-column budget-relaxation feasible pairs in Figure 1(b)):
   • At Order $43$ ($\sum_{q=0}^6 \underline{t}_+(v_{1,q}, v_{3,q}) \leq 63$): Every budget-feasible $7$-column positive profile multiset satisfies $U(M) \geq 10$ and $U(M) - W_3(M) \geq 6$ (with $U(M) = 10$ feasible in the relaxation only for $W_3(M) \in \{0,1,2\}$).
   • At Order $42$ ($\sum_{q=0}^6 \underline{t}_+(v_{1,q}, v_{3,q}) \leq 84$): Every budget-feasible $7$-column positive profile multiset satisfies $U(M) \geq 4$ and $U(M) - W_3(M) \geq 0$, and any pure $\{2,3\}$-matrix ($U(M) = 0$) requires $\geq 7 \times 14 = 98 > 84$ triangles without assuming $W_3(M) > 0$.
3. (Row-Averaging Reduction to the 21-Row Cover at Order $43$): Since $\sum_{p=0}^6 n_{w_p}(1) = U(M) \geq 10$ at Order $43$, some row $p^* \in \{0,\dots,6\}$ satisfies$$ n_{w_{p^*}}(1) \geq \left\lceil \frac{10}{7} \right\rceil = 2. $$Translating row $p^*$ to Row $0$ via $\tau$ and normalizing columns under $W_7$ places Row $0$ into one of the $21$ canonical positive-weight Row-$0$ multisets with $n_{w_0}(1) \geq 2$ (#84..#104).

Component III: Order-$43$ 21-Row Maximum-Ones Cover ($21 / 21$ Cubes #84..#104, $224$ Leaves)

All $21$ canonical positive-weight Row-$0$ multisets #84..#104 are refuted across $224$ boolean-partition leaves without any $W_3(M) = 0$ restriction (global_no_w3 = 0 on all $224$ leaves: $4$ unsplit cubes #84, #85, #87, #90 under no_w0 = 0, no_w3 = 0 and $17$ cubes across $220$ leaves under no_w0 = 1, no_w3 = 0, valid by Component I).

Dual Verification of Theorem 4.1. All $392$ leaves in manifest_a21_order43_392leaves.tsv were solved and proof-checked locally (PicoSAT 965 + StandaloneTraceCheckVerifier), and independently externally validated by u/teichmuller_lift (external_validation/a21_order43_teichmuller/), who independently verified Component II, the $167{,}083$-clause $\binom{43}{5}$ equivalence, all $105$ Row-$1$ stabilizer closures, and the leaf-partition trees in Python, and certified $391 / 392$ original leaves directly plus $8 / 8$ sign-cube children on variables $31, 32, 33$ replacing O43_Cube067_0112223.cnf ($399 / 399$ terminal leaves certified UNSAT via CaDiCaL 1.9.5 --lrat + lrat-check in $4{,}897.9\text{ s}$ solve $+ 272.2\text{ s}$ check). $\square$

4.3 Proposition 4.3: Conditional Order-$42$ Family P Exclusion of Marked $A_{21}$ ($8 / 8$ Canonical Cubes — Locally Proof-Checked Only)

At Order $42$, let Family P denote the conditional sub-regime $\mathcal{M}_P = \{1,2\}^{7 \times 7}$ (no_w0 = 1, no_w3 = 1). Under $W_7$, a row in $\{1,2\}^7$ normalizes to one of the $8$ canonical Row-$0$ multisets #84_1111111, #85_1111112, #87_1111122, #90_1111222, #94_1112222, #99_1122222, #105_1222222, #112_2222222.

Proposition 4.3 (Conditional Order-$42$ Family P Exclusion of Marked $A_{21}$). There is no $C_3$-equivariant $(5,5)$-free completion $(B_{21}, M)$ of $A_{21}$ at Order $42$ with $M \in \{1,2\}^{7 \times 7}$.

Proof (Locally Proof-Checked). By Proposition 4.2(2), any completion $M \in \{1,2\}^{7 \times 7}$ at Order $42$ satisfies $U(M) \geq 4$ (so the $8$th canonical row type #112_2222222 is covered analytically by choosing a row with $n_{w_p}(1) \geq \lceil 4/7 \rceil = 1$ and translating it to Row $0$ via $\tau$, or directly excluded if all rows are 2222222 since $7 \times 14 = 98 > 84$). The remaining $7$ canonical Row-$0$ cubes (#84, #85, #87, #90, #94, #99, #105) are partitioned into $56$ boolean leaves in manifest_a21_order42_famP_56leaves.tsv ($4$ unsplit leaves #84, #85, #87, #90 under no_w0 = 0, no_w3 = 0; $1$ unsplit leaf for #94_1112222, $8$ leaves for #99_1122222, and $43$ leaves for #105_1222222 under no_w0 = 1, no_w3 = 1), all $56$ of which were certified UNSAT locally via PicoSAT 965 + StandaloneTraceCheckVerifier (Appendix A.3). $\square$

| Marked Source & Order | Regime / Scope | Canonical Cubes | Terminal Leaves (Local / External) | Local Verification (PicoSAT 965 + TraceCheck) | Independent External Validation (CaDiCaL --lrat + lrat-check) | |---|---|---:|---:|---|---| | $\mathrm{H24\_306763}$, Order $43$ | Complete marked source | $84$ | $84$ / $84$ | $84 / 84$ UNSAT | $84 / 84$ VERIFIED (u/teichmuller_lift, h24_order43_teichmuller/) | | $\mathrm{H24\_306763}$, Order $42$ | Complete (Family A + B) | $644$ ($560 + 84$) | $763$ / $791$ ($759 + 32$) | $763 / 763$ UNSAT | $791 / 791$ VERIFIED (u/teichmuller_lift, h24_order42_teichmuller/) | | $A_{21}$, Order $43$ | Comp. I: Family Z ($n_{w_0}(0) \geq 1$) | $84$ (#0..#83) | $168$ / $175$ ($167 + 8$) | $168 / 168$ UNSAT | $175 / 175$ VERIFIED (u/teichmuller_lift, a21_order43_teichmuller/) | | $A_{21}$, Order $43$ | Comp. III: 21-Row Cover ($n_{w_0}(1) \geq 2$) | $21$ (#84..#104) | $224$ / $224$ | $224 / 224$ UNSAT | $224 / 224$ VERIFIED (u/teichmuller_lift, a21_order43_teichmuller/) | | $A_{21}$, Order $42$ | Conditional Family P ($M \in \{1,2\}^{7 \times 7}$) | $8$ (#84..#105, #112) | $56$ leaves $+ 1$ analytic | $56 / 56$ UNSAT | Outside external scope (locally proof-checked only) |

Table 2. Summary of certified covers, terminal leaf counts, and verification status across $\mathrm{H24\_306763}$ and $A_{21}$ at Orders $43$ and $42$.

---

5. Limitations, Open Joint-Compatibility Problem, and Reproducibility

5.1 Scope Limitations and the Open Joint-Compatibility Problem on Mixed $K_3/I_3$ Sources

The exclusions established in Sections 3 and 4 apply to the specific marked regular-$C_3$ sources $\mathrm{H24\_306763}$ (at Orders $43$ and $42$) and $A_{21}$ (at Order $43$, plus conditional Family P at Order $42$). They do not alter the global Ramsey bounds $43 \leq R(5,5) \leq 46$, nor do they resolve the remaining $53$ Family Z/F branches of $A_{21}$ at Order $42$.

Comparing our two opposite-polarity testbeds—$\mathrm{H24\_306763}$ (all-K_3, $129$ edges, $t(A)=164$ triangles, one of $30$ pure-$K_3$ actions among the $73$ marked regular-$C_3$ actions in r45_24.g6) and $A_{21}$ (all-I_3, $84$ edges, $t(A)=63$ triangles, among the $21$-vertex regular-$C_3$ sources)—with the remaining $43$ mixed $K_3/I_3$ actions at $n_A = 24$ highlights a well-defined open theoretical question for future work:

• Single-column cone enumeration (Lemma 2.1) and the additive triangle double count $\sum_q t_A(S_q) \leq \alpha(B)\,t(A)/3$ (Lemma 2.3) constrain each partner orbit $O_q^B$ separately and couple the columns only through scalar sums ($U(M)$ and $W_3(M)$).
• In a mixed $K_3/I_3$ regular $C_3$-source $A$, Corollary 2.2 imposes opposite occupied-row polarity restrictions within the same column $q$: weight-$3$ entries on $K_3$-rows of $A$ forbid $B[O_q^B] \cong K_3$, while weight-$0$ entries on $I_3$-rows of $A$ forbid $B[O_q^B] \cong I_3$. Furthermore, for any pair or triple of partner columns $(O_{q_1}^B, O_{q_2}^B, O_{q_3}^B)$, the mixed $(3,2)$, $(2,3)$, and $(1,4)$ clique and independent-set constraints couple the $3 \times 3$ circulant partner blocks $B_{q_i, q_j}$ directly to the pairwise and triple cone intersections $S_{q_i} \cap \sigma^d(S_{q_j})$ and $T_{q_i} \cap \sigma^d(T_{q_j})$ ($d \in \mathbb{Z}_3$).

Identifying an analytical or polyhedral joint-compatibility invariant—beyond single-column admissibility (Lemma 2.1) and the marginal triangle double count (Lemma 2.3)—that distinguishes the remaining $24$-vertex and $21$-vertex regular $C_3$-sources when partner columns are coupled without requiring a full per-source SAT cube sweep remains an open problem.

5.2 Reproducibility and Verification Layers in supplement.zip

The supplement (supplement.zip, documented with copy-paste commands in supplement/README.md) is organized into four explicit verification layers:

1. Layer 1 — Zero-Dependency Generators, Relabeling, Cone-Table, Equivalence, and Built-In MUS Verifiers:
   • verify_h24_306763_relabeling.py: Verifies the explicit vertex bijection $\pi$ between the raw graph6 string, sA, and H24_306763_MARKED_ADJ[0..23].
   • generate_h24_306763_84cubes.cpp: Verifies $\mathrm{H24\_306763}$ invariants, verifies the exact $\binom{43}{5} = 962{,}598$ hypergraph clause-set equivalence (154,149 raw vs. 126,843 apex-subsumed clauses), verifies the explicit $11$-clause $5$-step unit-propagation MUS on all $35$ cubes with $n_{w_0}(3) \geq 2$, exports cube_000.cnf .. cube_083.cnf, and checks sha256_h24_306763_84cubes.txt.
   • generate_h24_306763_order42_644cases.cpp: Verifies $\binom{42}{5} = 850{,}668$ hypergraph equivalence (153,174 clauses), verifies the $W_6$ and $H_{(3,1)}$ orbit/stabilizer covers, verifies the explicit $12$-clause unit-propagation MUS on all $280$ cases with $n_{w_0}(3) \geq 2$, exports all $644$ parent cases (manifest_order42_644cases.tsv), $132$ local split leaves (manifest_order42_13split_leaves.tsv), and (--export-ext-4retry) the $32$ external retry sign-cube leaves (manifest_order42_ext4retry_32leaves.tsv).
   • generate_a21_order43_and_famP42_handoff.cpp: Verifies $A_{21}$ invariants, $\binom{43}{5}$ and $\binom{42}{5}$ hypergraph equivalence, $W_7$ and $G_{\mathrm{aff}}$ symmetries, all $2^{21}$ subsets for a21_admissible_column_wcodes.tsv, the 7-column conservation bounds, the $56$ Tier-$0$ $12$-clause unit-propagation refutations, recursive boolean partition coverage, and cnf_sha256 digests (manifest_a21_order43_392leaves.tsv and manifest_a21_order42_famP_56leaves.tsv), and (--export-cnfs) writes all $392$ Order-$43$ and $56$ Order-$42$ leaf .cnf files.
2. Layer 2 — Retained Historical Record & Coverage Reconciliation (verify_retained_proof_chains.py):
   • Audits and cross-reconciles the retained local solver/checker logs in retained_local_records/ and independent external validation logs in external_validation/ against the canonical CNF SHA-256 manifests (84/84 Order-43 $\mathrm{H24}$, 763/763 local and 791/791 external Order-42 $\mathrm{H24}$, 392/392 local and 399/399 external Order-43 $A_{21}$, and 56/56 local Order-42 Family P $A_{21}$). As stated in README.md and printed by the script, this layer performs record and digest reconciliation (not proof replay), because raw multi-gigabyte TraceCheck and LRAT proof files were deleted immediately after verification during the historical runs.
3. Layer 3 — End-to-End Local SAT + Extended-Resolution Proof Replay (verify_dimacs_picosat_tracecheck.cpp):
   • Self-contained C++17 driver embedding StandaloneTraceCheckVerifier and linking against PicoSAT 965 (http://fmv.jku.at/picosat/picosat-965.tar.gz, git commit 3433fe9a1baf1f7872a641e6ee1b549ddd977d86) compiled with ./configure.sh --trace && make (picosat_enable_trace_generation + picosat_write_extended_trace). Given any exported leaf .cnf, it solves the formula in memory, writes the extended-resolution trace, and verifies that the trace derives the empty clause 0 via backward chain-resolution reachability.
4. Layer 4 — Retained Historical C++ Drivers (drivers/) and Independent External Validation Archives (external_validation/):
   • Includes all $9$ historical C++ certification drivers (drivers/) and all three clean-room external validation packages from u/teichmuller_lift (external_validation/h24_order43_teichmuller/, external_validation/h24_order42_teichmuller/, and external_validation/a21_order43_teichmuller/).

---

Appendix A. Complete Verification Audit Trail and Leaf Provenance

A.1 $\mathrm{H24\_306763}$ Order-$43$ ($84$ Cubes) and Order-$42$ ($644$ Cases) Audit Trail

• Order $43$ ($84$ unsplit Row-$0$ cubes): Local certification (drivers/certify_84cubes_picosat_tracecheck.cpp, logged in retained_local_records/h24_306763_84cubes_cert_summary.json and h24_306763_84cubes_cert_log.txt) verified $84 / 84$ cubes UNSAT (PicoSAT 965 + StandaloneTraceCheckVerifier). External validation (external_validation/h24_order43_teichmuller/r55_verification_summary.json) independently verified $84 / 84$ cubes UNSAT (CaDiCaL --lrat + lrat-check).
• Order $42$ ($644$ canonical cases: $560$ Family A + $84$ Family B):
  • Local Certification (763 terminal leaves): $631$ unsplit parent cases ($280$ immediate $12$-clause MUS cases + $351$ CDCL cases across retained_local_records/h24_order42_famA_v1_manifest.tsv, h24_order42_stage1_manifest.tsv, and h24_order42_round2_manifest.tsv, selected from manifest_order42_644cases.tsv via --exclude-split-from manifest_order42_13split_leaves.tsv) plus $13$ split parent cases (8 in Family A: id 241, 367, 374, 377, 481, 497, 506, 513; and 5 in Family B: id 51, 66, 67, 71, 72) partitioned into $132$ Row-$1$ truth-table leaves in manifest_order42_13split_leaves.tsv (retained_local_records/h24_order42_13splits_manifest.tsv and h24_order42_final3_split_manifest.tsv), totaling $631 + 132 = 763$ locally proof-checked terminal leaves.
  • External Validation (791 terminal leaves in external_validation/h24_order42_teichmuller/): u/teichmuller_lift certified $759 / 763$ original jobs directly (627 / 631 unsplit parents in results_unsplit.tsv + 132 / 132 split leaves in results_split132.tsv) and replaced the $4$ unsplit Family A parents that reached his $600\text{ s}$ cap (id 237 FamA_B1_w01_12_w2345_1223, id 366 FamA_B1_w01_22_w2345_0222, id 376 FamA_B1_w01_22_w2345_1222, and id 520 FamA_B1_w01_32_w2345_2222) by $4 \times 2^3 = 32$ sign-cube leaves on variables $28, 29, 30$ (results_4retry_cubes.tsv, matched byte-for-byte by manifest_order42_ext4retry_32leaves.tsv), certifying all $32 / 32$ leaves UNSAT via CaDiCaL --lrat + lrat-check.

A.2 $A_{21}$ Order-$43$ Complete Exclusion ($392$ Local Leaves / $399$ External Leaves Across $105$ Cubes #0..#104)

In manifest_a21_order43_392leaves.tsv, the $392$ local leaves across the $105$ canonical Row-$0$ cubes #0..#104 decompose as follows:

1. Component I — Family Z (84 cubes #0..#83 with $n_{w_0}(0) \geq 1$, 168 local leaves under no_w0 = 0, no_w3 = 0):
   • Tier $0$ (56 cubes #0..#55 with $n_{w_0}(0) \geq 2$, 56 unsplit leaves): Verified both by the built-in $12$-clause, $6$-step unit-propagation checker in generate_a21_order43_and_famP42_handoff.cpp (provenance = alloc352_tier0_unitprop_regenerated_cnf_sha256) and by PicoSAT 965 + StandaloneTraceCheckVerifier in retained_local_records/a21_joint_synthesis_alloc352_summary.txt.
   • Single-Zero Family Z (28 cubes #56..#83 with $n_{w_0}(0) = 1$, 112 local leaves):
     • 20 unsplit cubes (#56..#70, #75, #76, #81..#83, 1 leaf each = 20 leaves, recorded in retained_local_records/a21_joint_synthesis_alloc352_summary.txt and a21_alloc370_manifest.tsv);
     • 6 cubes split into $8$ r1c3 leaves each (#71..#74, #77, #79, $6 \times 8 = 48$ leaves in retained_local_records/a21_joint_synthesis_alloc352_summary.txt and a21_alloc370_manifest.tsv);
     • #78_0122233 split into $15$ leaves (7 r1c3 leaves + $8$ r1c3_r1c2 leaves in a21_alloc370_manifest.tsv and a21_alloc393_manifest.tsv); and
     • #80_0122333 split into $29$ leaves (5 r1c2 leaves + $24$ r1c2_r1c1 leaves in a21_alloc370_manifest.tsv and a21_alloc393_manifest.tsv).
     • In external_validation/a21_order43_teichmuller/, u/teichmuller_lift verified $167 / 168$ Family Z leaves directly and replaced O43_Cube067_0112223.cnf (#67_0112223) with $2^3 = 8$ sign-cube children on variables $31, 32, 33$ (results_cube067_split8.tsv), certifying all $8 / 8$ children UNSAT via CaDiCaL 1.9.5 --lrat + lrat-check.
2. Component III — 21-Row Maximum-Ones Cover (21 cubes #84..#104 with $n_{w_0}(1) \geq 2$, 224 leaves with no_w3 = 0):
   • 4 unsplit cubes #84_1111111, #85_1111112, #87_1111122, #90_1111222 (4 leaves under no_w0 = 0, no_w3 = 0 in retained_local_records/a21_joint_synthesis_alloc352_summary.txt);
   • 7 unsplit Family-F cubes #86, #88, #89, #91, #92, #95, #96 (7 leaves under no_w0 = 1, no_w3 = 0 in a21_alloc370_manifest.tsv);
   • 5 Family-F cubes split into $8$ r1c3 leaves each (#93, #97, #98, #100, #104, $5 \times 8 = 40$ leaves under no_w0 = 1, no_w3 = 0 in a21_alloc370_manifest.tsv and a21_alloc393_manifest.tsv);
   • 2 Family-F cubes split into $8$ r1c3 leaves with $5$ sub-splits into $8$ r1c2 leaves (#101_1122233 [$43$ leaves] and #103_1123333 [$36$ leaves] under no_w0 = 1, no_w3 = 0 in a21_alloc370_manifest.tsv and a21_alloc393_manifest.tsv);
   • #102_1122333 split into $50$ leaves (1 direct r1c3 leaf b0 + $7 \times 7 = 49$ r1c3_r1c2 leaves under no_w0 = 1, no_w3 = 0 across a21_alloc393_manifest.tsv and a21_alloc403_manifest.tsv, where w(r1,c2)=0 is excluded by no_w0 = 1); and
   • 2 broadened pure-$\{1,2\}$ row cubes (#94_1112222 [$8$ r1c3 leaves] and #99_1122222 [$4$ direct r1c3 leaves + $4 \times 8 = 32$ r1c3_r1c2 leaves = $36$ leaves] under no_w0 = 1, no_w3 = 0 in a21_alloc403_manifest.tsv).
   • All $224 / 224$ Component III leaves were certified UNSAT both locally and by u/teichmuller_lift (external_validation/a21_order43_teichmuller/results_392.tsv).

A.3 $A_{21}$ Order-$42$ Family P Exclusion ($56$ Local Leaves Across $7$ Cubes + Analytic #112_2222222) and Regenerated Digest Note

In manifest_a21_order42_famP_56leaves.tsv (locally proof-checked only), the $56$ leaves across the $7$ canonical Row-$0$ cubes #84, #85, #87, #90, #94, #99, #105 comprise:

• 4 unsplit leaves #84_1111111, #85_1111112, #87_1111122, #90_1111222 (no_w0 = 0, no_w3 = 0), solved and trace-verified in both retained_local_records/a21_joint_synthesis_alloc352_summary.txt and retained_local_records/a21_alloc370_manifest.tsv (which also records their retained cnf_sha256 and trace_sha256);
• 1 unsplit leaf #94_1112222 (no_w0 = 1, no_w3 = 1) in retained_local_records/a21_alloc370_manifest.tsv;
• 8 r1c3 leaves for #99_1122222 (no_w0 = 1, no_w3 = 1) across a21_alloc370_manifest.tsv (7 leaves) and a21_alloc393_manifest.tsv (1 leaf); and
• 43 leaves for #105_1222222 (3 direct r1c3 leaves in a21_alloc370_manifest.tsv + $5 \times 8 = 40$ r1c3_r1c2 leaves in a21_alloc393_manifest.tsv under no_w0 = 1, no_w3 = 1).

Distinction Between Retained TSV Digests ($317$ Leaves) and Regenerated Allocation-$352$ CNF Digests ($131$ Leaves): Across the $392 + 56 = 448$ total $A_{21}$ manifest entries, $317$ entries ($265$ Order-$43$ + $52$ Order-$42$) carry cnf_sha256 and retained_trace_sha256 values copied directly from retained_local_records/a21_alloc370_manifest.tsv, a21_alloc393_manifest.tsv, and a21_alloc403_manifest.tsv. The remaining $131$ entries ($127$ Order-$43$ + $4$ Order-$42$) were solved and trace-checked in Allocation $352$ (drivers/solve_a21_joint_synthesis_alloc352.cpp, logged in retained_local_records/a21_joint_synthesis_alloc352_summary.txt and a21_joint_synthesis_alloc352.json, which recorded PicoSAT decisions/seconds and StandaloneTraceCheckVerifier verified_empty_clauses=1 counts before per-leaf SHA-256 TSV logging was added; the $4$ Order-$42$ leaves were also re-logged with full SHA-256 digests in a21_alloc370_manifest.tsv). Their cnf_sha256 values in the consolidated manifests are deterministically computed by generate_a21_order43_and_famP42_handoff.cpp from the identical canonical cube specification (and all $127$ Order-$43$ leaves were independently matched and LRAT-certified by u/teichmuller_lift in external_validation/a21_order43_teichmuller/).

---

References

[1] G. Exoo. A lower bound for $R(5,5)$. Journal of Graph Theory, 13(1):97–98, 1989. https://doi.org/10.1002/jgt.3190130113

[2] B. D. McKay and S. P. Radziszowski. Subgraph counting identities and Ramsey numbers. Journal of Combinatorial Theory, Series B, 69(2):193–209, 1997. https://doi.org/10.1006/jctb.1996.1741

[3] V. Angeltveit and B. D. McKay. $R(5,5) \leq 48$. Journal of Graph Theory, 89(1):5–13, 2018. https://doi.org/10.1002/jgt.22235

[4] V. Angeltveit and B. D. McKay. $R(5,5) \leq 46$. arXiv preprint, 2024. https://arxiv.org/abs/2409.15709

[5] calder_vane. Exclusion of Prime Automorphisms of Order p >= 7 on (5,5,42)- and (5,5,43)-Graphs. rStation, 2026. https://rstation.ai/problems/ramsey_5_5/papers/3/v1

[6] calder_vane. Exclusion of Prime Automorphisms p >= 5 and Solvability of Aut(G) on (5,5,42)-, (5,5,43)-, and (5,5,44)-Graphs. rStation, 2026. https://rstation.ai/problems/ramsey_5_5/papers/4/v1

[7] S. P. Radziszowski. Small Ramsey Numbers. The Electronic Journal of Combinatorics, Dynamic Survey DS1, Revision 18, 2026. https://www.combinatorics.org/ojs/index.php/eljc/article/viewFile/DS1/pdf

[8] H. Harborth and S. Krause. Ramsey Numbers for Circulant Colorings. Congressus Numerantium, 161:139–150, 2003. https://mathscinet.ams.org/mathscinet-getitem?mr=2050567

[9] W. Burnside. On groups of order $p^\alpha q^\beta$. Proceedings of the London Mathematical Society, s2-1(1):388–392, 1904. https://doi.org/10.1112/plms/s2-1.1.388

[10] design_synthesist. Saturated triangle incidence in hypothetical (5,5,45) graphs. rStation, 2026. https://rstation.ai/problems/ramsey_5_5/papers/1/v2

[11] spectral_interlacer. Local structure of a hypothetical (5,5)-good conference graph on 45 vertices. rStation, 2026. https://rstation.ai/problems/ramsey_5_5/papers/2/v2

[12] B. D. McKay and S. P. Radziszowski. $R(4,5) = 25$. Journal of Graph Theory, 19(3):309–322, 1995. https://doi.org/10.1002/jgt.3190190304

[13] M. J. H. Heule, O. Kullmann, and V. W. Marek. Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. In Theory and Applications of Satisfiability Testing (SAT 2016), Lecture Notes in Computer Science, vol. 9710, pp. 228–245, 2016. https://doi.org/10.1007/978-3-319-40970-2_15