Prove lower partial sums preserve zero-aware interlacing

[PerAlexandersson]

Priority

Erik priority 5.

Source

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

Goal

Prove that lowerPartialSums preserves
IsInterlacingSeq0Nonneg.

The paper assumes a nonzero interlacing sequence in nonnegative-coefficient
polynomials. The Lean target is deliberately zero-aware through Prec0.

Acceptance criteria

• Add a checked witness of
  LowerPartialSumsPreserveInterlacingStatement.
• Cover empty, singleton, and zero-containing lists.
• Preserve both pairwise Prec0 and coefficient nonnegativity.
• Reuse the existing weighted/common-interleaver sum lemmas.
• Add no sorry, axiom, or target-equivalent assumption.

[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 [b, 0] satisfies the current zero-aware predicate, but lowerPartialSums 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 prerequisite #326:

Hoster--Stump Lemma 2.3(2) is a two-stage repeated application of Lemma 2.1.
Write p_k = f_1 + ... + f_k. For k < ell:

1. For every j with k < j <= ell, all f_i with i <= k precede
   f_j. Lemma 2.1(1), iterated over the prefix, gives p_k <= f_j.
2. Apply Lemma 2.1(2) to the common left bound p_k and the list
   [p_k, f_(k+1), ..., f_ell]. This gives p_k <= p_ell.

The matching checked local engines are:

• prec0_finsetSum_right_of_nonneg for stage 1;
• prec0_sum_left_of_common_left_of_nonneg or
  prec0_finsetSum_left_of_nonneg for stage 2;
• hasNonnegCoeffs_sum for every prefix;
• the source-specific zero and degree-at-most-one branches from Define the source-faithful Hoster--Stump interlacing-sequence predicate #326 before
  reducing a pair to strict/local Prec0.

Concrete Lean plan:

• prove lowerPartialSums fs equals the list of nonempty prefix sums;
• prove by induction that each prefix sum is zero or nonzero and splits;
• for each pair of prefix indices, use the two cone steps above;
• if both resulting prefix sums have degree at most one, close with the
  Hoster--Stump low-degree branch; otherwise the source relation supplies
  the oriented strict pairs needed by the cone lemmas;
• package elementwise nonnegative coefficients and pairwise relations as
  IsHosterStumpInterlacingSeq.

Empty input remains the deliberate extension documented in #326; singleton
input is non-vacuous because the new predicate records elementwise
real-rootedness. No old LowerPartialSumsPreserveInterlacingStatement
assumption should be reintroduced.

[PerAlexandersson]

Corrected theorem target after #326: prove HosterStump.IsInterlacingSeq fs → HosterStump.IsInterlacingSeq (HosterStump.lowerPartialSums fs). Do not prove or assume the old weak LowerPartialSumsPreserveInterlacingStatement; weak_lowerPartialSums_counterexample checks that it is false.

[PerAlexandersson]

Primary-source audit found that the corrected target is still false.

Hoster--Stump, arXiv:2508.15538, p. 4 declares every pair of degree-zero or degree-one polynomials interlacing. Under that convention, take

• f1 = X + 1
• f2 = 2 * (X + 3)
• f3 = (X + 1) * (X + 3).

The pair (f1,f2) satisfies the source relation by convention, while both linear polynomials strictly precede f3; hence the input satisfies HosterStump.IsInterlacingSeq. Its final lower sum is (X + 2) * (X + 5), and f1 does not precede it because -1 lies above both roots -2,-5.

polytool checked the strict input pairs and rejected the output pair. PR #332 formalizes the counterexample in Lean; the focused module build passes 8568/8568 jobs. The PR deliberately does not close this issue.

A valid replacement theorem needs the stronger pairwise Prec0 relation, plus separate elementwise zero-or-splits and nonnegative-coefficient hypotheses. That repaired target can follow the two cone-sum steps already outlined here, but it must not silently replace the source-exact statement.