Order-polynomial positivity for width-two posets with a chain of at most five elements

Statement and scope

Formal scope. Lean 4.35.0 checks the chamber certificates for a short chain of size at most four: for each of the 22 chambers the kernel (decide +kernel, no native_decide) verifies that squares and a nonnegative remainder add up exactly to the certified gap polynomial, and Lean proves that each such polynomial is nonnegative on the closed orthant of any linearly ordered field and dominates (a − 1)! times the sum of the comparable gaps, and that the chambers are exactly the Dyck words. The identification of the gap polynomials with the linear coefficient of the order polynomial (descent–rook correspondence, degree bound, determining set and point identities), the 42 chambers for a = 5 and the reduction to the linear coefficient have conventional proofs or certificates checked by an independent standard-library program.

Lean 4.35.0 checks the square certificates and proves nonnegativity and the linear lower bound for the 22 chamber polynomials with a short chain of size at most four. The link between the chamber polynomials and the order polynomial, the size-five chambers and the reduction to the linear coefficient have conventional proofs or certificates checked by an independent program.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site

manuscript.pdf 310 KB

PDF on GitHub

papers/mathematics/width-two-order-polynomial/manuscript.pdf

LaTeX source

papers/mathematics/width-two-order-polynomial/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/width-two-order-polynomial/

Lean project

papers/mathematics/width-two-order-polynomial/lean/ 5 Lean files

Lakefile

papers/mathematics/width-two-order-polynomial/lean/lakefile.toml

Toolchain

leanprover/lean4:v4.35.0

Library roots

• lean/ShortChain.lean
• lean/ShortChain/

Reproduce

The commands below are quoted from papers/mathematics/width-two-order-polynomial/VERIFICATION.md, which gives their context and working directory.

Certificates

python3 certificate/check_certificates.py --extra 3 --json certificate-check.json

Lean

bash scripts/verify.sh /tmp/width-two-verification

README

papers/mathematics/width-two-order-polynomial/README.md

Verification guide

papers/mathematics/width-two-order-polynomial/verification/README.md

Verification record

papers/mathematics/width-two-order-polynomial/VERIFICATION.md

Authorship

papers/mathematics/width-two-order-polynomial/AUTHORSHIP.md

Repository guide

verification/README.md

Unfinished proofs

UNFINISHED.md

Source and prior work

Prior work. Ferroni, Morales and Panova, arXiv:2503.16403v3, Conjecture 7.1. · Alexandersson and Jal, arXiv:2410.00127v3. Public partial results on the same conjecture, for ordinal sums of one- and two-element antichains (10m-u/open-problems-catalog) and for single cross-link factors (chris-hadad/lr-stretching-results), cover classes that neither contain nor are contained in this one.

Source. Ferroni, Morales and Panova posed the conjecture and proved the reduction to the linear coefficient (Skew shapes, Ehrhart positivity and beyond, arXiv:2503.16403v3, Conjecture 7.1, Theorem 3.4; Proc. London Math. Soc. 2026). The descent–rook correspondence is due to Alexandersson and Jal. Public partial results on the same conjecture (ordinal sums of one- and two-element antichains; single cross-link factors) are credited in the manuscript; neither class contains the other. Historical priority is not certified.

Questions and answers

What does the Ferroni–Morales–Panova conjecture say?

Conjecture 7.1 of Ferroni, Morales and Panova states that for every finite poset P of width at most two, |P|! times the order polynomial Ω_P(t), which counts weakly order-preserving maps to {1, …, m} at t = m, has nonnegative coefficients in the monomial basis. They reported computer checks when both chains of a two-chain cover have at most five elements.

What is proved here?

The conjecture holds whenever P is the union of two chains one of which has at most five elements; the other chain may be arbitrarily long and the comparabilities between the chains are arbitrary. The linear coefficient is at least (a − 1)!(b − 1)! m/(a + b)!, so it is positive exactly when the comparability graph is connected. The unrestricted conjecture remains open. Public partial results on ordinal sums of one- and two-element antichains and on single cross-link factors cover different classes.

Is the result formally verified?

Partly. Lean 4 checks the square certificates and proves nonnegativity of the chamber polynomials for a short chain of size at most four. The link between these polynomials and the order polynomial, the size-five chambers and the reduction to the linear coefficient have conventional proofs or certificates checked by an independent program.

Cite

Citation file papers/mathematics/width-two-order-polynomial/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026widthtwoorderpolynomial,
  author = {Goyal, Dev D.},
  title = {Order-Polynomial Positivity for Width-Two Posets with a Chain of at Most Five Elements},
  year = {2026},
  month = oct,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/width-two-order-polynomial}
}

Copy BibTeX

Related results

• Counterexamples to a late-iterate ordering conjecture for generalized Hofstadter functionsDisprovedInteger sequences and combinatorics · shared Lean library
• Sharp root log-concavity of alternating Motzkin sumsProvedInteger sequences and combinatorics · shared Lean library
• Sharp log-concavity for alternating Motzkin sumsNew theoremInteger sequences · standalone Lean package
• A positive constant-recursive sequence with nonquasipolynomial power ranksCounterexampleInteger sequences · standalone Lean package