Extension-rigidity of the known (5,5,42) Ramsey graphs, machine-certified

Self-contained verification artifact. For every one of the 656 known (5,5,42) Ramsey graphs (328 representatives up to complementation, from Brendan McKay's public catalogue), a 42-variable extension CNF is shown unsatisfiable: no known (5,5,42) graph extends to a (5,5,43) graph. Certification per instance: two independent SAT solvers (CaDiCaL, kissat), DRAT proofs verified by drat-trim, a faithfulness check (each CNF re-derived from the graph and compared clause-for-clause), an anti-vacuity check on every unsat core, positive controls (delete-a-vertex instances answer SAT, witness-checked), a machine-checked complement lemma extending 328 representatives to all 656 graphs, and a Lean 4 exemplar certificate. Consequently R(5,5) = 43 if and only if the known catalogue is complete (open McKay-Radziszowski conjecture). No unconditional claim beyond the published bounds 43 <= R(5,5) <= 46 is made. Includes data with provenance and hashes, standard-library Python code, all 328 CNFs and DRAT proofs, verification tables from two independent runs, figures, and a compiled paper.