The Unit Gap Is Base-Dependent: A Mechanically Verified Refutation and a Cross-Base Census

The gap between a Boolean function's minimum formula size (fan-out one) and its minimum circuit size is base-dependent; in particular, the number of variables at which it first exceeds one gate depends on the basis. In the And-Inverter Graph (AIG) basis it does so already at n=3 and reaches 6 at n=4; in the XOR-AND-graph (XAG) basis it stays within one gate through n=4 (a solver-gated census whose UNSAT side is not proof-certified) and first exceeds it at n=5. In AIG this refutes Theorem 2 of Krinkin (The Unit Gap, arXiv:2603.08033v2; since withdrawn), that the gap is 0 or 1 for every Boolean function, and his Corollary 6, bounding a shared-gate term s in {0,1}. The parity of three variables is a counterexample: opt=6 (UNSAT for k=1..5 gates, each certified by a DRAT proof checked with drat-trim) and formula size 9, so the gap is 3 and Krinkin's own s=3. The refutation is classical: the AIG basis with free inversions is U_2, where parity_n has circuit complexity exactly 3n-3 (Schnorr; Jukna), and Khrapchenko forces at least 9 leaves, so gap >= 2 follows from two published results and that identification, with no computation of ours. The error is locatable: Sections 2 and 3 of that paper give incompatible characterizations of formula size. An exhaustive census of the 222 NPN classes of n=4 (solver-gated; its UNSAT side is not DRAT-certified) gives 72 classes with gap >= 2 and maximum 6, attained by three classes, one of them parity-4. In XAG, the five-variable function 0x00063357 has opt=6 and formula size 8 (by a simulated circuit, SAT without DRAT, and a dynamic program); joining two public per-class tables for all 616,126 NPN classes of n=5 (Lee, Jiang, Mishchenko and Brayton, IWLS 2019; Knuth's optimal circuits as distributed in A. P. Goucher's optimal5) gives XAG gaps up to 3, with 6,828 classes at gap >= 2, resting on the optimality of the two sources.