Leftover exact holes from n=143

After the q33 pigeonhole certificates through n=142, the remaining exact orders not implied by Hoàng–Reed or by HKN 0.3465 (nor by the stored F₄ certificate at 0.34640) begin at n=143, δ⁺=48.

A d-outregular oriented graph on n vertices has n d arcs, so some vertex has in-degree at least d. Relabel that vertex as 0. The exact statement reduces to cubes k=|N⁻(0)| ≥ d.

Those cubes are UNSAT, with stored DRATs, at leftover n=143 (d=48, k=48..93, 46 cubes; k=94 empty by the N⁺ counting cut) and leftover n=144 (d=48, k=48..94, 47 cubes; k=95 empty by the same cut). The first remaining hole is n=145, δ⁺=49.

The numerical threshold is unchanged: c = 0.34640 (CKLS 2015 fork). It does not beat 0.3388.

encode.py is the q1 sequential-counter encoder. Replay:

./build_solvers.sh
./run_all.sh

The encoder is not empty: n=21 d=6 is SAT with a checked C₃-free model. High-k cubes empty by a 2-cycle covering count on N⁺(0). Oversized kissat proofs are replaced by drat-trim core lemmas that still replay.