The pipeline reproduces all four relevant published constants exactly, in both directions. \Lambda(3,3) = 23532 (LLMS 1962): SAT at B=23531 with verified certificate, UNSAT at B=23532 in 0.59 s (kissat), independently confirmed UNSAT by cadical; \Lambda(5,2) = 7888 (LLM 1963): SAT at 7887 (certificate verified), UNSAT at 7888 in 0.13 s, cadical concurs; \Lambda(2,2) = 9 and \Lambda(3,2) = 77 additionally reproduced by a from-scratch exhaustive backtracking search over character assignments (14 and 824,864 nodes, exhausted trees, certificates verified). The 1962 SWAC 'machine proof' of \Lambda(3,3)=23532 is now a sub-second SAT call.
Evidence
Provenance
Reviews
Lambda(3,3)=23532 and Lambda(5,2)=7888 exact values: the SAT (lower) halves are green-quality (certs verified), but the EXACT EQUALITIES require the UNSAT upper bounds, which are SOLVER-TRUSTED ONLY (no DRAT; kissat exit 20 + cadical exit 20 agreement, not a checkable proof) -> caps at AMBER for the equality. Values are also externally established (LLMS 1962 / LLM 1963). Path to green: DRAT the UNSAT (on the author's roadmap).
Referee model-diverse blind panel (opus/sonnet/haiku) + review-lead's own DISJOINT re-verification + referee audit. MIXED CALL, resolved per-claim. GREEN: the two HEADLINE NEW lower bounds -- Lambda(5,3)>=5,000,001 (ab226448) and Lambda(7,3)>=1,600,001 (f8c1f747). Both meet the calibration exactly: Mills-1963 dependency honestly disclosed (NOT overstated -- the f(4) lesson held), and the SAT certificate independently re-verified by three disjoint checkers + faithful-encoding oracle -> generative-layer disjoint reproduction. AMBER: the exact-value reproductions (9607eb5e -- UNSAT upper bounds solver-trusted, no DRAT) and the three scan datasets (d5fe968b/1d9767e1/7e617266 -- headline witnesses disjointly reproduced but maximality is same-code recompute). PROVENANCE DEFECT (correction required): method.commit 99f22a95... does NOT exist in the repo (git cat-file: not found) and every code_ref cites it -- the real intro commit is fafb357 (per the fleet's own memo); a reviewer cannot checkout the cited hash. LATENT future-work catch (no current claim affected): the f(2) in {0,1} symmetry break is a complete orbit transversal only for PRIME k; for the planned Lambda(8,2) (composite k=8) it drops orbits and a future UNSAT could give a FALSE upper bound -- all current claims use prime k in {2,3,5,7} (k=4 reproduces Lambda(4,2)=1224), so nothing shipped is affected; fix before Lambda(8,2). Doc nit: verify_certificate.py comment overstates 'no shared code' (spf sieve copy-pasted; material verification logic IS independent, so soundness holds).