Sharp fibers of integral polynomial parameters of degree at most q. The Hilbert multiplicity bounds the field degree by d*q^dimension; a separating integral element gives the same bound for every finite fiber.

theorem CCDN.bounded_degree_normalization_fiber_card_le {K : Type u_1} [Field K] [CharZero K] {n m : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [I.IsPrime] (q : ℕ) (hq : 0 < q) (l : Fin (m + 1) → MvPolynomial (Fin n) K) (hl : ∀ (i : Fin (m + 1)), (l i).totalDegree ≤ q) (hi : Function.Injective ⇑(projectionCoordinateMap I l)) (hint : (projectionCoordinateMap I l).IsIntegral) (d : ℕ) (hdimdeg : HasProjectiveDimensionDegree I m d) (z : Fin (m + 1) → K) (s : Finset (Fin n → K)) (hzero : ∀ x ∈ s, x ∈ idealZeroLocus I) (hproj : ∀ x ∈ s, ∀ (i : Fin (m + 1)), (MvPolynomial.eval x) (l i) = z i) : s.card ≤ d * q ^ (m + 1)

The fiber bound for the given normalization, with the function field and degree estimates obtained from the coordinate ring.

theorem CCDN.linear_normalization_fiber_card_le {K : Type u_1} [Field K] [CharZero K] {n m : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [I.IsPrime] (l : Fin (m + 1) → MvPolynomial (Fin n) K) (hl : ∀ (i : Fin (m + 1)), (l i).totalDegree ≤ 1) (hi : Function.Injective ⇑(projectionCoordinateMap I l)) (hint : (projectionCoordinateMap I l).IsIntegral) (d : ℕ) (hdimdeg : HasProjectiveDimensionDegree I m d) (z : Fin (m + 1) → K) (s : Finset (Fin n → K)) (hzero : ∀ x ∈ s, x ∈ idealZeroLocus I) (hproj : ∀ x ∈ s, ∀ (i : Fin (m + 1)), (MvPolynomial.eval x) (l i) = z i) : s.card ≤ d

The linear case q = 1 of bounded_degree_normalization_fiber_card_le: a fiber of a linear normalization has at most d points.