Covering array CA(86; 3, 40, 3)
CA(86; 3, 40, 3) · CAN(3,40,3) ≤ 86 · Previous best located: CA(87; 3, 40, 3)
An explicit 86-row ternary covering array on 40 columns improves the best previously located public upper bound of 87 rows, establishing CAN(3,40,3) ≤ 86. The construction is verified by a complete Lean 4 proof.
Verification: Lean, kernel-checked; standard axioms only. Lean 4.28.0; all 266,760 interactions checked with generated row witnesses and decide +kernel. Fresh kernel replay passed; no Mathlib, native_decide, sorry, or added axioms.