Root multiplicities in reciprocal coordinates

Reflection at a fixed degree bound preserves the multiplicity of each invertible root, replacing that root by its inverse. For a nonzero polynomial, the multiplicity of zero in the reflection is exactly the difference between the degree bound and the actual degree. These statements apply to formal reversals after coefficient specialization, even when specialization lowers the degree or annihilates the entire polynomial.

The fixed-bound statements are useful for descending root sections from reciprocal coordinates: a degree drop contributes roots at zero in the reflected family, while all invertible roots retain their original multiplicities. In a translated reciprocal coordinate, these correspond to the original finite roots away from the translation center.

The multiplicity transport works over arbitrary commutative rings, including rings with zero divisors. No splitting hypothesis is needed.

@[simp]

theorem Polynomial.reflect_pow {R : Type u_1} [Semiring R] (p : Polynomial R) {N : ℕ} (hN : p.natDegree ≤ N) (k : ℕ) : reflect (k * N) (p ^ k) = reflect N p ^ k

Reflection of a power at the corresponding multiple of a degree bound is the power of the reflection.

@[simp]

theorem Polynomial.rootMultiplicity_reflect {R : Type u_1} [CommRing R] (p : Polynomial R) {N : ℕ} (hN : p.natDegree ≤ N) (u : Rˣ) : rootMultiplicity (↑u⁻¹) (reflect N p) = rootMultiplicity (↑u) p

Reflection exchanges an invertible root with its inverse, preserving its multiplicity. The degree bound can exceed the actual degree, and the zero polynomial is included.

@[simp]

theorem Polynomial.rootMultiplicity_reflect_zero {R : Type u_1} [CommRing R] (p : Polynomial R) (hp : p ≠ 0) {N : ℕ} (hN : p.natDegree ≤ N) : rootMultiplicity 0 (reflect N p) = N - p.natDegree

The excess of a reflection bound over the degree of a nonzero polynomial is exactly the multiplicity of zero in its reflection.

@[simp]

theorem Polynomial.rootMultiplicity_reverse {R : Type u_1} [Field R] (p : Polynomial R) {a : R} (ha : a ≠ 0) : rootMultiplicity a⁻¹ p.reverse = rootMultiplicity a p

Reversal preserves multiplicity at nonzero roots, replacing each root by its inverse.

@[simp]

theorem Polynomial.rootMultiplicity_map_reverse {R : Type u_1} {S : Type u_2} [Semiring R] [CommRing S] (p : Polynomial R) (f : R →+* S) (u : Sˣ) : rootMultiplicity (↑u⁻¹) (map f p.reverse) = rootMultiplicity (↑u) (map f p)

Specializing a formal reversal preserves the multiplicities of invertible roots of the specialized polynomial, even when specialization lowers the degree or gives zero.

@[simp]

theorem Polynomial.rootMultiplicity_map_reverse_zero {R : Type u_1} {S : Type u_2} [Semiring R] [CommRing S] (p : Polynomial R) (f : R →+* S) (hp : map f p ≠ 0) : rootMultiplicity 0 (map f p.reverse) = p.natDegree - (map f p).natDegree

When a nonzero specialization drops degree, that degree drop is exactly the multiplicity of zero in the specialized formal reversal.