Certified Depth–Width Frontiers for Reversible SELECT Circuits: Exact four-target curves, an all-width eight-target lower bound, and DRAT-certified boundary instances

Abstract

We determine the complete fixed-width depth curve of the four-target one-hot selector SELECT_X in a fully declared classical-reversible model: gate set {X, CNOT, Toffoli}, pairwise-disjoint-support layers, all-to-all connectivity, dirty data targets, and clean ancillae restored to zero. The curve is D∗_SELECT(4,Q) = infinity for Q < 6; 5 for Q = 6; and 4 for Q >= 7. The two finite values are exact by exhaustive meet-in-the-middle; the all-width statement rests on a lossless normal-form reduction of every depth-3 clean-ancilla circuit to an independently certified finite core. A causal argument gives D∗(2^k,Q) >= k+1 for every k and every width. We then prove a conditional parametric saturation obstruction: if the width-free k-layer frontier contains at most 2^(k-1) carriers of the top address monomial but fewer than 2^(k-1) distinct minterms, then D∗(2^k,Q) >= k+2 at every width. For k = 3, independent Python and C++ exhaustions produce byte-identical complete frontiers (57 and 18,215 canonical states) and establish the hypotheses, yielding the all-width theorem D∗(8,Q) >= 5 for every Q >= 11. An explicit four-layer construction gives C_4(4) >= 10 > 8, so this sufficient criterion does not induct to k = 4. The prospective k+2 law therefore remains open and requires a different lower-bound invariant. If workspace may be left dirty, pure-encoding UNSAT certificates at widths 10 and 11, together with a verified width-12 construction, show that the smallest width at which four-target selection reaches depth 3 is exactly 12; for every Q >= 12, workspace restoration costs exactly one layer at the same width. For ancilla-free dirty-target fan-out we compute the exact depths through seven targets and prove that 2^d - 1 targets require depth at least d+1, above the causal floor. At minimum width the threshold values are 2, 4, 4 for m = 2, 3, 4, and a pure-encoding DRAT certificate gives D∗_THR(5) >= 5; the nonlinear payload has exact depth D∗_carry(6) = 6. The decisive UNSAT formulas and proofs are fixed by SHA-256 and accepted by an independently compiled proof checker; constructions are verified symbolically or exhaustively. We make no priority claim: a systematic novelty search is incomplete, and no result is asserted as first or novel. This record is version 3 of the Zenodo preprint. Earlier versions remain permanently citable through their version-specific DOIs. Version 3 extends version 2 with: the exact closure of the arithmetic-payload depth (D∗_carry(6) = 6, DRAT-certified, and carry(7) in {5,6}); the DRAT-certified threshold bound D∗_THR(5) >= 5; the completed garbage-width curve (minimum width for depth 3 exactly 12, via pure-encoding DRAT exclusions at widths 10 and 11); the all-width eight-target lower bound D∗(8,Q) >= 5 for every valid width, via a conditional parametric saturation argument and independent, byte-identical Python and C++ enumerations of the width-free k=3 frontier; an explicit witness showing the k=3 carrier criterion does not induct to k=4; and restricted (architecture-specific) depth-5 exclusions, explicitly not claimed as general impossibilities. The general depth-5 question at L=8 and the prospective all-k law remain open; the latter appears only as a conjecture. The large DRAT certificate archive is being prepared as a separate, DOI-linked Zenodo dataset.