A different rung of the same ladder: two four-color theorems are now kernel-checked — the known 4-regular case, re-proved by a new argument, and a new unconditional theorem for graphs with at most two degree-3 vertices — to our knowledge the first bound of four to reach into the mixed degree-{3,4} class. The general mixed case, with any number of degree-3 vertices, remains one descent lemma from completion.

The mixed degree-{3,4} target

The target R4_three_four is Maj′(G) ≤ 4 for every finite simple graph whose degrees all lie in {3,4}. Its genuinely new mathematical ground is exactly the mixed class — graphs carrying both a degree-3 and a degree-4 vertex. The best previously published general bound there is Maj′(G) ≤ 5, by Theorem 2 of Antoniuk–Prorok–Salia, arXiv:2607.00212; to our knowledge, closing the descent core would give the first bound of 4 for the whole class, a 5 → 4 improvement.

The pure sub-cases were already published. Cubic graphs satisfy the four-color bound by KKPW Proposition 15 and independently by APS Theorem 4; 4-regular graphs satisfy it by KKPW Proposition 21. The mixed class lies outside those hypotheses: degree 4 is not divisible by 3, degree 3 is odd, and APS Theorem 4 excludes degree-4 vertices.

Strong majority edge-coloring is a 2026 pen-and-paper concept, and apart from this program's own five-color verification, we know of no Lean or mathlib formalization of Maj′ or Conjecture 14. The theorems on this page are, to our knowledge, the first machine-checked strong-majority bounds of four; where the underlying mathematics was already published, we say so and claim only the formalization.

The round-13 gate recorded 105 declarations in the supporting inventory. Its sorry-free declarations were axiom-audited over Maj5Base and mathlib 8f9d9cff; no report exceeded [propext, Classical.choice, Quot.sound].

Since first publication of this article, part of the gap has closed. The theorem R4_three_four_t2 is kernel-complete and unconditional: every finite simple graph with all degrees in {3,4} and at most two degree-3 vertices satisfies Maj′(G) ≤ 4. Graphs with exactly two degree-3 vertices are mixed, so to our knowledge this is the first four-color theorem covering any part of the mixed class; for those graphs the best published bound was 5. Its proof bypasses the descent core: a migration argument shows some minimal split has clean placements everywhere, and the rest is the proved calculus below. The scope is a slice, not the class: for graphs with four or more degree-3 vertices R4_three_four still rests on the open combinatorial lemma strict_descent_of_no_clean_transversal, consumed only in the degree-3 regime, and the full KKPW Conjecture 14 remains open. Also kernel-complete is the 4-regular case credited above, as a re-proof.

The 4-regular re-proof

The 4-regular mathematics is already Proposition 21 of KKPW, not a new theorem here. The artifact's re-proof is unconditional and kernel-complete; its contribution is formalization and a different proof.

KKPW's one-paragraph proof uses an Euler-tour coloring; the artifact instead uses a capacitated-Hall avoidance argument. Every vertex of a 4-regular graph is clean, so every cross edge at that vertex has cap 3. The core Avoid.avoidance_core, implemented through Finset.all_card_le_biUnion_card_iff_existsInjective', selects one vertex from each odd cycle without selecting every vertex of any odd cross-cycle.

Falsification as method

The route did not begin with the construction that survived. An automated-prover pilot found the edge potential ePot, a sum of squared local color counts, and returned a ten-declaration sorry-free scaffold around it. The candidate was gated in a fresh pinned build, then killed by the program's own falsification: degrees-{3,4} graphs have global ePot minimizers that violate strong majority.

The decisive family-F witness has seven vertices and thirteen edges. An independent exhaustive search through all 4¹³ colorings found 312 global minimizers, 96 of them not strong-majority. Separate seven-vertex witnesses and an independent recomputation reached the same verdict. Global minimality already makes every recoloring non-improving, so enlarging the local stationarity radius cannot repair the potential.

Random hardening was not enough. P2″ passed 317 random graphs before the chained-K₅−e construction refuted it at order 10. Adversarial construction, not sample size alone, became a gate before further formalization spend.

The corrections also had higher order. A report that the q = 1 witness blocked the wider Scheme B was itself refuted by a two-edge strict exchange at that witness. An automated return asserted “0 counterexamples, exhaustive” twice in one response; independent recomputation found the counterexamples and is mandatory before such narrative claims can be used. Conversely, ePot_recolor_diff, once flagged false from a truncated quotation, matched the exact pinned formula in 4,440/4,440 tests, and a false negative about defectSafe_iff_crossSafe was settled in favor of the statement by the kernel. These are witness- or kernel-backed corrections, not narrative judgments.

Before publication, the same claims gate corrected an over-strong “new theorem” headline for the regular cases in the article's own marketing.

The toolkit

The campaign used a transplant gate. Statements went to provers as pins containing sorry; only sorry-free content was transplanted into the current architecture. Acceptance required a fresh rebuild, per-declaration #print axioms, and a token-diff of the statement. A return summary alone had no evidentiary standing.

Two unarmed attempts at the crux stopped at the same missing infrastructure. Before striking again, the program assembled the min-alternating realizability toolbox — more than twenty declarations, including exists_isMinAlternating — and the descent surgery engine. The realizability theorem permits any defect set choosing one vertex per odd cycle, with arbitrary signs, turning the remaining crux into pure placement combinatorics.

A complexity fence fixed the form of that last problem. Leven–Galil proved that deciding even-2-factorization of 4-regular graphs is NP-complete; a clean local characterization of ω-minimality is therefore unavailable here. The witness-seeded descent formulation is architecturally forced, not a stylistic preference.

Load-bearing steps were confirmed independently: E1_split and the minimal-split existence theorem each have two proofs; both directions of the class-I equivalence have independent derivations; strongMajority_of_crossSafe_split has three proofs; the clean-transversal bridge has two. The surrounding edge-coloring infrastructure was built while mathlib's edge-coloring API was still under development in mathlib4#33313.

Open: the descent core

The remaining lemma, strict_descent_of_no_clean_transversal, says the following in plain language. If a split of a connected, class-II, degrees-{3,4} graph admits no clean transversal, then another split exists with strictly smaller total odd-cycle count. A clean transversal chooses one cap-3-clean vertex from each odd cycle in one half without containing an odd cycle of the cross half in full.

To our knowledge, no known theorem implies either this descent lemma or the clean-transversal lemma. The STRIKE-B search covered Euler partitions; equitable and evenly-equitable edge colorings after de Werra, Hilton, and Erzurumluoğlu–Rodger; oddness of cubic graphs after Huck–Kochol and Steffen; even 2-factorizations and even cycle decompositions after Markström; and compatible Euler tours after Kotzig, Fleischner, and Sabidussi.

The missing statement is best viewed as a parity-controlled compatible-rerouting theorem at the boundary of the cycle-double-cover circle. Closing it would finish R4_three_four in general; the at-most-two-degree-3-vertices case no longer waits on it.

Artifacts