Symmetry-preserving query language expressiveness audit

Family 243: Separating choiceless counting from polynomial time and witnessed choice. First application triage, 9 October 2026 Australia/Brisbane.

Problem and potential new use

Database and logic-language researchers can compare choiceless counting with witnessed-choice features on unordered structures.

Applicability and commercial boundary

The separation is for the specified full formalism; a polynomial-time F3 linear system can still be solved using conventional algorithms. This is not a general data query performance impossibility.

Initial business decision

Research reference or conditional symbolic/verification engineering. No practical implementation, recurring buyer need or profitability has been demonstrated; a weak business bridge is explicitly deferred.

Next verification action

Map the finite-structure language features and construct a small illustrative linear system.

Evidence scope

The catalog statement was individually reviewed. Main-paper proof, construction effectiveness and selected formal scope comparison remain queued. No independent Lean verification was run. Source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. See source metadata.

Choiceless polynomial time with counting does not capture polynomial time.