Counting all affine-plane parameter choices whose section drops degree or is not geometrically irreducible. This includes zero restrictions, but incidence averaging uses a sharper separate bound on those.

noncomputable def CCDN.universalPlaneSection {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) (v : PlaneParameters σ → K) : Polynomial (Polynomial K)

The bivariate restriction at a point of the full parameter space.

Equations

• CCDN.universalPlaneSection f v = (CCDN.bivariateMap (MvPolynomial.eval v)) (CCDN.universalPlanePolynomial f)

def CCDN.BadPlaneParameters {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial σ K) : Type (max 0 u_1 u_2)

The plane parameters (possibly degenerate) at which the plane section of f drops total degree or is not geometrically irreducible.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.bivariateMap_comp_apply {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] (φ : R →+* S) (ψ : S →+* T) (f : Polynomial (Polynomial R)) : (bivariateMap (ψ.comp φ)) f = (bivariateMap ψ) ((bivariateMap φ) f)

Mapping the coefficients of a nested bivariate polynomial along a composite ring homomorphism ψ.comp φ is the same as mapping along φ and then along ψ.

theorem CCDN.finite_field_bad_plane_parameters_card {K : Type u_1} {σ : Type u_2} [Field K] [Fintype K] [Fintype σ] {p : ℕ} [CharP K p] (f : MvPolynomial (Option σ) K) (hf : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpos : 0 < f.totalDegree) (hchar : 2 * f.totalDegree ^ 2 < p) : Nat.card (BadPlaneParameters f) ≤ 2 * f.totalDegree ^ 3 * Fintype.card K ^ (3 * (Fintype.card σ + 1) - 1)

In m ambient coordinates, at most 2d^3q^(3*m-1) parameter choices are bad. This counts triples (base point, first direction, second direction).