A nonzero polynomial of degree at most 2*d^3 detects all plane sections that lose the full degree or fail geometric irreducibility.

theorem CCDN.universalPlaneMap_planeDegree_le {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) : ((universalPlaneMap K σ) f).totalDegree ≤ f.totalDegree

The universal plane restriction of f has total degree at most the total degree of f in the two plane coordinates.

theorem CCDN.universalPlanePolynomial_specialization_totalDegree {K : Type u_1} {L : Type u_2} {σ : Type u_3} [CommRing K] [CommRing L] (f : MvPolynomial σ K) (φ : MvPolynomial (PlaneParameters σ) K →+* L) : bivariateTotalDegree ((bivariateMap φ) (universalPlanePolynomial f)) ≤ f.totalDegree

Every specialization of the plane parameters of the universal plane restriction of f has total degree at most the total degree of f.

noncomputable def CCDN.universalPlaneBadWitness {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) (rows : Fin (2 * f.totalDegree ^ 2 - 1) → ℕ × ℕ) (cols : Fin (2 * f.totalDegree ^ 2 - 1) → ClosedFormColumns f.totalDegree) : MvPolynomial (PlaneParameters σ) K

The bad-plane witness: the universal outer leading coefficient of the plane restriction of f times the closed-form minor with rows rows and columns cols. The leading-coefficient factor detects all outer-degree drops.

Equations

• CCDN.universalPlaneBadWitness f rows cols = CCDN.universalPlaneLeading f * ((CCDN.closedFormCoefficientMatrix f.totalDegree (CCDN.universalPlanePolynomial f)).submatrix rows cols).det

theorem CCDN.universalPlaneBadWitness_good_specialization {K : Type u_1} {L : Type u_2} {σ : Type u_3} [CommRing K] [Field L] (f : MvPolynomial σ K) (hpos : 0 < f.totalDegree) (hchar : CharZeroOrGT L f.totalDegree) (rows : Fin (2 * f.totalDegree ^ 2 - 1) → ℕ × ℕ) (cols : Fin (2 * f.totalDegree ^ 2 - 1) → ClosedFormColumns f.totalDegree) (φ : MvPolynomial (PlaneParameters σ) K →+* L) (hw : φ (universalPlaneBadWitness f rows cols) ≠ 0) : ((bivariateMap φ) (universalPlanePolynomial f)).natDegree = f.totalDegree ∧ bivariateTotalDegree ((bivariateMap φ) (universalPlanePolynomial f)) = f.totalDegree ∧ Irreducible ((bivariateMap φ) (universalPlanePolynomial f))

Nonvanishing certifies full degree and irreducibility over ANY target field of characteristic zero or greater than d. In particular it applies in the algebraic closure when detecting geometrically bad finite-field planes.

theorem CCDN.exists_universalPlane_badWitness {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (f : MvPolynomial (Option σ) K) (hf : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpos : 0 < f.totalDegree) (hchar : CharZeroOrGT K (2 * f.totalDegree ^ 2)) : ∃ (rows : Fin (2 * f.totalDegree ^ 2 - 1) → ℕ × ℕ) (cols : Fin (2 * f.totalDegree ^ 2 - 1) → ClosedFormColumns f.totalDegree), universalPlaneBadWitness f rows cols ≠ 0 ∧ (universalPlaneBadWitness f rows cols).totalDegree ≤ 2 * f.totalDegree ^ 3

A concrete cubic-degree bad-section witness over the original field.

theorem CCDN.exists_integer_universalPlane_badWitness {L : Type u_1} {σ : Type u_2} [Field L] [CharZero L] [IsAlgClosed L] [Finite σ] (f : MvPolynomial (Option σ) ℤ) (hf : Irreducible ((MvPolynomial.map (Int.castRingHom L)) f)) (hpos : 0 < f.totalDegree) : ∃ (rows : Fin (2 * f.totalDegree ^ 2 - 1) → ℕ × ℕ) (cols : Fin (2 * f.totalDegree ^ 2 - 1) → ClosedFormColumns f.totalDegree), universalPlaneBadWitness f rows cols ≠ 0 ∧ (universalPlaneBadWitness f rows cols).totalDegree ≤ 2 * f.totalDegree ^ 3

A nonzero integer polynomial in the full parameter space, constructed for every geometrically irreducible integer equation.