LM24 degree valuation statement

This module proves LM24, Theorem D with its printed quantifier domain: both input series are nonzero. The ultrametric inequality and separation at zero are proved directly, while multiplicativity uses LM24's reduction to Berarducci, Corollary 9.9.

The addition on degrees is Hessenberg addition transported to NatOrdinal, with an absorbing bottom element for the zero series. The source's third clause is retained even though its fixed input b is assumed nonzero. The stronger all-input separation theorem is HahnSeries.degree_eq_bot.

theorem HahnSeries.Nonpositive.degree_mul {K : Type v} [Field K] [CharZero K] (b c : Nonpositive ℝ K) : (↑(b * c)).degree = (↑b).degree + (↑c).degree

The all-input multiplicativity law underlying LM24, Theorem D. The printed theorem assumes both inputs are nonzero; the zero cases follow from the ring laws.

theorem HahnSeries.Nonpositive.real_hahn_series_degree_valuation {K : Type v} [Field K] [CharZero K] (b c : Nonpositive ℝ K) (_hb : b ≠ 0) (_hc : c ≠ 0) : (↑(b + c)).degree ≤ max (↑b).degree (↑c).degree ∧ (↑(b * c)).degree = (↑b).degree + (↑c).degree ∧ ((↑b).degree = ⊥ ↔ b = 0)

LM24, Theorem D: degree is a multiplicative valuation on nonpositive real Hahn series.