Discriminants under integral normalization

Integral normalization replaces a degree n polynomial with leading coefficient a by a monic polynomial whose roots are the original roots multiplied by a. Its discriminant is a ^ ((n - 1) * (n - 2)) times the original discriminant. This identity lets one reduce nonmonic polynomial families to monic families while retaining control of the discriminant, even when the leading coefficient vanishes on an exceptional parameter set.

We first establish the root-scaling law over any commutative ring. Both formulas use Mathlib's convention that constant polynomials, including zero, have discriminant 1.

Mathlib's scaleRoots and integralNormalization satisfy f.scaleRoots f.leadingCoeff = f.integralNormalization * C f.leadingCoeff. The root-scaling identity controls the discriminant before monic normalization; for nonzero f, the integral-normalization identity gives the discriminant of the resulting monic polynomial.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), Section 4.

theorem TauCeti.discr_scaleRoots {R : Type u_1} [CommRing R] {f : Polynomial R} (a : R) : (f.scaleRoots a).discr = a ^ (f.natDegree * (f.natDegree - 1)) * f.discr

Scaling every root by a multiplies the discriminant of a degree n polynomial by a ^ (n * (n - 1)). The formula holds over every commutative ring, including at a = 0.

theorem TauCeti.discr_integralNormalization {R : Type u_1} [CommRing R] {f : Polynomial R} : f.integralNormalization.discr = f.leadingCoeff ^ ((f.natDegree - 1) * (f.natDegree - 2)) * f.discr

Integral normalization multiplies the discriminant of a degree n polynomial by the (n - 1) * (n - 2) power of its leading coefficient. In particular, normalization preserves the form “a power of a parameter times a unit” when both the leading coefficient and the discriminant have that form. Constants and zero are included.