Prove upper partial sums preserve zero-aware interlacing

[PerAlexandersson]

Priority

Erik priority 6.

Source

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

Goal

Prove that upperPartialSums, implemented by reverse/lower-sums/reverse,
preserves IsInterlacingSeq0Nonneg.

Acceptance criteria

• Add a checked witness of
  UpperPartialSumsPreserveInterlacingStatement.
• Use the exact current list definition.
• Cover empty, singleton, and zero-containing lists.
• Preserve pairwise Prec0 and coefficient nonnegativity.
• Prefer deriving this from the lower-partial-sum theorem plus a checked reversal
  lemma rather than duplicating the argument.

[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, the input [0, b] satisfies the current zero-aware predicate, but upperPartialSums 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]

Source-proof outline after #326:

Although upperPartialSums is implemented by reverse/lower/reverse, the proof
should follow Hoster--Stump Lemma 2.3(3) directly because reversing an
oriented interlacing sequence reverses the relation.

Write q_k = f_k + ... + f_n. For k < ell:

1. For each i with k <= i < ell, the polynomial f_i precedes every
   member of the tail f_ell, ..., f_n. Iterated Lemma 2.1(2) gives
   f_i <= q_ell.
2. Apply Lemma 2.1(1) to the common right bound q_ell and the summands
   [f_k, ..., f_(ell-1), q_ell]. This gives q_k <= q_ell.

Lean mapping:

• stage 1: prec0_sum_left_of_common_left_of_nonneg;
• stage 2: prec0_finsetSum_right_of_nonneg or a list wrapper;
• source zero/low-degree dispatch: the relation introduced by Define the source-faithful Hoster--Stump interlacing-sequence predicate #326;
• coefficient closure: hasNonnegCoeffs_sum.

A reversal lemma may still identify the implementation with suffix sums, but
it should not be used to reverse the mathematical interlacing orientation.
Do not restore UpperPartialSumsPreserveInterlacingStatement as an assumed
proposition.

[PerAlexandersson]

Corrected theorem target after #326: prove HosterStump.IsInterlacingSeq fs → HosterStump.IsInterlacingSeq (HosterStump.upperPartialSums fs). Derive it from the corrected lower-sum theorem plus reversal. The old weak proposition interface is false, as checked by weak_upperPartialSums_counterexample.