(a) Every colour class is a Hamilton cycle of length $2m+1\ge7$, so $M=0$. Formula (1) now gives (5), proving sharpness without an existence black box.

(d) The standalone verifier reconstructs (6), checks every edge exactly once, checks balance, and recomputes the following initial values:

| $m$ | $n=2m+1$ | exact minimum $R$ |

|---:|---:|---:|

| 3 | 7 | 14 |

| 4 | 9 | 48 |

| 5 | 11 | 110 |

| 6 | 13 | 208 |

| 7 | 15 | 350 |

| 8 | 17 | 544 |

| 9 | 19 | 798 |

| 10 | 21 | 1120 |

4. A uniform positive class for problem 811

Recall that the 2-core is obtained by repeatedly deleting vertices of degree at most one.

Theorem C

(a) Let $G$ be a finite simple graph with $m\ge1$ edges and $v$ vertices. If either

1. $G$ is a forest, or

2. the 2-core of $G$ is a single triangle,

then every balanced $m$-colouring of $K_{mt+1}$ contains a rainbow $G$ whenever

Consequently every such $G$ has the property asked for in problem 811.

(a), proof for forests. Assign the $m$ colours bijectively to the $m$ edges of $G$. Root every nontrivial tree component and orient its edges away from the root. Place a root at any unused host vertex. Suppose $u$ target vertices have been placed and the next oriented edge, from an already placed parent to a new child, was assigned colour $c$. The parent has exactly $t$ neighbours in colour $c$. At most $u-1\le v-2$ of these are already used (the parent itself is not in its own neighbourhood), while $t\ge v-1$. Hence an unused choice exists. Continue through all components, then place isolated vertices arbitrarily.

(a), proof for triangle 2-core. By Theorem A, the host contains a rainbow triangle. Map the core triangle of $G$ onto it. Deleting those three core edges from $G$ leaves a forest, and every resulting component meets the core triangle in at most one vertex; otherwise another cycle would survive in the 2-core. Assign the remaining $m-3$ colours bijectively to the remaining $m-3$ edges and apply the same rooted extension, rooting an attached component at its already embedded core vertex. Condition (7) again guarantees every step.

(c) This is an elementary positive classification, not a claim of publication novelty. Targeted searches did not locate this exact formulation.

5. What lexicographic amplification can and cannot do

For colourings $c$ of $K_q$ and $d$ of $K_s$ on the same palette, their lexicographic product colours an edge between $(x,a)$ and $(y,b)$ by $c(xy)$ if $x\ne y$, and by $d(ab)$ if $x=y$.

Lemma D: lexicographic products necessarily create a rainbow \(C_6\)

(a) Let $c$ be any balanced colouring with at least six colours. Then $c\times c$ contains a rainbow $C_6$. In particular, no balanced six-colour base—whether or not it avoids $C_6$ itself—can be amplified to a $C_6$ counterexample by the Axenovich–Clemen lexicographic-power method.

(a), proof. By Theorem A, choose three outer blocks $A,B,C$ whose cross edges have three distinct colours $a,b,c$. Choose three other distinct colours $d,e,f$. Every colour occurs on an edge of the base, so choose a $d$-edge inside block $A$, an $e$-edge inside $B$, and an $f$-edge inside $C$. Traversing the internal edge in $A$, then the $AB$ cross edge, then the internal edge in $B$, then $BC$, then the internal edge in $C$, then $CA$, gives a $C_6$ with colours

all distinct.

(d) For the published Clemen–Wagner matrix, the verifier constructs the explicit lex-square cycle

with colour sequence $(1,2,4,3,6,5)$.

Lemma E: an exact finite reduction for \(2K_3\)

For a colouring $c$, let $\mathcal P(c)$ be the set of three-element colour sets realized by rainbow triangles.

(a) For two colourings on the same palette,

A triangle in the product either lies inside one outer block, uses exactly two outer blocks, or uses three. In the middle case its two cross edges have the same colour, so it is not rainbow; the other two cases give (8).

(a) Consequently, for a six-colour base $c$:

• if $\mathcal P(c)$ contains no complementary pair $S,[6]\setminus S$, then every lexicographic power $c^k$ is rainbow-$2K_3$-free;
• if $\mathcal P(c)$ contains a complementary pair, then $c^2$ contains a rainbow $2K_3$ (put realizing triangles inside two different outer blocks).

(a) Lexicographic powers of a balanced base remain balanced: if every base colour has degree $t$ on $q$ vertices, then in $c\times c$ every colour has degree $tq+t$, independently of the vertex and colour. Also $q^k\equiv1\pmod6$ when $q\equiv1\pmod6$.

(a) Thus the historic $2K_3$ subcase has the following exact, finite sufficient target:

> Find one balanced six-colouring whose rainbow-triangle palette family is complement-free.

Such a base would immediately give arbitrarily large counterexamples and would include the uniformity step that a lone finite colouring lacks.

6. Exact computations and certificates

The standard-library verifier is:

• runs/erdos811_wave6m_verify.py

Run:

python3 runs/erdos811_wave6m_verify.py

(d, independently rechecked by that script) The published Clemen–Wagner $K_{13}$ matrix is symmetric, uses colours $1,\ldots,6$, and every vertex has degree two in every colour. It has:

• 0 rainbow $K_4$ among all $\binom{13}{4}=715$ vertex sets;
• 2550 unoriented rainbow $C_6$ copies among all 102,960 unoriented $C_6$ copies;
• 354 rainbow $2K_3$ copies among all 17,160 unordered pairs of disjoint triples;
• triangle counts $(M,B,R)=(0,78,208)$;
• all 20 possible rainbow-triangle colour palettes.

(a+d) Two short witnesses show directly that this known $K_4$ certificate does not address the other challenges:

• $C_6=(0,2,1,5,3,4)$ has edge colours $(5,3,6,4,2,1)$.
• The triangles $\{0,4,8\}$ and $\{1,2,3\}$ have colours $\{1,2,4\}$ and $\{3,5,6\}$.

(d) The verifier exhausts every labelled balanced three-colouring for the first two orders:

• $K_4$: 3 one-factors and 6 labelled balanced colourings, all with $(M,B,R)=(0,0,4)$.
• $K_7$: 465 spanning 2-factors and 13,950 labelled balanced colourings, with the exact histogram

| $(M,B,R)$ | number of labelled colourings |

|---|---:|

| $(0,21,14)$ | 5760 |

| $(1,18,16)$ | 7560 |

| $(3,12,20)$ | 630 |

(a) The sharp minimum 14 also follows uniformly from Corollary B, so the exhaustive table is a cross-check rather than the proof of the minimum.

(a+d) A labelled spanning 2-factor of $K_{13}$ has one of ten cycle types. Summing

over partitions of 13 into parts at least three gives exactly

possible choices for just one colour class. The verifier recomputes this number; it explains why raw factorization enumeration is not a credible next step.

7. Search attempts that did not become theorems

Auxiliary reproducible search files:

• runs/erdos811_wave6m_search.py: seeded local search using balance-preserving alternating four-cycle switches.
• runs/erdos811_wave6m_sat.py: exact SAT encoding of a balanced $K_{13}$ with no rainbow $2K_3$.
• runs/erdos811_wave6m_palette_sat.py: SAT encoding of the stronger complement-free-palette base, plus an experimental pure-Python DRUP checker.

(d, negative heuristic only) From the published matrix, 20,000 seeded four-cycle switches reduced the number of rainbow $2K_3$ copies from 354 to 136 but did not reach zero. A cyclic-base restart ended at 196. This says nothing about nonexistence.

(d, undecided) The direct $2K_3$ SAT instance had 106,938 variables and 745,302 clauses after a safe symmetry normalization; it encoded all 17,160 patterns. CaDiCaL did not decide it within the hard 180-second cap.

(d, explicitly not promoted to a certified result) Two independent SAT runs reported that no balanced six-colouring of $K_{13}$ has a complement-free rainbow-triangle palette family:

• CaDiCaL 1.9.5 returned UNSAT in 4.9 seconds on a 3998-variable sequential-counter encoding.
• Glucose 4 returned UNSAT in 8.0 seconds on a transparent 488-variable, 53,686-clause subset encoding.

The latter emitted 436,028 DRUP lines (28,030,465 bytes when newline-joined), SHA-256

75972ef54a5371938977c02c896a5664e62f0e004b288ad9cb95059a813e3ebf

(d/c) The included from-scratch Python reverse-unit checker did not finish within a separate 180-second cap (and had not reached its first 50,000-addition progress mark). Therefore this report does not assert the $K_{13}$ palette instance UNSAT as a verified theorem. The solver agreement and proof hash are a precise lead only.

8. Exact wall and next computations

(a) A finite $C_6$-free base is insufficient by itself: Lemma D proves that its lexicographic square already has a rainbow $C_6$. A $C_6$ counterexample therefore needs a genuinely different infinite construction or a non-lexicographic amplification theorem. This is the exact structural obstruction to reusing the successful clique machinery.

(a) For $2K_3$, Lemma E isolates a finite certificate that would include the uniformity step: a complement-free palette base. The first admissible order is 13. The current exact missing item is either:

1. a checked UNSAT certificate at order 13 followed by a search at order 25, or

2. a directly checkable complement-free base at some order $6t+1$.

(c, cost estimate) An optimized DRAT/LRAT check of the already generated 28 MB proof should be budgeted at under 1 core-hour; the pure-Python implementation is the bottleneck, not proof generation. If order 13 is certified impossible, an order-25 complement-free-palette SAT search has 1800 edge-colour variables before auxiliaries and 276,000 triangle-palette implication clauses. A reasonable first portfolio is 32 solver jobs for two hours each, or 64 core-hours; this is an experimental budget, not a runtime guarantee.

(c, cost estimate) The analogous auxiliary-variable encoding of all $C_6$ constraints at order 13 has 102,960 cycle patterns, about 621,738 variables and 4,434,702 clauses. A serious exact run would merit roughly 128–512 core-hours plus a checked UNSAT certificate. Because Lemma D blocks lexicographic amplification even if a finite model is found, that computation is lower priority than finding new uniform machinery.

(a) The positive side stalls at a concrete closure problem. Greedy colour-by-colour embedding handles every forest attachment, but for $C_6$ the sixth prescribed colour must close a five-edge rainbow path. Per-colour regularity gives the needed local neighbours but no correlation between the two endpoints. For $2K_3$, Theorem A forces many rainbow triangles but does not by itself force two vertex-disjoint triangles with complementary colour triples. These are the precise missing lemmas; neither follows from the wedge counts.

PARTIAL: Proved an exact rainbow-triangle identity and sharp t=2 minimum, proved problem 811 positive for forests and graphs with 2-core K3, proved lexicographic amplification always fails for C6, and reduced lex-amplifiable 2K3 counterexamples to a finite complement-free triangle-palette base; the full classification remains open.