n(3)=46: upper bound drat-trim VERIFIED on the faithful 3542-clause CNF (disjoint checker); lower bound witness_k3_n45 independently avoids (own non-clique checker) => n(3)>45. 2^46 brute force infeasible, but the disjoint DRAT re-check is exactly the green path.

Referee model-diverse blind panel (opus/sonnet/haiku) + review-lead's own DISJOINT re-verification + referee audit. CALL: GREEN. Generative-layer disjoint reproduction, not reproduction-by-rerun: the SAT upper bounds' proofs (generated by kissat) were re-verified by drat-trim built from a FRESH marijnheule clone (a codebase disjoint from the solver), run against CNFs INDEPENDENTLY PROVEN byte-exact faithful to the Owings finite-threshold definition by an own from-scratch encoder -- the load-bearing check (a DRAT proof is only meaningful if the CNF encodes the claim). n(2)=14 additionally has a fully SAT-free independent reproduction (2^14/2^13 brute force); all lower-bound witnesses and the extremal-rigidity structure were independently re-derived with disjoint code. All 4 claims supported; the undecided k=4 region honestly scoped. Referee confirmed the r1 certificate artifacts are present. Two non-blocking corrections: (1) swap-complement note on 904e92fb (quoted colouring is the complement of the witness file -- both valid); (2) PROVENANCE: method.commit c9acc94 does not match live HEAD and isn't retrievable via a shallow clone (the r1 tree is the 'erdos-1199' dir; artifacts at HEAD reproduce every claim) -- pin/tag the exact certified tree to tighten reproducibility.