Prove moving-window sums preserve zero-aware interlacing

[PerAlexandersson]

Priority

Erik priority 7.

Source

Hoster--Stump, arXiv:2508.15538, Lemma 2.3(4).

The Lean parameter width is the paper's ell; each output sums
width + 1 consecutive entries.

Goal

Add a checked theorem witnessing
MovingWindowSumsPreserveInterlacingStatement.

Acceptance criteria

• Retain the exact condition width < fs.length.
• Prove the exact current movingWindowSums width fs output.
• Cover boundary widths and zero-containing lists.
• Preserve pairwise Prec0 and coefficient nonnegativity.
• Add no target-shaped hypothesis or new proposition scaffold.

[PerAlexandersson]

Primary-source audit correction: the current proposition is false as stated. Hoster--Stump's interlacing sequence consists of real-rooted polynomials in R_{>=0}[X]; local IsInterlacingSeq0Nonneg records nonnegative coefficients and pairwise Prec0 only. Because Prec0 is automatically true when either entry is zero, it does not ensure that the other entry splits.

For example, with b = 1 + X + X^2, width 1 and input [0, b, 0] satisfy the current premises, but movingWindowSums returns [b, b], which would require Prec b b although b is not real-rooted.

The list formula and ordering do match Lemma 2.3. The prerequisite repair is a source-faithful sequence predicate that separately requires every entry to be zero or split, preserves nonnegative coefficients, and handles the paper's special degree-at-most-one convention. The current target should not be proved or assumed before that repair.

[PerAlexandersson]

Shared source-predicate prerequisite: #326.

[PerAlexandersson]

Corrected theorem target after #326: for width < fs.length, prove HosterStump.IsInterlacingSeq fs → HosterStump.IsInterlacingSeq (HosterStump.movingWindowSums width fs). The canonical formula has fs.length - width windows, matching the displayed source range; weak_movingWindowSums_counterexample checks the old weak interface is false.