Elementary finite-field torsion bounds

This file records the part of the finite-field Corvaja--Zannier estimate that uses only the fact that a nonzero polynomial has at most its degree many roots. It does not use curve geometry or the Corvaja--Zannier Wronskian argument.

theorem BGS.External.torusCurveTorsionIntersection_card_le_orders {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) (hfirst : 0 < firstOrder) (hsecond : 0 < secondOrder) : (torusCurveTorsionIntersection K f firstOrder secondOrder).card ≤ firstOrder * secondOrder

The torsion intersection injects into the product of the two groups of roots of unity. Consequently its cardinality is at most the product of the two specified orders.

theorem BGS.External.torusCurveTorsionIntersection_le_corvajaZannierBound_of_smallChar (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree firstOrder secondOrder : ℕ) (hfirstOrder : 0 < firstOrder) (hsecondOrder : 0 < secondOrder) (hsmall : p ≤ 12 * firstDegree * secondDegree) : ↑(torusCurveTorsionIntersection K f firstOrder secondOrder).card ≤ Markoff.corvajaZannierCorollaryTwoNumericalBound p firstOrder secondOrder firstDegree secondDegree (planeTorusEulerCharacteristicBound firstDegree secondDegree)

In the small-characteristic regime p ≤ 12 d₁ d₂, the second branch of the Corvaja--Zannier numerical maximum follows from the elementary finite-group cardinality bound.

def BGS.External.GeneralCorvajaZannierPlaneCurveTheoremAboveElementaryRange : Prop

The part of the general plane-curve statement lying strictly outside the elementary range p ≤ 12 d₁ d₂. This is an ordinary proposition, not an additional assumption or axiom.

Equations

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

theorem BGS.External.generalCorvajaZannierPlaneCurveTheorem_iff_aboveElementaryRange : GeneralCorvajaZannierPlaneCurveTheorem ↔ GeneralCorvajaZannierPlaneCurveTheoremAboveElementaryRange

The full general plane-curve theorem is equivalent to its restriction to the complementary range 12 d₁ d₂ < p; the omitted range is exactly the elementary small-characteristic theorem above.