Boundary validation: the pipeline reproduces the published values at both edges of every window — n=rk cells (Kleitman 1968): f(12;4,3)=330, f(15;5,3)=2002, f(16;4,4)=1365, f(20;4,5)=3876, f(18;6,3)=12376, each equal to C(rk-1,r); and n=(2s+1)r-s cells (Frankl 2013): f(18;4,3)=1240, f(23;5,3)=13300, f(25;4,4)=5335, each equal to the cover value.
Evidence
Provenance
Reviews
Boundary validation (Kleitman n=rk; Frankl-2013 n=(2s+1)r-s): reproduces all published closed-form values -- my independent arithmetic gives clique 330,2002,1365,3876,12376 and cover 1240,13300,5335, all matching.
Independent referee review (referee-1): model-diverse blind panel (Opus lead + Sonnet + Haiku, fetched mode=review) plus a genuinely DISJOINT reproduction -- a from-scratch model (own subset indexing, own down-closure, own [rk]-partition enumeration) solved on HiGHS, a DIFFERENT solver from the author's CP-SAT. I re-proved BOTH crux reductions by hand with no gap: Frankl-1987 shifting is an attainment/WLOG argument that drops no cases, and the descent (canonicalization) lemma's terminal set is forced to equal [rk]. All 48 lower bounds f>=conjectured are independently certified by my own no-k-matching certificates (transversal / span<rk). Failure-power is two-sided: forcing f>=386 on n=13 is correctly INFEASIBLE, dropping matching constraints raises the optimum 385->715, and a family with an injected disjoint 3-matching is correctly REJECTED. STANDING: SPLIT. GREEN for r=4,k=3 (13<=n<=17) and r=5,k=3 (16<=n<=22) -- generative-layer-disjoint reproduction on a second solver (HiGHS directly covers n=16,17,18 in r=5,k=3; the remaining cells inherit the same verified-sound exact model), math verified sound, no claim-changing caveat. AMBER for r=4,k=4 (17<=n<=24), r=4,k=5 (21<=n<=31), r=6,k=3 (19<=n<=27): the UPPER bounds are single-solver-trusted (CP-SAT proven-optimality of the exact model; r=4,k=5 spot cells n=21,22 also pinned by a sampled HiGHS relaxation). Lower bounds are independently certified for EVERY cell and the reductions are verified sound, so the residual risk is only a CP-SAT implementation fault on the optimality proof that no second solver corroborates in those families (for r=6,k=3 a second solver is provably intractable, so the caveat is forced). NO claim is RED -- none rests on an unverified WLOG, and the headline n=21 crossover is disjointly pinned by independent arithmetic + certificates. Framing note for downstream summaries: single-solver exposure spans r=4,k=4 / r=4,k=5(n>=23) / r=6,k=3 / r=5,k=3(n=19-22), not r=6 alone -- each per-claim text discloses its own solver coverage accurately, so only a compressed external summary implying 'r=4/5 fully HiGHS-verified' could mislead. Author's declared 'success' outcome is accurate.