pith. sign in

arxiv: 2604.23958 · v1 · submitted 2026-04-27 · 💻 cs.CC

Constructive Separations from Gate Elimination

Marco Carmosino , Ngu Dang , Tim Jackman This is my paper

Pith reviewed 2026-05-07 17:25 UTC · model grok-4.3

classification 💻 cs.CC
keywords gate eliminationcircuit lower boundsconstructive refutersXOR functionaffine dispersersDeMorgan circuitscomplexity separations
0
0 comments X

The pith

Gate elimination lower bound proofs can be turned into efficient algorithms that find counterexamples for circuits too small to compute functions like XOR and affine dispersers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that standard gate elimination arguments for proving circuit size lower bounds are already constructive: each elimination step either shrinks the circuit or exposes a structural or functional violation that directly yields an input where the circuit errs. This holds for elementary bounds on XOR and the multiplexer as well as the more involved 3.1n-o(n) bound for affine dispersers. A reader would care because Chen, Jin, Santhanam, and Williams highlighted constructivity as central to several long-standing open problems in complexity theory. The authors achieve the result by treating the elimination process itself as the refuter algorithm rather than a purely existential argument.

Core claim

Gate elimination arguments yield refuters—efficient algorithms that, when given a circuit too small to compute a function f, produce an input on which the circuit errs. This covers elementary lower bounds for XOR and the multiplexer as well as sophisticated arguments for affine dispersers. The perspective shift treats each gate elimination step as either simplifying the circuit or revealing a violation from which an explicit counterexample can be extracted. The XOR result is strengthened to handle circuits that exactly match the 3(n-1) lower bound size.

What carries the argument

Gate elimination process reinterpreted as a refuter algorithm, where each step simplifies the circuit or exposes a structural or functional violation allowing efficient extraction of a counterexample input.

If this is right

  • Any gate elimination lower bound for affine dispersers immediately supplies a polynomial-time refuter for circuits smaller than 3.1n-o(n).
  • The XOR refuter works even against circuits that achieve the exact optimal size 3(n-1).
  • The multiplexer and other elementary functions with gate elimination proofs now come with explicit refuting algorithms.
  • Constructivity follows from the elimination steps themselves without needing extra properties of the target function.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same re-interpretation might turn other non-constructive lower bound techniques into refuters once their steps are examined for extractable violations.
  • Characterizing the optimal circuits for a function appears necessary to reach the matching-size case, limiting immediate extension beyond XOR.
  • Implementing the refuters for small n would give concrete test cases for whether the extracted counterexamples match known hard instances for those functions.

Load-bearing premise

Every gate elimination step either reduces the circuit while preserving the lower bound property or directly supplies an efficiently computable violation that yields a concrete error input.

What would settle it

A DeMorgan circuit of size at most 3(n-1) for XOR_n on which the claimed refuter outputs no input where the circuit errs, or outputs an input where the circuit actually computes the correct value.

Figures

Figures reproduced from arXiv: 2604.23958 by Marco Carmosino, Ngu Dang, Tim Jackman.

Figure 1
Figure 1. Figure 1: While simplifying, gate elimination arguments track certain complexity measures; view at source ↗
read the original abstract

Gate elimination is the primary technique for proving explicit lower bounds against general Boolean circuits, including Li and Yang's state-of-the-art $3.1n - o(n)$ bound for affine dispersers (STOC 2022). Every circuit lower bound is implicitly existential: every circuit that is too small to compute $f$ must err on some input. This raises a natural question: are these lower bounds \emph{constructive}? That is, can we efficiently produce such errors? Chen, Jin, Santhanam, and Williams showed that constructivity plays a central role in many longstanding open problems in complexity theory, and explicitly raised the question of which circuit lower bound techniques can be made constructive (FOCS 2021). We show that a variety of gate elimination arguments yield refuters -- efficient algorithms that, when given a circuit that is too small to compute a function $f$, produce an input on which the circuit errs. Our results range from elementary lower bounds for $XOR$ and the multiplexer to more sophisticated arguments for affine dispersers. Underlying these results is a shift in perspective: gate elimination arguments \emph{are} algorithms. Each step either simplifies the circuit or reveals a violation of some structural or functional property, from which, with a little additional work, explicit counterexamples can be extracted. We further strengthen the $XOR$ result to handle circuits that \emph{match} the lower bound: given any DeMorgan circuit of size $3(n-1)$ that fails to compute $XOR_n$, we can efficiently produce a counterexample. While refuters follow from the gate elimination arguments themselves, this refinement requires a complete characterization of the set of optimal circuits computing $XOR$ -- a requirement rarely met by other explicit functions.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 3 minor

Summary. The paper shows that gate-elimination arguments for explicit circuit lower bounds can be reframed as constructive refuters: efficient algorithms that, given a circuit smaller than the lower bound for a function f (such as XOR_n, the multiplexer, or affine dispersers), output an input on which the circuit errs. The results cover elementary cases directly via circuit scanning and extend to the Li-Yang 3.1n-o(n) affine-disperser bound via supplied extraction routines; the XOR result is strengthened to size-exact circuits of 3(n-1) gates via an explicit characterization of all optimal DeMorgan circuits.

Significance. If the claimed extraction procedures are polynomial-time and the XOR characterization is fully explicit, this work is significant for reframing gate elimination as an algorithmic process rather than a purely existential proof technique. It directly addresses the constructivity questions raised by Chen, Jin, Santhanam, and Williams (FOCS 2021) and supplies concrete refuters even for the current state-of-the-art affine-disperser bound. The tight-bound strengthening for XOR, which requires a complete structural characterization, is a notable technical achievement rarely achieved for explicit functions.

major comments (2)
  1. [Affine disperser argument] In the affine-disperser section, the extraction routine that produces a counterexample from a violating affine subspace (or constant gate) must be shown to run in time polynomial in the circuit size; the high-level description leaves open whether the subspace search or substitution steps introduce superlinear overhead that would undermine the refuter efficiency claim.
  2. [XOR strengthening] For the strengthened XOR result, the complete characterization of all size-3(n-1) optimal circuits is load-bearing for the size-exact refuter; the manuscript should state the characterization explicitly (as a lemma or theorem) and confirm that it permits an efficient (poly-time) procedure to locate an error without enumerating an exponential number of circuits.
minor comments (3)
  1. [Abstract] The abstract's phrasing 'with a little additional work' is informal; the main text should replace it with a precise accounting of the extra steps and their complexity.
  2. [Elementary cases] Figure or pseudocode illustrating the extraction procedure for the elementary XOR/multiplexer cases would improve readability and make the 'gate elimination as algorithm' perspective more concrete.
  3. [Conclusion] The paper should include a short discussion of whether the same constructive perspective applies to other gate-elimination proofs beyond the three treated here.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive assessment, the recommendation of minor revision, and the constructive comments that help strengthen the clarity of our constructivity results. We address each major comment below.

read point-by-point responses

  1. Referee: [Affine disperser argument] In the affine-disperser section, the extraction routine that produces a counterexample from a violating affine subspace (or constant gate) must be shown to run in time polynomial in the circuit size; the high-level description leaves open whether the subspace search or substitution steps introduce superlinear overhead that would undermine the refuter efficiency claim.

    Authors: We thank the referee for highlighting this point. The extraction routines are supplied in the manuscript and are designed to be efficient: given a violating affine subspace (specified by a basis of dimension at most n), we locate a counterexample by evaluating the circuit on a linear number of points derived from the basis vectors or by solving a small system of linear equations over GF(2) via Gaussian elimination. Each circuit evaluation is linear in the circuit size, and the overall procedure is O(n^3) in the worst case, which is polynomial in the input size (the circuit). Substitution for constant gates is likewise linear. In the revised manuscript we will add a dedicated subsection with a formal runtime analysis proving the polynomial bound. revision: yes

  2. Referee: [XOR strengthening] For the strengthened XOR result, the complete characterization of all size-3(n-1) optimal circuits is load-bearing for the size-exact refuter; the manuscript should state the characterization explicitly (as a lemma or theorem) and confirm that it permits an efficient (poly-time) procedure to locate an error without enumerating an exponential number of circuits.

    Authors: We agree that an explicit statement improves readability. The manuscript already derives a complete structural characterization of all DeMorgan circuits of size exactly 3(n-1) that compute XOR_n: every such circuit must consist of a specific recursive pattern of 3-gate blocks, each computing a partial XOR on a subset of variables with no redundant gates. We will extract this characterization as a standalone lemma (Lemma 4.3) in the revision. The lemma directly yields a polynomial-time refuter: given any circuit of size 3(n-1), we perform a single linear-time scan of its gates to verify the required structure; any deviation immediately identifies a local error pattern whose witnessing input can be computed in O(n) time by propagating the mismatch. No enumeration of circuits is required. revision: yes

Circularity Check

0 steps flagged

No significant circularity; refuters are direct algorithmic lifts of gate-elimination steps

full rationale

The derivation reinterprets each gate-elimination step as either a size-reducing simplification or an explicit structural/functional violation (e.g., constant-input gates or affine subspaces) from which a counterexample is extracted by direct evaluation or substitution. This holds for the elementary XOR/multiplexer cases by circuit scanning and for the Li-Yang affine-disperser case via supplied extraction routines. The XOR strengthening uses an explicit finite enumeration of size-3(n-1) optimal circuits, which is a verifiable computation rather than a self-referential fit or imported uniqueness theorem. No self-definitional equations, fitted-input predictions, load-bearing self-citations, or ansatz smuggling appear; the central claim remains independent of the target result.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on standard Boolean-circuit definitions and the gate-elimination technique from prior literature; no new free parameters or invented entities are introduced.

axioms (2)
  • standard math DeMorgan circuits and standard notions of circuit size and computation
    Used to define the lower-bound statements and the notion of a refuter.
  • domain assumption Gate-elimination steps preserve or reveal structural properties that allow counterexample extraction
    This is the key modeling assumption that turns the proof into an algorithm.

pith-pipeline@v0.9.0 · 5619 in / 1274 out tokens · 67222 ms · 2026-05-07T17:25:28.834340+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

16 extracted references · 11 canonical work pages

  1. [1]

    Designing programs that check their work.Journal of the ACM (JACM), 42(1):269–291, January 1995.doi:10.1145/200836.200880

    1 Manuel Blum and Sampath Kannan. Designing programs that check their work.Journal of the ACM (JACM), 42(1):269–291, January 1995.doi:10.1145/200836.200880. 2 Norbert Blum. A boolean function requiring 3n network size.Theor. Comput. Sci., 28:337–345, 1984.doi:10.1016/0304-3975(83)90029-4. 3 Marco Carmosino, Ngu Dang, and Tim Jackman. Simple Circuit Extens...

    work page doi:10.1145/200836.200880 1995

  2. [2]

    URL:https: //drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.23, doi:10.4230/ LIPIcs.STACS.2026.23

    Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL:https: //drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.23, doi:10.4230/ LIPIcs.STACS.2026.23. 4 Lijie Chen, Ce Jin, Rahul Santhanam, and Ryan Williams. Constructive separations and their consequences.TheoretiCS, 3,

    work page doi:10.4230/lipics.stacs.2026.23 2026

  3. [3]

    5 Evgeny Demenkov and Alexander S

    URL: https://doi.org/10.46298/theoretics.24.3, doi:10.46298/THEORETICS.24.3. 5 Evgeny Demenkov and Alexander S. Kulikov. An elementary proof of a 3n - o(n) lower bound on the circuit complexity of affine dispersers. In Filip Murlak and Piotr Sankowski, editors, Mathematical Foundations of Computer Science 2011 - 36th International Symposium, MFCS 2011, Wa...

    work page doi:10.46298/theoretics.24.3 2011

  4. [4]

    Springer, 2011.doi:10.1007/978-3-642-22993-0\_25

    Proceedings, volume 6907 ofLecture Notes in Computer Science, pages 256–265. Springer, 2011.doi:10.1007/978-3-642-22993-0\_25. 6 Magnus Gausdal Find, Alexander Golovnev, Edward A. Hirsch, and Alexander S. Kulikov. A better-than-3n lower bound for the circuit complexity of an explicit function. In2016 IEEE 57th Annual Symposium on Foundations of Computer S...

    work page doi:10.1007/978-3-642-22993-0 2011

  5. [5]

    7 Alexander Golovnev, Edward A

    doi:10.1109/FOCS.2016.19. 7 Alexander Golovnev, Edward A. Hirsch, Alexander Knop, and Alexander S. Kulikov. On the limits of gate elimination.J. Comput. Syst. Sci., 96:107–119,

    work page doi:10.1109/focs.2016.19 2016

  6. [6]

    8 Stefan Grosser and Marco Carmosino

    URL:https://doi.org/ 10.1016/j.jcss.2018.04.005,doi:10.1016/J.JCSS.2018.04.005. 8 Stefan Grosser and Marco Carmosino. Student-teacher constructive separations and (un)provability in bounded arithmetic: Witnessing the gap. In Michal Koucký and Nikhil Bansal, editors,Proceedings of the 57th Annual ACM Symposium on Theory of Com- puting, STOC 2025, Prague, C...

    work page doi:10.1016/j.jcss.2018.04.005 2018

  7. [7]

    9 Rahul Ilango

    doi:10.1145/3717823.3718216. 9 Rahul Ilango. Constant depth formula and partial function versions of MCSP are hard. SIAM J. Comput., 53(6):S20–317,

    work page doi:10.1145/3717823.3718216

  8. [8]

    10 Stasys Jukna.Boolean Function Complexity - Advances and Frontiers, volume 27 ofAlgorithms and combinatorics

    URL:https://doi.org/10.1137/20m1383562, doi: 10.1137/20M1383562. 10 Stasys Jukna.Boolean Function Complexity - Advances and Frontiers, volume 27 ofAlgorithms and combinatorics. Springer, 2012.doi:10.1007/978-3-642-24508-4. 11 Klein and Paterson. Asymptotically optimal circuit for a storage access function.IEEE Transactions on Computers, 100(8):737–738,

    work page doi:10.1137/20m1383562 2012

  9. [9]

    3.1n-o(n) circuit lower bounds for explicit functions

    12 Jiatu Li and Tianqi Yang. 3.1n-o(n) circuit lower bounds for explicit functions. In Stefano Leonardi and Anupam Gupta, editors,STOC ’22: 54th Annual ACM SIGACT Symposium on Theory of Computing, Rome, Italy, June 20 - 24, 2022, pages 1180–1193. ACM,

    2022

  10. [10]

    13 SA Lozhkin and DE Khzmalyan

    doi:10.1145/3519935.3519976. 13 SA Lozhkin and DE Khzmalyan. The complexity of the standard multiplexer function in a class of switching circuits.Computational Mathematics and Modeling, 32(4):478–489,

    work page doi:10.1145/3519935.3519976

  11. [11]

    15 Wolfgang J Paul

    URL: https://doi.org/10.1016/j.apal.2019.102735, doi:10.1016/J.APAL.2019.102735. 15 Wolfgang J Paul. A 2.5 n-lower bound on the combinational complexity of boolean functions. InProceedings of the seventh annual ACM symposium on Theory of computing, pages 27–36,

    work page doi:10.1016/j.apal.2019.102735 2019

  12. [12]

    trivially

    17 Claus-Peter Schnorr. Zwei lineare untere schranken für die komplexität boolescher funktionen. Computing, 13(2):155–171, 1974.doi:10.1007/BF02246615. CVIT 2016 23:16 Constructive Separations from Gate Elimination A An OptimalXORChecker Refuters find errors for computational models which fallbelowa threshold established from a lower bound. It is natural ...

    work page doi:10.1007/bf02246615 1974

  13. [13]

    In this and the previous branches, the only indices of⃗ athat are changed are inI, and hence the condition that the error agrees with the original⃗ ai on all non-Iinputs is met

    Settingxp as described leavesC to be a constant, but XORI(·)⊕cdoes not become constant. In this and the previous branches, the only indices of⃗ athat are changed are inI, and hence the condition that the error agrees with the original⃗ ai on all non-Iinputs is met. Otherwise, the algorithm in steps 25 - 28 follows the final Work and Inductive Hypothesis s...

    2016

  14. [14]

    We proceed via induction; fixk >2to be the size ofI and presume thatXOR-Checkeris correct on any inputs where|I|=k−1

    In the base case,n = 2, the algorithm brute forces over all four possible inputs andC must err on at least one of them else it computesXOR2. We proceed via induction; fixk >2to be the size ofI and presume thatXOR-Checkeris correct on any inputs where|I|=k−1. CVIT 2016 23:20 Constructive Separations from Gate Elimination Algorithm 4Checker for circuits pur...

    2016

  15. [15]

    For completeness, we show that these algorithms are correct and run in polynomial time. ParitySupport Algorithm 5Identifies the affine function by a circuit of fanout1⊕-type gates Input:C, a normalized circuit of fanout1⊕-type gates Output:I,csuch thatCcomputes ⨁ i∈Ixi⊕c 1: procedureParitySupport(C) 2: I←∅ 3: fori∈[n]do 4: iffanout(x i) is oddthen 5: addi...

    2016

  16. [16]

    Therefore the algorithm correctly outputs the direction matrix and offset for the intersec- tion of the given affine subspaces

    Therefore: u=U⃗ x+⃗ u=U[Iδ|0n−1] ( K⃗ z′+ (⃗ w0 ⃗ z0 )) +⃗ u=UX⃗z′+U⃗ w0 +⃗ u=W⃗ z′+⃗ w. Therefore the algorithm correctly outputs the direction matrix and offset for the intersec- tion of the given affine subspaces. As Gaussian elimination is efficient, the overall algorithm runs in polynomial time with respect tonas desired.◀ ConstraintToAffine Algorith...

    2016