Affine boundary of the split trace cover

The split trace equation is naturally an equation on G_m × G_m, whereas splitTraceCoverPolynomial is its denominator-cleared affine model. Weil estimates are often stated for an affine or projective model, so the points introduced on the coordinate axes must be accounted for explicitly. For positive covering exponents and nonzero second weight, the affine model adds exactly the origin and no other coordinate-axis point.

theorem BGS.Markoff.splitTraceCoverPolynomial_axis_zero_eq_origin {K : Type u_1} [Field K] (alpha beta : K) (d e : ℕ) (hd : 0 < d) (he : 0 < e) (hbeta : beta ≠ 0) (x y : K) (hzero : (MvPolynomial.eval ![x, y]) (splitTraceCoverPolynomial alpha beta d e) = 0) (haxis : x = 0 ∨ y = 0) : x = 0 ∧ y = 0

A zero of the denominator-cleared split trace polynomial on either coordinate axis is the origin. The positivity hypotheses are essential: they ensure that clearing the Laurent denominators really contributes powers of both coordinates.

theorem BGS.Markoff.splitTraceCoverPolynomial_origin_zero {K : Type u_1} [Field K] (alpha beta : K) (d e : ℕ) (hd : 0 < d) (he : 0 < e) : (MvPolynomial.eval ![0, 0]) (splitTraceCoverPolynomial alpha beta d e) = 0

The origin is always the affine boundary point added by clearing denominators when both covering exponents are positive.

theorem BGS.Markoff.splitTraceCoverPolynomial_nonorigin_has_nonzero_coordinates {K : Type u_1} [Field K] (alpha beta : K) (d e : ℕ) (hd : 0 < d) (he : 0 < e) (hbeta : beta ≠ 0) (x y : K) (hzero : (MvPolynomial.eval ![x, y]) (splitTraceCoverPolynomial alpha beta d e) = 0) (hnonorigin : (x, y) ≠ (0, 0)) : x ≠ 0 ∧ y ≠ 0

Away from the single affine boundary point, every zero of the cleared polynomial has two nonzero coordinates and therefore is genuinely a point of the original Laurent trace curve.

noncomputable def BGS.Markoff.affineSplitTraceCoverZeros (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) : Finset (K × K)

Affine zeros of the denominator-cleared split trace polynomial.

Equations

• BGS.Markoff.affineSplitTraceCoverZeros K alpha beta d e = {z : K × K | (MvPolynomial.eval ![z.1, z.2]) (BGS.Markoff.splitTraceCoverPolynomial alpha beta d e) = 0}

noncomputable def BGS.Markoff.torusSplitTraceCoverZeros (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) : Finset (K × K)

Zeros of the cleared polynomial that lie on the original two-dimensional torus.

Equations

• BGS.Markoff.torusSplitTraceCoverZeros K alpha beta d e = {z ∈ BGS.Markoff.affineSplitTraceCoverZeros K alpha beta d e | z.1 ≠ 0 ∧ z.2 ≠ 0}

noncomputable def BGS.Markoff.splitTraceCurveSolutions (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) : Finset (Kˣ × Kˣ)

Solutions of the original Laurent trace equation, represented on Kˣ × Kˣ rather than in the denominator-cleared affine plane.

Equations

• BGS.Markoff.splitTraceCurveSolutions K alpha beta d e = {z : Kˣ × Kˣ | BGS.Markoff.SplitTraceCurveEquation alpha beta d e z.1 z.2}

@[simp]

theorem BGS.Markoff.mem_affineSplitTraceCoverZeros_iff (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) (z : K × K) : z ∈ affineSplitTraceCoverZeros K alpha beta d e ↔ (MvPolynomial.eval ![z.1, z.2]) (splitTraceCoverPolynomial alpha beta d e) = 0

@[simp]

theorem BGS.Markoff.mem_torusSplitTraceCoverZeros_iff (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) (z : K × K) : z ∈ torusSplitTraceCoverZeros K alpha beta d e ↔ (MvPolynomial.eval ![z.1, z.2]) (splitTraceCoverPolynomial alpha beta d e) = 0 ∧ z.1 ≠ 0 ∧ z.2 ≠ 0

@[simp]

theorem BGS.Markoff.mem_splitTraceCurveSolutions_iff (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) (z : Kˣ × Kˣ) : z ∈ splitTraceCurveSolutions K alpha beta d e ↔ SplitTraceCurveEquation alpha beta d e z.1 z.2

theorem BGS.Markoff.torusSplitTraceCoverZeros_card_eq_splitTraceCurveSolutions_card (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) : (torusSplitTraceCoverZeros K alpha beta d e).card = (splitTraceCurveSolutions K alpha beta d e).card

The nonzero affine zeros of the cleared polynomial and the solutions of the original Laurent equation have exactly the same cardinality. This is the finite-field bridge needed before a point estimate for one model can be used for the other.

theorem BGS.Markoff.affineSplitTraceCoverZeros_erase_origin (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) (hd : 0 < d) (he : 0 < e) (hbeta : beta ≠ 0) : (affineSplitTraceCoverZeros K alpha beta d e).erase (0, 0) = torusSplitTraceCoverZeros K alpha beta d e

Erasing the unique coordinate-axis point from the affine zero set leaves exactly the genuine torus zero set.

theorem BGS.Markoff.affineSplitTraceCoverZeros_card_eq_torus_card_add_one (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) (hd : 0 < d) (he : 0 < e) (hbeta : beta ≠ 0) : (affineSplitTraceCoverZeros K alpha beta d e).card = (torusSplitTraceCoverZeros K alpha beta d e).card + 1

Clearing Laurent denominators adds exactly one affine point. This is the exact boundary correction required when a point estimate for the affine polynomial is converted to the torus count used in the paper's endgame.