General curve-theorem interfaces

These propositions are deliberately independent of the Markoff surface and of every split, nonsplit, or cage family. Downstream code must construct the relevant plane curve, prove its geometric hypotheses and bidegree bounds, and then apply one of these two general statements. Both interfaces now have in-repository inhabitants; keeping the propositions separate makes their Markoff-specific applications explicit.

def BGS.External.HasBidegreeAtMost {K : Type u_1} [CommSemiring K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree : ℕ) : Prop

A bivariate polynomial has coordinate degrees bounded by firstDegree and secondDegree.

Equations

• BGS.External.HasBidegreeAtMost f firstDegree secondDegree = ∀ monomial ∈ f.support, monomial 0 ≤ firstDegree ∧ monomial 1 ≤ secondDegree

noncomputable def BGS.External.affinePlaneCurveZeros (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) : Finset (K × K)

Affine rational zeros of a bivariate polynomial.

Equations

• BGS.External.affinePlaneCurveZeros K f = {z : K × K | (MvPolynomial.eval ![z.1, z.2]) f = 0}

@[simp]

theorem BGS.External.mem_affinePlaneCurveZeros_iff {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {z : K × K} : z ∈ affinePlaneCurveZeros K f ↔ (MvPolynomial.eval ![z.1, z.2]) f = 0

def BGS.External.BivariateAffineHasseWeilBound (coefficient : ℕ) : Prop

A general affine plane-curve Hasse--Weil estimate with its coefficient fixed in the type. Keeping this layer separate from the existential wrapper makes numerical specializations auditable.

Equations

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

def BGS.External.GeneralBivariateAffineHasseWeilTheorem : Prop

The general affine plane-curve Hasse--Weil interface used by the Markoff applications.

This is the standard bidegree corollary of Hasse--Weil: normalization and the boundary of a geometrically irreducible curve of positive bidegree contribute only a universal multiple of firstDegree * secondDegree.

Equations

• BGS.External.GeneralBivariateAffineHasseWeilTheorem = ∃ (coefficient : ℕ), 0 < coefficient ∧ BGS.External.BivariateAffineHasseWeilBound coefficient

noncomputable def BGS.External.torusCurveTorsionIntersection (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) : Finset (Kˣ × Kˣ)

Torsion points of a general bivariate torus curve.

Equations

• BGS.External.torusCurveTorsionIntersection K f firstOrder secondOrder = {z : Kˣ × Kˣ | (MvPolynomial.eval ![↑z.1, ↑z.2]) f = 0 ∧ z.1 ^ firstOrder = 1 ∧ z.2 ^ secondOrder = 1}

@[simp]

theorem BGS.External.mem_torusCurveTorsionIntersection_iff {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {firstOrder secondOrder : ℕ} {z : Kˣ × Kˣ} : z ∈ torusCurveTorsionIntersection K f firstOrder secondOrder ↔ (MvPolynomial.eval ![↑z.1, ↑z.2]) f = 0 ∧ z.1 ^ firstOrder = 1 ∧ z.2 ^ secondOrder = 1

def BGS.External.TorusCurveNotSubtorusTranslate {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Prop

No nontrivial character is constant on the geometric torus curve.

Equations

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

def BGS.External.IsCorvajaZannierPlaneCurve {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Prop

A general plane torus curve satisfies the geometric hypotheses of the Corvaja--Zannier theorem. Nonzero partial derivatives express that both coordinate functions are separating; prime-to-characteristic torsion orders then retain nonzero differentials.

Equations

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

def BGS.External.planeTorusEulerCharacteristicBound (firstDegree secondDegree : ℕ) : ℝ

A general bidegree-only upper bound for the Euler characteristic of the normalization of a torus plane curve. For bidegree (d₁,d₂), genus is at most (d₁-1)(d₂-1) and the toric boundary has at most 2d₁+2d₂ points.

Equations

• BGS.External.planeTorusEulerCharacteristicBound firstDegree secondDegree = 2 * ↑firstDegree * ↑secondDegree

def BGS.External.GeneralCorvajaZannierPlaneCurveTheorem : Prop

The Corvaja--Zannier plane-curve interface, stated for every admissible bivariate torus curve rather than for the weighted Markoff trace family. The in-repository proof is BGS.CorvajaZannier.generalCorvajaZannierPlaneCurveTheorem; the source proof and its formal dependency path are tracked in the dedicated Blueprint chapter.

Equations

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