Document Hoster-Stump lower-sum obstruction

[PerAlexandersson]

Summary

Depends on #331.

This audits issue #316 against Hoster--Stump, arXiv:2508.15538, p. 4 and Lemma 2.3(2). The paper's convention that every pair of degree-zero or degree-one polynomials interlaces makes the claimed lower-partial-sum closure false for mixed linear/quadratic sequences.

The PR adds a checked counterexample:

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

The input satisfies the source-exact sequence predicate: the first pair uses the low-degree convention, and both linear polynomials strictly precede f3. The final lower sum is (X + 2) * (X + 5), whose roots -2 and -5 do not bracket the root -1 of f1.

This intentionally does not close #316. A valid replacement needs a stronger pairwise Prec0 hypothesis in addition to elementwise source real-rootedness and nonnegative coefficients.

Validation

• lake ... build RealRooted.HosterStumpInterlacing
• 8568/8568 jobs passed

[PerAlexandersson]

Mandatory cleanup-only continuation pushed as af638396.

• centralizes SourcePrec.of_prec and SourcePrec.of_lowDegree;
• replaces repeated nested disjunction construction in the counterexample;
• shares repeated degree-one real-rooted witnesses;
• changes no source definition, counterexample statement, or mathematical route;
• focused build passes 8568/8568 jobs warning-free.