Polynomial graph expansion by interpolation and two root counts

The interpolation dimension and the quotient polynomial degree both use the actual source size. The no-root condition on the modulus is used only to normalize the interpolation coefficients.

theorem Algebraic.Cutwidth.Extractor.Internal.polynomialNeighbor_pow_two {F : Type u_1} [CommRing F] (E : Polynomial F) (r m : ℕ) (f : Polynomial F) (y : F) : polynomialNeighbor E (2 ^ r) m f y = (y, polynomialCondenser E r m f y)

theorem Algebraic.Cutwidth.Extractor.Internal.card_polynomialNeighborSet_of_degree_one {F : Type u_1} [Field F] [Fintype F] (E : Polynomial F) (monic : E.Monic) (degree : E.natDegree = 1) (h m : ℕ) (P : Finset (Polynomial F)) (source : ∀ f ∈ P, f.degree < E.degree) : (polynomialNeighborSet E h (m + 1) P).card = Fintype.card F * P.card

theorem Algebraic.Cutwidth.Extractor.Internal.le_card_polynomialNeighborSet {F : Type u_1} [Field F] [Fintype F] {A h m : ℕ} (E : Polynomial F) (monic : E.Monic) (irreducible : Irreducible E) (degree : 1 < E.natDegree) (base : 0 < h) (P : Finset (Polynomial F)) (source : ∀ f ∈ P, f.degree < E.degree) (size : P.card ≤ h ^ m) (budget : A + (E.natDegree - 1) * (h - 1) * m ≤ Fintype.card F) : A * P.card ≤ (polynomialNeighborSet E h m P).card

theorem Algebraic.Cutwidth.Extractor.Internal.polynomialNeighborSet_expansion {F : Type u_1} [Field F] [Fintype F] {h m : ℕ} (E : Polynomial F) (monic : E.Monic) (irreducible : Irreducible E) (degree : 1 < E.natDegree) (base : 0 < h) (P : Finset (Polynomial F)) (source : ∀ f ∈ P, f.degree < E.degree) (size : P.card ≤ h ^ m) : (Fintype.card F - (E.natDegree - 1) * (h - 1) * m) * P.card ≤ (polynomialNeighborSet E h m P).card