@misc{indiciae64182c2046c5, title = {Descriptive Complexity in Lean: Completeness by First-Order Reductions}, author = {Pierre Senellart and Anton Gnatenko}, year = {2026}, url = {https://arxiv.org/abs/2609.18261}, note = {Source identifier: 2609.18261} }