Prove X-shifted split sums preserve zero-aware interlacing

[PerAlexandersson]

Priority

Erik priority 8.

Source

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

The paper's t_k is X times the entries before the split plus the
entries from the split onward.

Goal

Prove that xShiftedSplitSums preserves
IsInterlacingSeq0Nonneg.

Acceptance criteria

• Add a checked witness of
  XShiftedSplitSumsPreserveInterlacingStatement.
• Handle both endpoint splits and zero-containing lists.
• Preserve pairwise Prec0 and coefficient nonnegativity.
• Reuse prec0_mul_X_of_prec0 and finite-sum infrastructure where applicable.
• 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 singleton [b] satisfies the current predicate vacuously, but xShiftedSplitSums returns [b, X*b], which would require real-rootedness of b.

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.