Formalize real-rooted descent polynomials of parking functions

[PerAlexandersson]

Goal

Formalize the real-rootedness of the descent generating polynomial of ordinary
parking functions,

$$ D_n(t)=\sum_{a\in PF_n} t^{\operatorname{des}(a)}. $$

The intended route is the parking-function/word descent-set transfer

$$ \sum_{a\in PF_n} F(\operatorname{Des}(a)) =\frac{1}{n+1}\sum_{w\in[n+1]^n}F(\operatorname{Des}(w)), $$

followed by a checked real-rootedness theorem for the corresponding word
descent polynomial. The formalization should prove or reuse the word-side
theorem rather than taking real-rootedness as a hypothesis.

Suggested milestones:

• define parking functions and their descent sets in a reusable combinatorial
  namespace;
• formalize the descent-set transfer/equidistribution identity;
• specialize it to the descent generating polynomial;
• connect the word polynomial to existing Eulerian, recurrence, interlacing,
  or stability infrastructure in this repository;
• prove the resulting parking-function polynomial is Splits over ℝ (with
  the repository's usual zero-polynomial convention where appropriate).

Reference: A. Cruz, P. E. Harris, K. J. Harry, J. Kretschmann,
M. McClinton, A. Moon, J. O. Museus, and E. Redmon,
On Some Discrete Statistics of Parking Functions,
J. Integer Seq. 27 (2024), Article 24.8.6.

Nearby target: weak peaks

There is a useful refinement which is also determined solely by the descent
set. Define

$$ \operatorname{wpk}(a) =#{i: a_{i-1}\le a_i>a_{i+1}}. $$

Then

$$ i\in\operatorname{wPk}(a) \iff i-1\notin\operatorname{Des}(a)\ \text{and} i\in\operatorname{Des}(a). $$

Consequently the same transfer gives

$$ \sum_{a\in PF_n}t^{\operatorname{wpk}(a)} =\frac1{n+1}\sum_{w\in[n+1]^n}t^{\operatorname{wpk}(w)}. $$

Experimentally these weak-peak polynomials appear real-rooted. Once the
descent-set transfer is available, formalizing the weak-peak corollary and
proving the word-side real-rootedness is a natural follow-up.

Warning: ordinary strict peaks are not real-rooted in general

Do not formulate the analogous claim for the strict interior peak
statistic

$$ \operatorname{pk}(a) =#{2\le i\le n-1:a_{i-1}<a_i>a_{i+1}}. $$

Ties make this statistic invisible to the descent set. Already at $n=3$,

$$ \sum_{a\in PF_3}t^{\operatorname{pk}(a)}=12+4t, \qquad \sum_{w\in[4]^3}t^{\operatorname{pk}(w)}=50+14t, $$

so the second polynomial is not four times the first.

Cruz et al. define $PF_n^j$, the parking functions with $j$ strict peaks, and
pose their enumeration as Problem 45. Their table through $n=8$ gives
real-rooted polynomials (with an apparent typo in the $n=8,j=1$ entry: the
coefficient should be $1,454,478$, not $145,478$, so that the row sums to
$9^7$).

Exact content-based computation continues to

$$ Q_9(t)=2086839+19458570t+49531336t^2+27490542t^3+1432713t^4, $$

which is real-rooted, but at $n=10$ gives

$$ Q_{10}(t)=24188458+278306304t+970166022t^2 +930536936t^3+154749971t^4. $$

As checks, $Q_{10}(1)=11^9=2,357,947,691$, while

$$ \operatorname{disc}(Q_{10}) =-18820687145162911443045336014912773771786658177536<0. $$

Its roots are approximately

$$ -4.778529087684,\quad -0.841871826798,\quad -0.196381482603\pm0.016984165881i. $$

Exact Sturm counts show that $Q_n$ has only real zeros for $n\le9$, whereas
$Q_{10}$ has exactly two real zeros. Thus $n=10$ is the first failure through
that range.

The computation avoids enumerating all $11^9$ parking functions. It sums over
contents $\mu=(\mu_1,\ldots,\mu_n)$ satisfying

$$ \mu_1+\cdots+\mu_i\ge i\quad(1\le i\le n), \qquad \sum_i\mu_i=n, $$

and computes the strict-peak polynomial of each multiset-permutation class by
a two-state recurrence remembering the last letter and whether the preceding
comparison was an ascent.

Formalizing the explicit $n=10$ counterexample would be useful if it can be
done cheaply with exact polynomial arithmetic, but it should not block the
main descent-polynomial theorem.

Completion criteria

• no sorry, new axiom, or proposition scaffold presented as a proof;
• focused and full project builds pass without new warnings;
• the public theorem is imported by RealRooted.lean;
• the issue/PR clearly distinguishes the checked descent theorem, the
  experimental weak-peak target, and the refuted strict-peak analogue.