API checks for addition of principal series

The approach-zero series and the constant one give a compiled counterexample to LM24, Proposition 3.6.2 as printed: both summands are principal and the degree of the sum equals the degree of the first summand, but the nonzero terminal constant makes the sum nonprincipal.

Adding the approach-zero series to itself exercises the corrected equal-degree theorem on a nonconstant, infinite-support example. This is the author-confirmed repair used by later LM24 arguments; the broader author-suggested repair for two simultaneously zero or nonzero degrees is not assumed here.

theorem Tests.printed_proposition_3_6_2_counterexample : ∃ (b : HahnSeries.Nonpositive ℝ ℚ) (c : HahnSeries.Nonpositive ℝ ℚ), b.IsPrincipal ∧ c.IsPrincipal ∧ (↑(b + c)).degree = (↑b).degree ∧ ¬(b + c).IsPrincipal

The printed formulation of LM24, Proposition 3.6.2 is false.

theorem Tests.approachZero_add_self_isPrincipal : (approachZeroNonpositive + approachZeroNonpositive).IsPrincipal

The corrected equal-degree theorem applies to two genuine infinite principal series.