Bundle zero-aware nonnegative interlacing with elementwise real-rootedness

[PerAlexandersson]

Parent

Cleanup prerequisite discovered while auditing #326.

Problem

Many matrix/interlacing declarations repeat the pair of assumptions

hfs : IsInterlacingSeq0Nonneg fs
hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)

The weak predicate must remain weak: it is intentionally used for sparse
Branden-style test families, and changing its semantics would affect a broad
matrix/tactic API. The repeated real-rootedness side condition should instead
be bundled once.

Goal

Introduce a reusable predicate with the shape

def IsInterlacingSeq0NonnegRealRooted (fs : List R[X]) : Prop :=
  IsInterlacingSeq0Nonneg fs ∧
    ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)

and migrate repeated theorem signatures incrementally.

Initial API

• sublist preservation.
• conversion from IsInterlacingSeqNonneg.
• filtering zero entries yields IsInterlacingSeqNonneg.
• receiver lemmas exposing zero-aware interlacing, nonnegative coefficients,
  and splitting of nonzero members.

Acceptance criteria

• Do not strengthen or rename Prec0 or IsInterlacingSeq0Nonneg.
• Reuse the existing sublist_of_realRooted_of_ne and
  filter_ne_zero_of_realRooted proofs rather than duplicating them.
• Migrate at least one production consumer from separate assumptions to the
  bundle.
• Keep Define the source-faithful Hoster--Stump interlacing-sequence predicate #326's Hoster--Stump low-degree relation separate: this generic bundle
  deliberately retains local Prec0 semantics.
• Add no proposition scaffold or admitted theorem.
• Focused and full Lake builds pass without warnings.

[PerAlexandersson]

Draft PR #329 implements the additive bundle API and migrates one ProductFamily consumer without changing Prec0 semantics. No local build was run; CI is the validation gate.