Rank logic captures polynomial time on structures with bounded colour classes

For every finite relational vocabulary τ and every q ≥ 1, inflationary fixed-point logic with counting and prime-field rank defines an isomorphism-invariant ordered copy of every finite τ-structure that is supplied with a linear preorder whose classes have size at most q. Consequently, for each fixed q, rank logic captures polynomial time on the class of structures whose colour classes have size at most q. No assumption is made on the colour groups. For fixed q only the prime fields Fp with p ≤ q are needed, and the rank arity may grow with q. Dahan recently noted that no natural logic was known to capture P on bounded colour-class graphs. A companion record from the same program, audited by an independent AI referee and to be deposited separately, shows that choiceless polynomial time with counting does not capture P on bounded colour classes. On this class, therefore, rank logic is strictly more expressive than CPT. The proof decides exact feasibility of bounded torsor diagrams, and hence of bounded coset systems, by induction on the local group bound B, in which every recursive call has local group bound at most ⌊B/2⌋. It extends an earlier argument for solvable colour groups with two new mechanisms: a centralizer reduction that decides the nonabelian socle layer using only groups of order at most ⌊B/2⌋, and a perfect-kernel localization lemma that localizes affine cocycle obstructions without assuming that H1 vanishes. Provenance and status. The proofs in this deposit were produced by AI models (OpenAI GPT models, working in separate chat threads) in a research program directed by Matthew Liston. They were checked by Claude (Anthropic) in the program's coordinating sessions; those checks were careful reads that re-derived the key identities, not full referee reports. The main proof, and the results it imports, were then audited by two independent AI referees (OpenAI models, run in sessions separate from those that produced the proofs). Both audits returned the verdict proved with fixable gaps, and the fixes they requested are included in this deposit (Appendix A of the paper). There has been no human refereeing yet, and there is no machine-checked formal proof. We are confident that the argument is correct and intend to verify it formally. Our formal-verification capacity is currently committed to other papers, so we are releasing this version now and will return to the formalization. Files. The PDF is the paper, with the full proof record reproduced verbatim in Appendix B. The zip archive contains the proof record, its three dependency records, the two AI audit reports, the generating thread's internal report, two finite-check scripts with their recorded outputs and an independent rerun, and SHA256SUMS. SHA-256 of the main proof record (proofs/RANK_LOGIC_ALL_BOUNDED_COLOURS_PROOF_2026-11-05.txt): 51770700072f5bbf5b252a295782ebc6e57971d0db219f709fee4f0f88341ca9. Contact: [email protected]

Authors

Publication Details

Journal
Zenodo (CERN European Organization for Nuclear Research)
Published
2026-11-06
DOI
https://doi.org/10.5281/zenodo.23996259
Citations
2
Primary Topic
Advanced Graph Theory Research
Type
preprint
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
NOV
preprint

Rank logic captures polynomial time on structures with bounded colour classes

Matthew Liston
2 citations
Zenodo (CERN European Organization for Nuclear Research)
Advanced Graph Theory Research
preprint

Rank logic captures polynomial time on structures with bounded colour classes

Matthew Liston
preprint en
2 citations

Abstract

For every finite relational vocabulary τ and every q ≥ 1, inflationary fixed-point logic with counting and prime-field rank defines an isomorphism-invariant ordered copy of every finite τ-structure that is supplied with a linear preorder whose classes have size at most q. Consequently, for each fixed q, rank logic captures polynomial time on the class of structures whose colour classes have size at most q. No assumption is made on the colour groups. For fixed q only the prime fields Fp with p ≤ q are needed, and the rank arity may grow with q. Dahan recently noted that no natural logic was known to capture P on bounded colour-class graphs. A companion record from the same program, audited by an independent AI referee and to be deposited separately, shows that choiceless polynomial time with counting does not capture P on bounded colour classes. On this class, therefore, rank logic is strictly more expressive than CPT. The proof decides exact feasibility of bounded torsor diagrams, and hence of bounded coset systems, by induction on the local group bound B, in which every recursive call has local group bound at most ⌊B/2⌋. It extends an earlier argument for solvable colour groups with two new mechanisms: a centralizer reduction that decides the nonabelian socle layer using only groups of order at most ⌊B/2⌋, and a perfect-kernel localization lemma that localizes affine cocycle obstructions without assuming that H1 vanishes. Provenance and status. The proofs in this deposit were produced by AI models (OpenAI GPT models, working in separate chat threads) in a research program directed by Matthew Liston. They were checked by Claude (Anthropic) in the program's coordinating sessions; those checks were careful reads that re-derived the key identities, not full referee reports. The main proof, and the results it imports, were then audited by two independent AI referees (OpenAI models, run in sessions separate from those that produced the proofs). Both audits returned the verdict proved with fixable gaps, and the fixes they requested are included in this deposit (Appendix A of the paper). There has been no human refereeing yet, and there is no machine-checked formal proof. We are confident that the argument is correct and intend to verify it formally. Our formal-verification capacity is currently committed to other papers, so we are releasing this version now and will return to the formalization. Files. The PDF is the paper, with the full proof record reproduced verbatim in Appendix B. The zip archive contains the proof record, its three dependency records, the two AI audit reports, the generating thread's internal report, two finite-check scripts with their recorded outputs and an independent rerun, and SHA256SUMS. SHA-256 of the main proof record (proofs/RANK_LOGIC_ALL_BOUNDED_COLOURS_PROOF_2026-11-05.txt): 51770700072f5bbf5b252a295782ebc6e57971d0db219f709fee4f0f88341ca9. Contact: [email protected]

Zenodo (CERN European Organization for Nuclear Research)
Advanced Graph Theory Research
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

Laika access coming soon