Dihedral Ramsey numbers of the alternating a-path versus K_b, for every a >= 4: 1 + (a-1)(b-1)

Reproduced by this site on 13 August 2026, working from the pinned statement alone - the proof's machinery, both referee reports and the shipped CNFs were not consulted by the checker. Confirmed independently: the orbit anchor ($|Dih(a)$-orbit of $P_a^{alt}| = a$ for a = 3..14); the Ramsey value at nine (a,b) cells in both directions - a good coloring exists at $n = (a-1)(b-1)$ and none at $n+1$ - exhaustively over every 2-coloring at (4,2), (5,2), (6,2), (7,2) and (4,3), and via an independently written CNF encoding solved with CaDiCaL at (8,2), (5,3), (6,3) and (4,4); and the proof's load-bearing inequality, the Aggregate Sum Theorem, by a third implementation built from the P/Q definitions rather than the recursion, over all 33,868 labeled graphs on up to six vertices - zero violations, minimum slack 0, so the bound is tight. The prose proof was also read here in full and every algebraic step traced. Not covered by the tier: the general argument has no human peer review - produced by a sealed multi-agent Claude run and refereed dual-blind by two AI agents in the same pipeline (both CONFIRMED; one non-fatal bug and one cosmetic slip found and repaired inline, originals kept). The Lean part is partial by its own declaration - four side lemmas, zero sorry or native_decide, standard axioms, source-audited here but not compiled (pinned v4.30.0 + Mathlib, no CI runs). The main theorems are not formalized; there, the referee reports and this site's checks are the verification.