Acknowledgments

The authors used OpenAI’s GPT-5.6-sol as a research and coding assistant to help strengthen the results, improve the exposition, and generate and audit the Python and Lean 4 code accompanying the paper.

The authors reviewed the resulting mathematics and code and take responsibility for the final content. GPT-5.6-sol is acknowledged as a tool, not listed as an author.

The same disclosure appears in the authoritative manuscript and in ACKNOWLEDGMENTS.md.