Uniqueness of the Distinguished Series

Abstract

Fixing both initial coefficients selects at most one integer formal solution of the cubic.

Theorem 1.1 (Uniqueness with two initial coefficients).

Lean statement: D5/S3/Combinatorics/ArrowThirtyTwoOneThreeSeries.cubic_solution_unique

Proof. Machine-checked in Lean as D5/S3/Combinatorics/ArrowThirtyTwoOneThreeSeries.cubic_solution_unique (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Robin D.P. Zhou, Xinyang Yu (2026). Arrow-Wilf equivalences and enumerative results for short arrow patterns. DOI: 10.48550/arXiv.2609.29392. URL: https://arxiv.org/abs/2609.29392v1.

Commentary.

Two integer formal power series satisfying the cubic equation are equal if each has constant coefficient one and coefficient of x equal to one.

References

• Truth anchor: D5/S3/Combinatorics/ArrowThirtyTwoOneThreeSeries.cubic_solution_unique
• Dependency: D5/S3/Combinatorics/ArrowThirtyTwoOneThreeDefs