The general Corvaja--Zannier plane-curve theorem

This file is the final public assembly. Its first theorem isolates the sole powered-image index input, so that the geometric index theorem can be audited independently; the unconditional endpoint below instantiates that input.

theorem BGS.CorvajaZannier.generalPlaneCurvePropositionTwoCertificatesAboveElementaryRange_of_poweredImageIndexBound (hindex : ∀ (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [inst : Field K] [Fintype K] [DecidableEq K] [CharP K p] (f : MvPolynomial (Fin 2) K) (m n : ℕ) (hcurve : External.IsCorvajaZannierPlaneCurve f), 0 < m → 0 < n → ¬p ∣ m → ¬p ∣ n → have hf := ⋯; Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f) : GeneralPlaneCurvePropositionTwoCertificatesAboveElementaryRange

A uniform source-to-powered-image index bound supplies all Proposition 2 certificates above the elementary range.

theorem BGS.CorvajaZannier.generalCorvajaZannierPlaneCurveTheorem_of_poweredImageIndexBound (hindex : ∀ (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [inst : Field K] [Fintype K] [DecidableEq K] [CharP K p] (f : MvPolynomial (Fin 2) K) (m n : ℕ) (hcurve : External.IsCorvajaZannierPlaneCurve f), 0 < m → 0 < n → ¬p ∣ m → ¬p ∣ n → have hf := ⋯; Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f) : External.GeneralCorvajaZannierPlaneCurveTheorem

The public finite-field Corvaja--Zannier theorem follows from the exact powered-image index statement.

theorem BGS.CorvajaZannier.poweredImageIndexBound_of_isCorvajaZannierPlaneCurve (p : ℕ) (K : Type) [Field K] [CharP K p] (f : MvPolynomial (Fin 2) K) (m n : ℕ) (hcurve : External.IsCorvajaZannierPlaneCurve f) (hm : 0 < m) (hn : 0 < n) (hmPrime : ¬p ∣ m) (hnPrime : ¬p ∣ n) : have hf := ⋯; Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f

The geometric powered-image index input required by the final assembly is provided by the exact Galois stabilizer count.

theorem BGS.CorvajaZannier.generalPlaneCurvePropositionTwoCertificatesAboveElementaryRange : GeneralPlaneCurvePropositionTwoCertificatesAboveElementaryRange

The unconditional certificates for the high-characteristic range.

theorem BGS.CorvajaZannier.generalCorvajaZannierPlaneCurveTheorem : External.GeneralCorvajaZannierPlaneCurveTheorem

The general Corvaja--Zannier finite-field plane-curve theorem.