Define the source-faithful Hoster--Stump interlacing-sequence predicate

[PerAlexandersson]

Source

Hoster--Stump, arXiv:2508.15538, Section 2 and Lemma 2.3.

Problem

The current IsInterlacingSeq0Nonneg predicate is not the paper's notion of an
interlacing sequence. It records pairwise Prec0 and nonnegative coefficients,
but it does not require each nonzero member to split over R. Since Prec0 f g
is automatic when either entry is zero, a zero can hide a non-real-rooted
neighbor.

This makes the current statement interfaces in #316, #317, #318, and #319
false. For example, b = 1 + X + X^2 has nonnegative coefficients but is not
real-rooted:

• [b, 0] breaks the lower-partial-sum target.
• [0, b] breaks the upper-partial-sum target.
• [0, b, 0] with width 1 breaks the moving-window target.
• [b] breaks the shifted-split target.

The paper also declares any two degree-at-most-one polynomials to interlace,
which local Prec does not implement in every orientation.

Goal

Introduce a source-faithful Hoster--Stump sequence predicate, or an equivalent
API, that separately records:

• nonnegative coefficients for every member;
• every member is zero or is nonzero and splits over R;
• every earlier/later pair obeys the paper's zero and degree-at-most-one
  conventions, and otherwise the correctly oriented local Prec.

Then restate #316--#319 using this predicate.

Acceptance criteria

• Cite Section 2 and Lemma 2.3 next to the definitions.
• Preserve the exact current list formulas and ordering.
• Document that Lemma 2.3(4)'s printed tuple endpoint is off by one; the formula
  gives n - ell windows of width ell + 1, matching the current Lean list
  length.
• Decide explicitly whether empty-list behavior is a harmless extension or
  whether source-literal statements require List.Nonempty.
• Add checked counterexamples or otherwise retire the four false old
  proposition interfaces.
• Do not use the false old interfaces as assumptions.

[PerAlexandersson]

API-deduplication audit result:

Prec0 and IsInterlacingSeq0Nonneg must not be strengthened globally.
They are intentionally weak and have many matrix/tactic consumers. No current
generic relation exactly matches Hoster--Stump's additional convention that
any two degree-at-most-one polynomials interlace.

The source-faithful design should therefore have:

1. A Hoster--Stump-scoped pair relation that requires both members to split
   and then permits zero, the degree-at-most-one exception, or oriented
   Prec.
2. A sequence predicate requiring nonnegative coefficients, elementwise
   splitting, and pairwise use of that relation.
3. A separate generic bundle for the frequently repeated
   IsInterlacingSeq0Nonneg plus elementwise-splitting assumptions.

The generic bundle is cleanup infrastructure, not the source relation, and is
tracked separately so #326 does not silently change repository-wide Prec0
semantics.

Generic cleanup issue: #328

[PerAlexandersson]

Primary-source refinement: the source-faithful Hoster--Stump pair relation needs one condition beyond elementwise splitting. Section 2 explicitly declares any two polynomials of degree at most one to interlace, regardless of the usual orientation. Local Prec does not include that convention: a linear polynomial followed by a constant cannot satisfy its degree orientation.

Therefore the scoped pair relation should be: both members satisfy the source real-rooted/zero condition, and either endpoint is zero, or both natDegrees are at most one, or local oriented Prec f g holds. The sequence predicate must combine this pairwise relation for every earlier/later pair with nonnegative coefficients and elementwise real-rootedness (including singleton lists).

PR #329's IsInterlacingSeq0NonnegRealRooted is a useful generic bundle and fixes the zero-masks-nonreal-root defect, but it is not by itself the exact Hoster--Stump Section 2 predicate because it deliberately retains local Prec0. Keep #326 as the source-specific layer.

[PerAlexandersson]

Implemented in PR #331. The new RealRooted.HosterStumpInterlacing module defines the exact Section 2 zero/splitting and degree-at-most-one conventions, a nonnegative elementwise-real-rooted pairwise sequence predicate, all four Lemma 2.3 list formulas, and checked counterexamples retiring the four false weak targets. Empty lists are documented as a harmless extension; singleton real-rootedness is non-vacuous. Focused build passed 8568/8568 jobs. Issues #316--#319 now state corrected theorem targets. The issue should close when PR #331 merges.