Restricted Bell polynomial real-rootedness — Lean-verified counterexample

The restricted Bell polynomial B₈₀₀,≤₅ has a nonreal complex zero, refuting Conjecture 6.4 of Moll–Ramírez–Villamizar (2017). The explicit counterexample is verified in Lean from the finite-set-partition definition.

Priority: A bounded literature search on November 2, 2026 did not locate an earlier exact-scope counterexample. This is not a comprehensive priority review; no novelty or first-discovery claim is made.

Original problem
Real-rootedness of restricted Bell polynomials, Conjecture 6.4 of Moll, Ramírez, and Villamizar
Also known as
restricted Bell polynomial real-rootedness conjecture; bounded-block Bell polynomial zeros
Identifiers
Moll–Ramírez–Villamizar Conjecture 6.4 (2017) · arXiv:1707.08138 · Journal of Combinatorics 9 (2018), Conjecture 6.2
Source
Victor H. Moll, José L. Ramírez, and Diego Villamizar, Combinatorial and Arithmetical Properties of the Restricted and Associated Bell and Factorial Numbers, Conjecture 6.4, §6.1, printed page 14 (2017 arXiv PDF; arXiv record). Published in Journal of Combinatorics 9 (2018), 693–720, as Conjecture 6.2.
Result
The restricted Bell polynomial B₈₀₀,≤₅ has a nonreal complex zero, refuting Conjecture 6.4 of Moll–Ramírez–Villamizar (2017). The explicit counterexample is verified in Lean from the finite-set-partition definition.
Verification
Lean, kernel-checked; standard axioms only. Lean 4.28.0 and Mathlib v4.28.0; the unconditional theorem starts from bounded finite partitions. The 13 audited declarations use only propext, Classical.choice, and Quot.sound; no native_decide.
Repository
https://github.com/cozuya/restricted-bell-counterexample

The claim

Let S≤m(n,k) count partitions of n labeled elements into k nonempty blocks, with each block of size at most m. Define

Bn,≤m(x) = Σk=0n S≤m(n,k) xk.

Conjecture 6.4 asserts that every root is real and nonpositive whenever m ≥ 1 and m is neither 3 nor 4. The restriction is on each block’s maximum size, not on the number of blocks.

Counterexample

Take n = 800 and m = 5, a permitted cap. The exact counting polynomial has degree 800 and factors as

B800,≤5(x) = x160Q(x),   deg Q = 640,   Q monic.

The Lean theorem proves that this polynomial has a complex root with nonzero imaginary part. This is a counterexample to the universal real-rootedness claim; no numerical approximation to a root is required.

Why this falsifies the claim

The first 39 leading coefficients of Q are obtained from an exact restricted-Stirling recurrence, proved equivalent to the original partition count. Newton’s identities turn these coefficients into the first 39 power sums s0,…,s38 of the negatives of its roots, counted with multiplicity.

Form the 20×20 Hankel matrix Hi,j = si+j. If all roots were real, every real vector u would satisfy uTHu ≥ 0, because the expression is a sum of squares. An explicit 20-entry integer vector instead gives uTHu < 0, verified by exact arithmetic. Hence Q, and therefore the restricted Bell polynomial, has a nonreal root.

Verification

The principal theorem is RestrictedBell.restrictedBell_800_5_nonreal, with type ∃ z : ℂ, (RestrictedBell.countingBell 800 5).IsRoot z ∧ z.im ≠ 0. The corollary RestrictedBell.realRootedness_conjecture_false negates the universally quantified conjecture. The polynomial is defined from bounded partitions of Fin 800, not an arbitrary polynomial with copied coefficients.

The Lean development proves the partition-counting recurrence, certifies 801 recurrence rows in nine batches, checks the Newton relations and the exact negative quadratic form, and connects them to the final theorem. The recorded clean rebuild passed on November 2, 2026, using Lean 4.28.0 and Mathlib v4.28.0. All 13 audited declarations report precisely propext, Classical.choice, and Quot.sound; there are no sorry, custom axioms, or native_decide dependencies in those results.

Reproduction: follow the pinned setup in the repository and run ./verify.sh. Exact-arithmetic Python verifiers provide a separate cross-check, but are outside the Lean proof’s trust boundary. The verification report records the local run; hosted CI is tracked separately.

Prior art and earlier refutations

The conjecture was posed in the 2017 preprint (Conjecture 6.4) and published in 2018 (Conjecture 6.2). A bounded search conducted on November 2, 2026 did not locate a previously published refutation for the same block-size-bounded polynomial family. Similar results about restricted Stirling matrices, other Bell polynomial families, or minimum block sizes do not by themselves settle this statement.

Limits: the counterexample is not claimed to be minimal; no classification of all caps is given. The separate log-concavity conjecture is not refuted. Formal verification establishes the mathematical contradiction, not historical novelty or priority. See the repository’s prior-art notes.

Provenance

Chris Ozols, with AI-assisted discovery, independent exact-arithmetic checking, and Lean 4 formalization. The candidate arose from a ColdHarvest research run on November 2, 2026. The public repository preserves the original computational certificate, an independent audit, the completed Lean source, hashes, and reproducible verification scripts. This account makes no claim of historical priority.