Documentation

LeanPool.MarkoffModP.BGS.CorvajaZannier.PlaneCurveSupportDeterminant

Rank-two support certificates for a plane curve #

A diagonal stabilizer of a torus curve is controlled by the lattice generated by differences of exponent vectors in its equation. This file introduces the two-dimensional determinant used for that lattice and proves the sharp box bound |det| ≤ 2 * degreeOf 0 f * degreeOf 1 f.

The bound is characteristic-free. In the high-characteristic range used by the Corvaja--Zannier endpoint, every nonzero such determinant is automatically nonzero modulo the characteristic.

source
def BGS.CorvajaZannier.planeCurveSupportDifferenceDet (r s t : Fin 2 →₀ ℕ) :
ℤ

The oriented lattice area of the two support differences based at r.

Equations
Instances For
    source
    def BGS.CorvajaZannier.PlaneCurveSupportHasRankTwo {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) :
    Prop

    A polynomial has rank-two support when three of its monomials have linearly independent exponent differences.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGS.CorvajaZannier.abs_planeCurveSupportDifferenceDet_le_twice_bidegree {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {r s t : Fin 2 →₀ ℕ} (hr : r ∈ f.support) (hs : s ∈ f.support) (ht : t ∈ f.support) :
      |planeCurveSupportDifferenceDet r s t| ≤ 2 * ↑(MvPolynomial.degreeOf 0 f) * ↑(MvPolynomial.degreeOf 1 f)

      Every support-lattice determinant is bounded by twice the area of the coordinate-degree box. This is the sharp uniform determinant estimate needed for the diagonal-stabilizer route to the powered-image index bound.

      source
      theorem BGS.CorvajaZannier.natAbs_planeCurveSupportDifferenceDet_le_twice_bidegree {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {r s t : Fin 2 →₀ ℕ} (hr : r ∈ f.support) (hs : s ∈ f.support) (ht : t ∈ f.support) :
      (planeCurveSupportDifferenceDet r s t).natAbs ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f

      Natural-number form of the support determinant bound.

      source
      theorem BGS.CorvajaZannier.exists_positive_supportDet_natAbs_le_twice_bidegree {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hrank : PlaneCurveSupportHasRankTwo f) :
      ∃ (r : Fin 2 →₀ ℕ) (s : Fin 2 →₀ ℕ) (t : Fin 2 →₀ ℕ), r ∈ f.support ∧ s ∈ f.support ∧ t ∈ f.support ∧ 0 < (planeCurveSupportDifferenceDet r s t).natAbs ∧ (planeCurveSupportDifferenceDet r s t).natAbs ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f

      A rank-two support certificate supplies a positive lattice index bounded by the public Euler budget.