# Separating choiceless counting from polynomial time and witnessed choice

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Choiceless polynomial time with counting does not capture polynomial time](../../preprints/Choiceless-polynomial-time-with-counting-does-not-capture-polynomial-time-September-23-2026/paper.pdf)
- [Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting](../../preprints/Witnessed-symmetric-choice-is-strictly-stronger-than-choiceless-polynomial-time-with-counting-September-24-2026/paper.pdf)

## Scope

The formalized result separates polynomial time from choiceless polynomial time with counting. It gives an explicit query on finite structures with eight relations that is invariant under isomorphism and decidable in polynomial time, but is not definable in the stated hereditarily finite-set language with cardinality and polynomial bounds on stages and intermediate objects. The query applies to all finite inputs without a promise. The separate witnessed-symmetric-choice result is not included.

The formalization proves that witnessed symmetric choice strictly increases the expressive power of choiceless polynomial time with counting. It constructs one fixed sentence with exactly one witnessed-choice occurrence that gives a Boolean answer on every finite input, while no sentence of the original counting formalism defines the same class of inputs.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Polynomial-time query outside choiceless polynomial time | [ChoicelessPolynomialTime.lean](../ComparatorChallenges/ChoicelessPolynomialTime.lean) |
| Strict expressive gain from one witnessed symmetric choice | [WitnessedChoice.lean](../ComparatorChallenges/WitnessedChoice.lean) |