Point-count algebra for the incidence auxiliary curve

This file reduces the off-diagonal auxiliary-curve count to the exact Hasse character sum exposed in BGS.FiniteField.EllipticCharacterSum.

def BGS.Markoff.squareRootCount {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (t : F) : ℤ

The number of square roots of t, regarded as an integer.

Equations

• BGS.Markoff.squareRootCount t = ↑{x : F | x ^ 2 = t}.card

theorem BGS.Markoff.squareRootCount_eq_quadraticChar_add_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (t : F) : squareRootCount t = (quadraticChar F) t + 1

def BGS.Markoff.branchValue {F : Type u_1} [Field F] (A C y : F) : F

The generic quadratic branch value occurring in each auxiliary equation.

Equations

• BGS.Markoff.branchValue A C y = A * y ^ 2 - C

def BGS.Markoff.auxiliaryTripleCount {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (A B C D : F) : ℤ

The weighted number of affine triples (y, lambda, mu) on two quadratic branches.

Equations

• BGS.Markoff.auxiliaryTripleCount A B C D = ∑ y : F, BGS.Markoff.squareRootCount (BGS.Markoff.branchValue A C y) * BGS.Markoff.squareRootCount (BGS.Markoff.branchValue B D y)

theorem BGS.Markoff.auxiliaryTripleCount_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {A B C D : F} (hA : A ≠ 0) (hB : B ≠ 0) (hC : C ≠ 0) (hD : D ≠ 0) : auxiliaryTripleCount A B C D = ↑(Fintype.card F) - (quadraticChar F) A - (quadraticChar F) B + ∑ y : F, (quadraticChar F) (branchValue A C y * branchValue B D y)

Exact character expansion of the number of affine auxiliary triples.

theorem BGS.Markoff.sum_quadraticChar_two_linear_factors {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {A B C D : F} (hA : A ≠ 0) (hB : B ≠ 0) (hcross : A * D ≠ B * C) : ∑ x : F, (quadraticChar F) ((A * x - C) * (B * x - D)) = -(quadraticChar F) (A * B)

A quadratic with two distinct roots has character sum minus the character of its leading coefficient.

theorem BGS.Markoff.quarticTrace_add_leadingChar_eq_cubicTrace {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {A B C D : F} (hA : A ≠ 0) (hB : B ≠ 0) (hcross : A * D ≠ B * C) : ∑ y : F, (quadraticChar F) (branchValue A C y * branchValue B D y) + (quadraticChar F) (A * B) = ∑ x : F, (quadraticChar F) (x * (A * x - C) * (B * x - D))

Replacing the square variable in the quartic trace sum by a free variable produces the cubic trace sum, including the correction at infinity.

theorem BGS.Markoff.cubicTrace_eq_monicCubicTrace {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {A B C D : F} (hA : A ≠ 0) (hB : B ≠ 0) : ∑ x : F, (quadraticChar F) (x * (A * x - C) * (B * x - D)) = ∑ X : F, (quadraticChar F) (X * (X - B * C) * (X - A * D))

Scaling X = A * B * x turns the cubic trace polynomial into the monic cubic with roots 0, B * C, and A * D.

theorem BGS.Markoff.quarticTrace_add_leadingChar_eq_monicCubicTrace {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {A B C D : F} (hA : A ≠ 0) (hB : B ≠ 0) (hcross : A * D ≠ B * C) : ∑ y : F, (quadraticChar F) (branchValue A C y * branchValue B D y) + (quadraticChar F) (A * B) = ∑ X : F, (quadraticChar F) (X * (X - B * C) * (X - A * D))

The quartic trace, including its leading-coefficient correction, is exactly the character trace of the monic cubic model.

def BGS.Markoff.auxiliaryEllipticCurve {F : Type u_1} [Field F] (u v : F) : WeierstrassCurve F

The monic Weierstrass model obtained from the cubic trace sum. Its equation is Y^2 = X * (X - u) * (X - v).

Equations

• BGS.Markoff.auxiliaryEllipticCurve u v = BGS.FiniteField.legendreWeierstrassCurve u v

theorem BGS.Markoff.auxiliaryEllipticCurve_equation_iff {F : Type u_1} [Field F] (u v x y : F) : (auxiliaryEllipticCurve u v).toAffine.Equation x y ↔ y ^ 2 = x * (x - u) * (x - v)

theorem BGS.Markoff.auxiliaryEllipticCurve_delta {F : Type u_1} [Field F] (u v : F) : (auxiliaryEllipticCurve u v).Δ = 16 * u ^ 2 * v ^ 2 * (u - v) ^ 2

theorem BGS.Markoff.auxiliaryEllipticCurve_delta_ne_zero {F : Type u_1} [Field F] (hF : ringChar F ≠ 2) {u v : F} (hu : u ≠ 0) (hv : v ≠ 0) (huv : u ≠ v) : (auxiliaryEllipticCurve u v).Δ ≠ 0

theorem BGS.Markoff.auxiliaryEllipticCurve_isElliptic {F : Type u_1} [Field F] (hF : ringChar F ≠ 2) {u v : F} (hu : u ≠ 0) (hv : v ≠ 0) (huv : u ≠ v) : (auxiliaryEllipticCurve u v).IsElliptic

theorem BGS.Markoff.auxiliaryEllipticCurve_branches_delta_ne_zero {F : Type u_1} [Field F] (hF : ringChar F ≠ 2) {A B C D : F} (hA : A ≠ 0) (hB : B ≠ 0) (hC : C ≠ 0) (hD : D ≠ 0) (hcross : A * D ≠ B * C) : (auxiliaryEllipticCurve (B * C) (A * D)).Δ ≠ 0

The cubic model associated to two distinct quadratic branches is elliptic.

theorem BGS.Markoff.auxiliaryEllipticCurve_branches_isElliptic {F : Type u_1} [Field F] (hF : ringChar F ≠ 2) {A B C D : F} (hA : A ≠ 0) (hB : B ≠ 0) (hC : C ≠ 0) (hD : D ≠ 0) (hcross : A * D ≠ B * C) : (auxiliaryEllipticCurve (B * C) (A * D)).IsElliptic

def BGS.Markoff.markoffAuxiliaryEllipticCurve {F : Type u_1} [Field F] (a b : F) : WeierstrassCurve F

The Weierstrass curve attached to the two Markoff auxiliary branches.

Equations

• BGS.Markoff.markoffAuxiliaryEllipticCurve a b = BGS.Markoff.auxiliaryEllipticCurve ((9 * b ^ 2 - 4) * (4 * a ^ 2)) ((9 * a ^ 2 - 4) * (4 * b ^ 2))

theorem BGS.Markoff.markoffAuxiliaryEllipticCurve_delta_ne_zero {F : Type u_1} [Field F] (hF : ringChar F ≠ 2) {a b : F} (ha : a ≠ 0) (hb : b ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) (hB : 9 * b ^ 2 - 4 ≠ 0) (hab : a ^ 2 ≠ b ^ 2) : (markoffAuxiliaryEllipticCurve a b).Δ ≠ 0

Admissibility and the off-diagonal condition make the Markoff cubic model elliptic.

theorem BGS.Markoff.squareRootCount_nonnegative {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (t : F) : 0 ≤ squareRootCount t

theorem BGS.Markoff.squareRootCount_le_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (t : F) : squareRootCount t ≤ 2

theorem BGS.Markoff.squareRootCount_eq_zero_of_no_root {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {t : F} (h : ¬∃ (x : F), x ^ 2 = t) : squareRootCount t = 0

theorem BGS.Markoff.twelve_lt_auxiliaryTripleCount {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hHasse : FiniteField.LegendrePointCardHasseBound F) (hF : ringChar F ≠ 2) (hcard : 26 ≤ Fintype.card F) {A B C D : F} (hA : A ≠ 0) (hB : B ≠ 0) (hC : C ≠ 0) (hD : D ≠ 0) (hcross : A * D ≠ B * C) : 12 < auxiliaryTripleCount A B C D

The exact Hasse input makes the total number of affine auxiliary triples exceed the twelve triples that can lie above three forbidden first coordinates.

theorem BGS.Markoff.exists_auxiliary_triple_away_from_three {F : Type u_1} [Field F] [Fintype F] (hHasse : FiniteField.LegendrePointCardHasseBound F) (hF : ringChar F ≠ 2) (hcard : 26 ≤ Fintype.card F) {A B C D : F} (hA : A ≠ 0) (hB : B ≠ 0) (hC : C ≠ 0) (hD : D ≠ 0) (hcross : A * D ≠ B * C) (bad : Finset F) (hbad : bad.card ≤ 3) : ∃ y ∉ bad, ∃ (lambda : F) (mu : F), lambda ^ 2 = branchValue A C y ∧ mu ^ 2 = branchValue B D y

Hasse's bound for the explicit elliptic model yields an auxiliary point away from any three forbidden first coordinates.