pith. sign in

arxiv: 2605.23805 · v1 · pith:AS4R3LJGnew · submitted 2026-05-22 · 💻 cs.CC

Recursion and proof theoretical characterizations of small circuit classes with modulo counting via discrete differential equations (long version)

Melissa Antonelli , Arnaud Durand , Rui Li This is my paper

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

classification 💻 cs.CC
keywords discrete differential equationsconstant-depth circuitsmodulo countingFAC0implicit complexitybounded theoriesproof theory
0
0 comments X

The pith

Discrete ODE schemas characterize functions computed by constant-depth modulo-n counting circuits for every n

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

The paper develops an implicit complexity approach based on discrete ordinary differential equations to study polynomial-size constant-depth circuits that include gates counting modulo any fixed n. Earlier recursion-based methods had succeeded only for the special cases of modulo 2 and modulo 6. Replacing bounded recursion with ODE schemas produces uniform characterizations of the corresponding function classes FAC0[n] for every natural number n. The authors further construct first-order bounded theories whose provably total functions match each of these classes. A sympathetic reader would care because the syntactic shape of the equations supplies a machine-independent handle on the computational power of these small circuit families.

Core claim

Considering ODE schemas rather than bounded recursion allows for a more fine-grained analysis, leading to (uniform) characterizations for all classes FAC0[n]. Inspired by the syntactic form of the ODE schemas, first-order bounded theories are presented for capturing provably total functions in each of these classes.

What carries the argument

ODE schemas: syntactic forms of discrete ordinary differential equations whose solutions exactly match the functions computed by the circuits with modulo-n gates

Load-bearing premise

The syntactic form of the proposed ODE schemas exactly matches the computational power of polynomial-size constant-depth circuits with modulo-n gates for every n, without hidden uniformity or size assumptions.

What would settle it

Exhibit a function that solves one of the ODE schemas yet lies outside every polynomial-size constant-depth circuit family with modulo-n gates, or exhibit a circuit-computable function that cannot be obtained as the solution of any such schema.

read the original abstract

The paper proposes an implicit (i.e., machine-independent) complexity approach to studying computation by polynomial-size, constant-depth circuits with gates counting modulo a constant through the lens of discrete ordinary differential equations (ODEs). So far, recursion-theoretic characterizations have been provided for functions computed by circuits of constant depth, including gates counting modulo 2 and 6 only (i.e., for the classes FAC0[2] and FAC0[6], resp.). In this paper, it is shown that considering ODE schemas, rather than bounded recursion, allows for a more fine-grained analysis, leading to (uniform) characterizations for all classes FAC0[n] (n \in N), i.e. functions computed by circuits including counting modulo n gates. Inspired by the syntactic form of the ODE schemas, we go further in this direction and present first-order bounded theories for capturing provably total functions in each of these classes.

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 / 1 minor

Summary. The paper proposes an implicit complexity approach using discrete ordinary differential equations (ODEs) to characterize functions computed by uniform polynomial-size constant-depth circuits with modulo-n gates (FAC0[n] for all n in N). It claims that ODE schemas, rather than bounded recursion, enable fine-grained uniform characterizations extending prior results limited to FAC0[2] and FAC0[6], and introduces corresponding first-order bounded theories capturing the provably total functions in each class.

Significance. If the claimed equivalences hold, the work would extend recursion-theoretic and proof-theoretic characterizations to all moduli n, offering a more uniform and machine-independent framework for analyzing these circuit classes. The use of ODE schemas for fine-grained analysis and the development of bounded theories are potential strengths if supported by explicit derivations.

major comments (2)
  1. [Abstract] The abstract asserts that ODE schemas yield characterizations for all FAC0[n], but provides no derivation, proof sketch, or concrete example for any specific n (e.g., n=3). This makes it impossible to verify whether the syntactic restrictions on the difference operator and initial conditions exactly match the power of uniform poly-size constant-depth MOD_n circuits without hidden size or uniformity assumptions.
  2. [Main technical development (ODE schemas)] The central equivalence between the proposed ODE schemas and FAC0[n] is load-bearing; the manuscript must demonstrate (in the main technical sections) that the schemas introduce neither hidden uniformity conditions nor size blow-ups when instantiated for arbitrary fixed n, as any mismatch in the form of the difference operator could under- or over-generate relative to the circuit model.
minor comments (1)
  1. Clarify the precise definition of 'uniform' used for the FAC0[n] characterizations and how it aligns with standard circuit uniformity notions.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for highlighting the need for explicit verification of the central claims. We address each major comment below by pointing to the relevant sections where the required demonstrations are provided.

read point-by-point responses

  1. Referee: [Abstract] The abstract asserts that ODE schemas yield characterizations for all FAC0[n], but provides no derivation, proof sketch, or concrete example for any specific n (e.g., n=3). This makes it impossible to verify whether the syntactic restrictions on the difference operator and initial conditions exactly match the power of uniform poly-size constant-depth MOD_n circuits without hidden size or uniformity assumptions.

    Authors: The abstract is a concise summary. The full derivations, including a concrete running example for n=3 and the precise syntactic restrictions on the difference operator and initial conditions, appear in Sections 3 and 4. These sections contain the inductive proofs establishing equivalence to uniform polynomial-size constant-depth MOD_n circuits, with explicit verification that no hidden size or uniformity assumptions are introduced. revision: no

  2. Referee: [Main technical development (ODE schemas)] The central equivalence between the proposed ODE schemas and FAC0[n] is load-bearing; the manuscript must demonstrate (in the main technical sections) that the schemas introduce neither hidden uniformity conditions nor size blow-ups when instantiated for arbitrary fixed n, as any mismatch in the form of the difference operator could under- or over-generate relative to the circuit model.

    Authors: Sections 3–5 contain the required demonstrations. Theorem 4.2 and its proof establish the equivalence for arbitrary fixed n by showing that the restricted difference operator and initial conditions generate exactly the functions of the target circuit class. The proof proceeds by induction on circuit depth, preserves polynomial size bounds, and matches the standard uniformity conditions of the circuit families without introducing mismatches or blow-ups. revision: no

Circularity Check

0 steps flagged

No circularity: derivation relies on independent syntactic analysis of ODE schemas

full rationale

The abstract and available text present characterizations of FAC0[n] via discrete ODE schemas as a machine-independent approach extending prior recursion-theoretic results for FAC0[2] and FAC0[6]. No self-definitional equations, fitted inputs renamed as predictions, load-bearing self-citations, uniqueness theorems imported from the authors, ansatzes smuggled via citation, or renamings of known results are present. The central claim that ODE schemas yield uniform characterizations for all n is framed as an independent syntactic analysis rather than reducing to the input definitions by construction. The derivation chain is self-contained against external circuit definitions.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract supplies no explicit free parameters, axioms, or invented entities; the ledger is therefore empty.

pith-pipeline@v0.9.0 · 5690 in / 956 out tokens · 20283 ms · 2026-05-25T02:17:41.016892+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

35 extracted references · 35 canonical work pages

  1. [1]

    B. Allen. Arithmetizing uniform NC.Ann. Pure Appl. Log., 53(1):1–50, 1991

    work page 1991

  2. [2]

    Allender and K.W

    E. Allender and K.W. Wagner. Counting hierarchies: polynomial time and constant. Bull. EATCS, 40:182–194, 1990

    work page 1990

  3. [3]

    Antonelli, A

    M. Antonelli, A. Durand, and J. Kontinen. A new characterization of FAC0 via discrete ordinary differential equations. In Rastislav Kr´ alovic and Anton´ ın Kucera, editors, 49th International Symposium on Mathematical Foundations of Computer Science, MFCS 2024, Bratislava, Slovakia, August 26-30, 2024, volume 306 ofLIPIcs, pages 10:1–10:18. Schloss Dagst...

    work page 2024

  4. [4]

    Antonelli, A

    M. Antonelli, A. Durand, and J. Kontinen. Characterizing small circuit classes from FAC0 to FAC1 via discrete ordinary differential equations. In Pawel Gawrychowski, Filip Mazowiecki, and Michal Skrzypczak, editors,50th International Symposium on Mathematical Foundations of Computer Science, MFCS 2025, Warsaw, Poland, Au- gust 25-29, 2025, volume 345 ofLI...

    work page 2025

  5. [5]

    Barlag, V

    T. Barlag, V. Holzapfel, L. Strieker, J. Virtema, and H. Vollmer. Graph neural net- works and arithmetic circuits. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M. Tomczak, and Cheng Zhang, editors,Advances in Neural Information Processing Systems 38: Annual Conference on Neural Infor- mation Processing Systems 202...

    work page 2024

  6. [6]

    Blanc and O

    M. Blanc and O. Bournez. A characterization of polynomial time computable functions from the integers to the reals using discrete ordinary differential equations. In J´ erˆ ome Durand-Lose and Gy¨ orgy Vaszil, editors,Machines, Computations, and Universality - 9th International Conference, MCU 2022, Debrecen, Hungary, August 31 - September 2, 2022, Procee...

    work page 2022

  7. [7]

    Blanc and O

    M. Blanc and O. Bournez. A characterisation of functions computable in polynomial time and space over the reals with discrete ordinary differential equations: Simulation of turing machines with analytic discrete odes. In J´ erˆ ome Leroux, Sylvain Lombardy, and David Peleg, editors,48th International Symposium on Mathematical Founda- tions of Computer Sci...

    work page 2023

  8. [8]

    Blanc and O

    M. Blanc and O. Bournez. The complexity of computing in continuous time: Space complexity is precision. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors,51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, Tallinn, Estonia, July 8-12, 2024, volume 297 ofLIPIcs, pages 129:1–129:22. Schloss Dagstuhl -...

    work page 2024

  9. [9]

    Bournez and A

    O. Bournez and A. Durand. Recursion schemes, discrete differential equations and characterization of polynomial time computations. In Peter Rossmanith, Pinar Heg- gernes, and Joost-Pieter Katoen, editors,44th International Symposium on Mathemat- ical Foundations of Computer Science, MFCS 2019, Aachen, Germany, August 26-30, 2019, volume 138 ofLIPIcs, page...

    work page 2019

  10. [10]

    Bournez and A

    O. Bournez and A. Durand. A characterization of functions over the integers com- putable in polynomial time using discrete ordinary differential equations.Comput. Complex., 32(2):7, 2023

    work page 2023

  11. [11]

    Buss.Bounded Arithmetic

    S. Buss.Bounded Arithmetic. PhD thesis, 1986

    work page 1986

  12. [12]

    P.G. Clote. A sequential characterization of the parallel complexity class NC. Technical report, Boston College, 1988

    work page 1988

  13. [13]

    Clote.Sequential, machine-independent characterizations of the parallel complex- ity classes AlogTIME, ACk, NCk and NC, pages 49–69

    P.G. Clote.Sequential, machine-independent characterizations of the parallel complex- ity classes AlogTIME, ACk, NCk and NC, pages 49–69. Progress in Computer Science and Applied Logic. Birkh¨ auser, Boston, MA, 1990

    work page 1990

  14. [14]

    P.G. Clote. On polynomial size Frege proofs of certain combinatorial principles. In P. Clote and Krj´ ıcek J., editors,Arithmetic, Proof Theory, and Computational Com- plexity, pages 166–184. Clarendon Press, 1993

    work page 1993

  15. [15]

    Clote and G

    P.G. Clote and G. Takeuti. First order bounded arithmetic and small complexity classes. In P.G. Clote and J.B. Remmel, editors,Feasible Mathematics II, pages 154–

    work page

  16. [16]

    A. Cobham. The intrinsic computational difficulty of functions. InLogic, Methodology and Phylosophy of Science: Proc. 1964 International Congress, pages 24–30. 1965

    work page 1964

  17. [17]

    Compton and C

    K.J. Compton and C. Laflamme. An algebra and a logic for nc 1. InProceedings of the Third Annual Symposium on Logic in Computer Science (LICS ’88), Edinburgh, Scotland, UK, July 5-8, 1988, pages 12–21. IEEE Computer Society, 1988. 20

    work page 1988

  18. [18]

    Cook and P

    S. Cook and P. Nguyen. Theories for TC 0 and other small circuit classes.Log. Meth. Comput. Sci., 2(1–40), 2006

    work page 2006

  19. [19]

    Durand, A

    A. Durand, A. Haak, and H. Vollmer. Model-theoretic characterization of boolean and arithmetic circuit classes of small depth. In Anuj Dawar and Erich Gr¨ adel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 354–363. ACM, 2018

    work page 2018

  20. [20]

    M. L. Furst, J. B. Saxe, and M. Sipser. Parity, circuits, and the polynomial-time hierarchy. In22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981, pages 260–270. IEEE Computer Society, 1981

    work page 1981

  21. [21]

    Gelfand.Calcul des diff´ erences finies

    A.O. Gelfand.Calcul des diff´ erences finies. Dunod, 1963

    work page 1963

  22. [22]

    Hella, J

    L. Hella, J. Kontinen, and K. Luosto. Regular representations of uniform tc 0.ACM Trans. Comput. Log., 26(4):21:1–21:46, 2025

    work page 2025

  23. [23]

    Division is in uniform TC 0

    William Hesse. Division is in uniform TC 0. In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors,Automata, Languages and Programming, pages 104–114, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg

    work page 2001

  24. [24]

    Immerman

    N. Immerman. Languages that capture complexity classes.SIAM J. Comput., 16:760– 778, 1987

    work page 1987

  25. [25]

    Immerman

    N. Immerman. Expressibility and parallel complexity.SIAM J. Comput., 18(3):625– 638, 1989

    work page 1989

  26. [26]

    Johannsen.A bounded arithmetic theory for constant depth threshold circuits, vol- ume 6 ofSpringer Lecture Notes in Logic, chapter G ¨ODEL ’96, pages 224–234

    J. Johannsen.A bounded arithmetic theory for constant depth threshold circuits, vol- ume 6 ofSpringer Lecture Notes in Logic, chapter G ¨ODEL ’96, pages 224–234. H´ ajek, P., 1996

    work page 1996

  27. [27]

    On proofs about threshold circuits and counting hierarchies

    Jan Johannsen and Chris Pollett. On proofs about threshold circuits and counting hierarchies. InThirteenth Annual IEEE Symposium on Logic in Computer Science, In- dianapolis, Indiana, USA, June 21-24, 1998, pages 444–452. IEEE Computer Society, 1998

    work page 1998

  28. [28]

    Jordan and K

    C. Jordan and K. Jord´ an.Calculus of finite differences, volume 33. American Math- ematical Soc., 1965

    work page 1965

  29. [29]

    Maass, G

    W. Maass, G. Schnitger, and E.D. Sontag. On the computational power of sigmoid versus boolean threshold circuits. In32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, October 1-4, 1991, pages 767–776. IEEE Computer Society, 1991

    work page 1991

  30. [30]

    Cambridge University Press, 2001

    Sara Negri, Jan von Plato, and Aarne Ranta.Structural Proof Theory. Cambridge University Press, 2001. 21

    work page 2001

  31. [31]

    Parberry.Circuit Complexity and Neural Networks

    I. Parberry.Circuit Complexity and Neural Networks. MIT Press, 1994

    work page 1994

  32. [32]

    Smolensky

    R. Smolensky. Algebraic methods in the theory of lower bounds for Boolean circuit complexity. In Alfred V. Aho, editor,Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987, New York, New York, USA, pages 77–82. ACM, 1987

    work page 1987

  33. [33]

    Vollmer.Introduction to Circuit Complexity: A Uniform Approach

    H. Vollmer.Introduction to Circuit Complexity: A Uniform Approach. Springer, 1999. 22 A Proofs for Section 2 (Preliminaries) A.1 Details of Section 2.1 Iffis the solution of (1) withλ=ℓand has initial valuef(0,y) =g(y), then, in particular, f(1,y) =f(0,y)+ ℓ(1)−ℓ(0) ×h(0,y, f(0,y)) =f(0,y)+h(0,y, f(0,y)). More generally, f(x,y) =f(α(ℓ(x)),y) sincexandα(ℓ(...

    work page 1999

  34. [34]

    ∃x n ≤s nA(x1,

    if it is of the form∃x 1 ≤s 1 . . .∃x n ≤s nA(x1, . . . , xn), whereA(x 1, . . . , xn)is esb. This formula is denotedA sb. Such definition and notation extend in the predictable ways to sets of formulas,Γ sb,∆ sb, . . .. Lemma 4.i. Every function that is esb-definable inTAC 0 is inFAC 0. ii. IfΓ⇒∆is provable inTAC 0,Γand∆are made of epΣ b 1-formulas andΓ ...

    work page

  35. [35]

    So TAC0(f0, f1) is a conservative extension ofTAC 0(f0); therefore,TAC 0[n](f1) is a conser- vative extension ofTAC 0[n]

    By Proposition 5,ℓ-ODE ↑ 2 is inACDL; by Lemma 4,f 1 is esb-definable inTAC 0(f0). So TAC0(f0, f1) is a conservative extension ofTAC 0(f0); therefore,TAC 0[n](f1) is a conser- vative extension ofTAC 0[n]. It is easy to show thatTAC 0[n](f1)⊢B ′′(a, f1(a)). Hence, TAC0[n]⊢ ∃y B ′′(a, y) by Proposition 10, as desired. In order to prove the completeness, we ...

    work page