Proposition Two with Euler budget seven for the weighted trace curve #
The general bidegree endpoint uses the ambient budget 8. For the weighted
trace curve, the common affine origin saves one boundary degree, while the
sparse support determinant bounds the powered-image index by 2. This module
feeds both exact inputs into the natural and swapped Proposition Two proofs.
theorem
BGS.Markoff.weightedTracePropositionTwo_natural_eulerSeven
{K : Type u_1}
[Field K]
[Fintype K]
[DecidableEq K]
{p : ℕ}
[Fact (Nat.Prime p)]
[CharP K p]
(alpha beta : K)
(hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta)
(m n : ℕ)
(hm : 0 < m)
(hn : 0 < n)
(hmPrime : ¬p ∣ m)
(hnPrime : ¬p ∣ n)
(hcardK : 2 < Fintype.card K)
:
let f := weightedTraceTorusClosurePolynomial alpha beta;
have hf := ⋯;
CorvajaZannier.PropositionTwoNumericalAlternatives (n * MvPolynomial.degreeOf 0 f) (m * MvPolynomial.degreeOf 1 f) p 7
↑(CorvajaZannier.planeCurveExhaustiveTorsionGcdWeightedDegree hf ⋯ m n)
theorem
BGS.Markoff.weightedTracePropositionTwo_swapped_eulerSeven
{K : Type u_1}
[Field K]
[Fintype K]
[DecidableEq K]
{p : ℕ}
[Fact (Nat.Prime p)]
[CharP K p]
(alpha beta : K)
(hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta)
(m n : ℕ)
(hm : 0 < m)
(hn : 0 < n)
(hmPrime : ¬p ∣ m)
(hnPrime : ¬p ∣ n)
(hcardK : 2 < Fintype.card K)
:
let f := weightedTraceTorusClosurePolynomial alpha beta;
have hf := ⋯;
CorvajaZannier.PropositionTwoNumericalAlternatives (m * MvPolynomial.degreeOf 1 f) (n * MvPolynomial.degreeOf 0 f) p 7
↑(CorvajaZannier.planeCurveExhaustiveTorsionGcdWeightedDegree hf ⋯ m n)
theorem
BGS.Markoff.weightedTracePropositionTwo_eulerSeven
{K : Type u_1}
[Field K]
[Fintype K]
[DecidableEq K]
{p : ℕ}
[Fact (Nat.Prime p)]
[CharP K p]
(alpha beta : K)
(hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta)
(m n : ℕ)
(hm : 0 < m)
(hn : 0 < n)
(hmPrime : ¬p ∣ m)
(hnPrime : ¬p ∣ n)
(hcardK : 2 < Fintype.card K)
:
let f := weightedTraceTorusClosurePolynomial alpha beta;
have hf := ⋯;
CorvajaZannier.PropositionTwoNumericalAlternatives
(CorvajaZannier.planeCurveTorsionLowerDegree (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f) m n)
(CorvajaZannier.planeCurveTorsionUpperDegree (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f) m n) p 7
↑(CorvajaZannier.planeCurveExhaustiveTorsionGcdWeightedDegree hf ⋯ m n)
The natural and swapped orientations give the minimum/maximum form with Euler budget exactly seven.