Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Descriptive complexity: decision classes defined by counting

lax-175070·formalized by Pierre Senellart @PierreSenellart · Claude (Anthropic)·created ·GitHub @de5af88·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    Decision classes defined by counting, from the descriptive-complexity library. It builds on the NP core registered as lax-904597 and on the submissions on logarithmic space (lax-485149), polynomial time (lax-535992), the polynomial hierarchy (lax-564036), AC⁰ (lax-895169), and counting problems, #P, and FP (lax-366625).

    A problem is in one of these classes when its answer is a property of the numbers of witnesses of existential second-order sentences over ordered structures, the descriptive form of the numbers of accepting runs of a nondeterministic machine: ⊕P, after Papadimitriou and Zachos and, independently, Goldschlager and Parberry, when the number is odd; Mod_k P, after Cai and Hemachandra, when it is not a multiple of k; PP, after Gill, when one number exceeds another; C₌P, after Wagner, when two numbers are equal; and UP, after Valiant, when there is at most one witness and the answer is whether there is one. Comparing two numbers, rather than taking the sign of one integer, is the two-number form of the GapP characterization of Fenner, Fortnow, and Kurtz.

    UP is contained in NP and in ⊕P, NP and coNP in PP, and ⊕P and PP are closed under complement. ⊕SAT is ⊕P-complete and Mod_k-SAT is Mod_k P-complete, and more generally the parity and the residues of every parsimoniously #P-complete problem are complete, since a parsimonious reduction preserves every property of the count; ⊕P and Mod_k P are also reducibility to the parity and residues of the number of accepting runs of a Turing machine. Comparing the models of a CNF formula in which a selected variable is true with those in which it is false gives a PP-complete problem, by majority, and a C₌P-complete one, by equality; the hardness proof pairs two kernels in one Tseitin formula. No complete problem is known for UP, a question which Hartmanis and Hemachandra showed not to relativize.

    The proofs are those of the library's development after version 1.2.2, on its Lean 4.33 branch, sliced to what these statements use; they assume the submission's own statements and those of the submissions it requires where they compose. The library and its documentation are at https://github.com/PierreSenellart/descriptive-complexity and https://pierresenellart.github.io/descriptive-complexity/DescriptiveComplexity.html. The Lean code was written with the assistance of several Claude models; the design and the statements are the author's.

    Concepts

    Concept map
    28 concepts
    100%
    Proven claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimStatement 1, 2, … of a claim with several statementsClaim from this submission / another submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-175070,
  author = {Pierre Senellart and Claude (Anthropic)},
  title = {Descriptive complexity: decision classes defined by counting},
  year = {2026},
  howpublished = {Lax Archive, lax-175070},
  url = {https://laxarchive.org/lax-175070/},
  note = {draft},
}

    References

    1. Pierre Senellart. DescriptiveComplexity: Completeness by First-Order Reductions in Lean. 2026. doi:10.5281/zenodo.21678423 · github.com/PierreSenellart/descriptive-complexity
    2. Christos H. Papadimitriou and Stathis K. Zachos. Two remarks on the power of counting. In Theoretical Computer Science, 6th GI-Conference 269–275, 1982. doi:10.1007/BFb0009651
    3. Leslie M. Goldschlager and Ian Parberry. On the construction of parallel computers from various bases of boolean functions. Theor. Comput. Sci. 43:43–58, 1986. doi:10.1016/0304-3975(86)90165-9
    4. Jin-yi Cai and Lane A. Hemachandra. On the power of parity polynomial time. Math. Syst. Theory 23(1):95–106, 1990. doi:10.1007/BF02090768
    5. John Gill. Computational Complexity of Probabilistic Turing Machines. SIAM J. Comput. 6(4):675–695, 1977. doi:10.1137/0206049
    6. Klaus W. Wagner. The complexity of combinatorial problems with succinct input representation. Acta Informatica 23(3):325–356, 1986. doi:10.1007/BF00289117
    7. Leslie G. Valiant. Relative complexity of checking and evaluating. Inf. Process. Lett. 5(1):20–23, 1976. doi:10.1016/0020-0190(76)90097-1
    8. Stephen A. Fenner, Lance J. Fortnow and Stuart A. Kurtz. Gap-definable counting classes. J. Comput. Syst. Sci. 48(1):116–148, 1994. doi:10.1016/S0022-0000(05)80024-8
    9. Juris Hartmanis and Lane A. Hemachandra. Complexity classes without machines: On complete languages for UP. Theor. Comput. Sci. 58(1–3):129–142, 1988. doi:10.1016/0304-3975(88)90022-9
    10. G. S. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part II 115–125, 1968. Translated from the Russian.

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…