Split trace curves: an exact polynomial model and the first irreducibility wall

The source equation is a Laurent equation on a two-dimensional torus. We keep that torus equation separate from its cleared affine polynomial, because boundary monomials are units on the torus but not in an affine polynomial ring.

For the degree-one cover, the birational change u = x / y turns the normalized equation into

u * (1 - u) * y^2 + sigma * u - 1 = 0.

The latter polynomial is Eisenstein at sigma * u - 1 when sigma is neither zero nor one. This gives an irreducibility proof that survives every field extension. The higher power-cover descent required by the paper is deliberately not encoded in this theorem: irreducibility of the quotient curve does not imply irreducibility after adjoining the two power roots.

def BGS.Markoff.weightedSplitTorusTrace {K : Type u_1} [Field K] (alpha beta : K) (w : Kˣ) : K

A weighted split-torus trace. The paper's orbit coordinates have this form.

Equations

• BGS.Markoff.weightedSplitTorusTrace alpha beta w = alpha * ↑w + beta * ↑w⁻¹

@[simp]

theorem BGS.Markoff.weightedSplitTorusTrace_one_one {K : Type u_1} [Field K] (w : Kˣ) : weightedSplitTorusTrace 1 1 w = splitTorusTrace w

def BGS.Markoff.SplitTraceCurveEquation {K : Type u_1} [Field K] (alpha beta : K) (d e : ℕ) (x y : Kˣ) : Prop

The exact split trace-cover equation from source equation (31).

Equations

• BGS.Markoff.SplitTraceCurveEquation alpha beta d e x y = (BGS.Markoff.weightedSplitTorusTrace alpha beta (y ^ e) = BGS.Markoff.splitTorusTrace (x ^ d))

noncomputable def BGS.Markoff.splitTraceCoverPolynomial {K : Type u_1} [Field K] (alpha beta : K) (d e : ℕ) : MvPolynomial (Fin 2) K

The affine polynomial obtained by multiplying the Laurent equation by x^d * y^e.

Variable 0 is x and variable 1 is y. In particular, the third term contains the factor y^e; this is the factor missing from the displayed polynomial on source line 749.

Equations

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

theorem BGS.Markoff.eval_splitTraceCoverPolynomial {K : Type u_1} [Field K] (alpha beta : K) (d e : ℕ) (x y : K) : (MvPolynomial.eval ![x, y]) (splitTraceCoverPolynomial alpha beta d e) = alpha * x ^ d * y ^ (2 * e) + beta * x ^ d - x ^ (2 * d) * y ^ e - y ^ e

theorem BGS.Markoff.eval_splitTraceCoverPolynomial_eq_zero_iff {K : Type u_1} [Field K] (alpha beta : K) (d e : ℕ) (x y : Kˣ) : (MvPolynomial.eval ![↑x, ↑y]) (splitTraceCoverPolynomial alpha beta d e) = 0 ↔ SplitTraceCurveEquation alpha beta d e x y

On the torus, vanishing of the cleared polynomial is exactly the source Laurent equation. No affine boundary point is silently added to this statement.

theorem BGS.Markoff.splitTraceCoverPolynomial_degenerate_factorization {K : Type u_1} [Field K] (d e : ℕ) : splitTraceCoverPolynomial 1 1 d e = (MvPolynomial.X 1 ^ e - MvPolynomial.X 0 ^ d) * (MvPolynomial.X 0 ^ d * MvPolynomial.X 1 ^ e - 1)

At the excluded parameter alpha * beta = 1, the normalized cleared polynomial visibly factors. This proves that the paper's nondegeneracy condition is mathematically necessary.

def BGS.Markoff.normalizedSplitTraceBirationalEquation {K : Type u_1} [Field K] (sigma u y : K) : K

The birational degree-one equation obtained from the normalized cleared equation by setting u = x / y and removing the invertible factor y.

Equations

• BGS.Markoff.normalizedSplitTraceBirationalEquation sigma u y = u * (1 - u) * y ^ 2 + sigma * u - 1

theorem BGS.Markoff.normalizedSplitTrace_birational_change {K : Type u_1} [Field K] (sigma x y : K) (hy : y ≠ 0) : x * y ^ 2 + sigma * x - x ^ 2 * y - y = y * normalizedSplitTraceBirationalEquation sigma (x / y) y

noncomputable def BGS.Markoff.normalizedSplitTraceLeadingCoefficient {K : Type u_1} [Field K] : Polynomial K

The coefficient of y^2 in the birational degree-one trace equation.

Equations

• BGS.Markoff.normalizedSplitTraceLeadingCoefficient = Polynomial.X * (1 - Polynomial.X)

noncomputable def BGS.Markoff.normalizedSplitTraceEisensteinPrime {K : Type u_1} [Field K] (sigma : K) : Polynomial K

The prime used in the Eisenstein proof.

Equations

• BGS.Markoff.normalizedSplitTraceEisensteinPrime sigma = Polynomial.C sigma * Polynomial.X - 1

noncomputable def BGS.Markoff.normalizedSplitTraceBirationalPolynomial {K : Type u_1} [Field K] (sigma : K) : Polynomial (Polynomial K)

The birational degree-one trace equation, as a polynomial in y over K[u].

Equations

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

@[simp]

theorem BGS.Markoff.eval_normalizedSplitTraceBirationalPolynomial {K : Type u_1} [Field K] (sigma u y : K) : Polynomial.eval u (Polynomial.eval (Polynomial.C y) (normalizedSplitTraceBirationalPolynomial sigma)) = normalizedSplitTraceBirationalEquation sigma u y

theorem BGS.Markoff.normalizedSplitTraceEisensteinPrime_irreducible {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : Irreducible (normalizedSplitTraceEisensteinPrime sigma)

theorem BGS.Markoff.normalizedSplitTraceEisensteinPrime_not_dvd_leading {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hsigmaOne : sigma ≠ 1) : ¬normalizedSplitTraceEisensteinPrime sigma ∣ normalizedSplitTraceLeadingCoefficient

theorem BGS.Markoff.normalizedSplitTraceBirationalPolynomial_natDegree {K : Type u_1} [Field K] (sigma : K) : (normalizedSplitTraceBirationalPolynomial sigma).natDegree = 2

theorem BGS.Markoff.normalizedSplitTraceBirationalPolynomial_isPrimitive {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hsigmaOne : sigma ≠ 1) : (normalizedSplitTraceBirationalPolynomial sigma).IsPrimitive

theorem BGS.Markoff.normalizedSplitTraceBirationalPolynomial_isEisenstein {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hsigmaOne : sigma ≠ 1) : (normalizedSplitTraceBirationalPolynomial sigma).IsEisensteinAt (Ideal.span {normalizedSplitTraceEisensteinPrime sigma})

theorem BGS.Markoff.normalizedSplitTraceBirationalPolynomial_irreducible {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hsigmaOne : sigma ≠ 1) : Irreducible (normalizedSplitTraceBirationalPolynomial sigma)

The degree-one birational trace polynomial is irreducible over every field, under exactly the two nondegeneracy conditions used by the Eisenstein argument.

theorem BGS.Markoff.map_normalizedSplitTraceBirationalPolynomial {K : Type u_1} [Field K] {L : Type u_2} [Field L] (phi : K →+* L) (sigma : K) : Polynomial.map (Polynomial.mapRingHom phi) (normalizedSplitTraceBirationalPolynomial sigma) = normalizedSplitTraceBirationalPolynomial (phi sigma)

theorem BGS.Markoff.normalizedSplitTraceBirationalPolynomial_irreducible_after_baseChange {K : Type u_1} [Field K] {L : Type u_2} [Field L] (phi : K →+* L) (sigma : K) (hsigma : sigma ≠ 0) (hsigmaOne : sigma ≠ 1) : Irreducible (Polynomial.map (Polynomial.mapRingHom phi) (normalizedSplitTraceBirationalPolynomial sigma))

Universal scalar-extension irreducibility. In particular, taking an algebraic closure gives absolute irreducibility of this explicit birational degree-one model.