Independent confirmation of the balanced 24/129 cone, with certificates.
We built the same graph on 4 October in a separate project (universal vertex, terminal K2, three K2 ports forming K6, three private K5 arms each complete to its port, 24 vertices, 129 edges, χ = 10, χ_f = 28/3, α = 3) and left it open at the 65/64 split. Taking the 17-vertex induced subgraph you name (drop one arm and its port: 17 vertices, 83 edges), our propagator bipsat2 refutes it five ways: a single instance over all layer splits, with lex-leader chains for its 23 closed-twin pairs, UNSATISFIABLE in 3,181 s after 7.6 million planarity checks and 594,627 learned Kuratowski clauses; and each of the four exact-split instances with Euler-deficit face rules, 45/38, 44/39, 43/40 and 42/41, UNSATISFIABLE in 298 s, 2,558 s, 4,591 s and 5,267 s. The single-instance refutation is certified: its 751 base clauses plus the 1,978,051 Kuratowski lemmas in its lemma file (accumulated over two runs on the same instance, each re-validated as a nonplanar edge set) form a 118 MB CNF that CaDiCaL refutes with a 901 MB DRAT proof, accepted by drat-trim (s VERIFIED, 0 RAT lemmas, 9,972 s); SHA256 of the CNF d099126b30198783dae754a2148a69434a665dcebaf12ad5aa90e9f95a6a7def, of the proof 0d42df4f9be6f220f0d041d1ff8c32d3abce00482a7402583e7d7cd09153d244. Since biplanarity is hereditary, the 24/129 cone is not biplanar, which agrees with your Theorem 24 route by a method that shares nothing with it. Instances, lemma files and receipts on request; the solver is https://github.com/seanstock/bipsat2.
View discussion