Documentation

LeanPool.MarkoffModP.BGS.Markoff.MiddleGame.WeightedTraceEulerSeven

Euler budget seven for the weighted trace curve #

The reduced weighted trace closure has bidegree (2,2) and, when the second weight is nonzero, contains the affine origin. Both coordinate functions vanish at the finite place selected above that origin. Combining this shared place with the generic canonical-divisor estimate lowers the sound log-canonical degree budget from 8 to 7.

This is deliberately weaker than the paper's unsupported value 3, but it uses only the normalization-place machinery proved in the repository.

source
theorem BGS.Markoff.weightedTraceTorusClosurePolynomial_degreeOf_first {K : Type u_1} [Field K] (alpha beta : K) (hbeta : beta ≠ 0) :
MvPolynomial.degreeOf 0 (weightedTraceTorusClosurePolynomial alpha beta) = 2

The first actual coordinate degree of the weighted trace closure.

source
theorem BGS.Markoff.weightedTraceTorusClosurePolynomial_degreeOf_second {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) :
MvPolynomial.degreeOf 1 (weightedTraceTorusClosurePolynomial alpha beta) = 2

The second actual coordinate degree of the weighted trace closure.

source
def BGS.Markoff.weightedTraceTorusClosureOrigin {K : Type u_1} [Field K] (alpha beta : K) (hbeta : beta ≠ 0) :
CorvajaZannier.AffinePlaneCurvePoint (weightedTraceTorusClosurePolynomial alpha beta)

The common affine origin of the two coordinate divisors.

Equations
Instances For
    source
    theorem BGS.Markoff.weightedTraceTorusClosure_canonicalExceptionalDegree_le_seven {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) (hcardK : 2 < Fintype.card K) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) :
    let f := weightedTraceTorusClosurePolynomial alpha beta; have hf := ⋯; have hx := ⋯; CorvajaZannier.finiteExtensionDivisorDegree K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K (CorvajaZannier.PlaneCurveFunctionField f) ⋯) + ∑ w ∈ CorvajaZannier.propositionTwoExceptionalPlaces K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0 ^ m) (CorvajaZannier.planeCurveFunction f 1 ^ n), ↑(CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) w) ≤ 7

    The sound log-canonical degree budget for the weighted trace curve is at most seven. The sole field-size premise is the one needed by the canonical different estimate.