Incidence of Markoff conic fibers

This file formalizes the algebra behind Proposition 6 of Bourgain--Gamburd--Sarnak. Geometric integrality is proved in BGS.Markoff.IncidenceCoordinateRing; the independent Hasse point-count gap is isolated in BGS.FiniteField.EllipticCharacterSum.

def BGS.Markoff.fiber1 {F : Type u} [Field F] (a : F) : Set (Point F)

The Markoff fiber obtained by fixing the first coordinate.

Equations

• BGS.Markoff.fiber1 a = {x : BGS.Markoff.Point F | BGS.Markoff.IsMarkoff x ∧ x.x1 = a}

def BGS.Markoff.fiber2 {F : Type u} [Field F] (a : F) : Set (Point F)

The Markoff fiber obtained by fixing the second coordinate.

Equations

• BGS.Markoff.fiber2 a = {x : BGS.Markoff.Point F | BGS.Markoff.IsMarkoff x ∧ x.x2 = a}

def BGS.Markoff.fiber3 {F : Type u} [Field F] (a : F) : Set (Point F)

The Markoff fiber obtained by fixing the third coordinate.

Equations

• BGS.Markoff.fiber3 a = {x : BGS.Markoff.Point F | BGS.Markoff.IsMarkoff x ∧ x.x3 = a}

def BGS.Markoff.FibersMeet {F : Type u} (s t : Set (Point F)) : Prop

Two fibers meet when their set-theoretic intersection is nonempty.

Equations

• BGS.Markoff.FibersMeet s t = (s ∩ t).Nonempty

def BGS.Markoff.IncidenceAux {F : Type u} [Field F] (a b y lambda mu : F) : Prop

The affine auxiliary equations used in the paper to find one third-coordinate fiber meeting the fibers with first-coordinate value a and second-coordinate value b.

Equations

• BGS.Markoff.IncidenceAux a b y lambda mu = ((9 * a ^ 2 - 4) * y ^ 2 - lambda ^ 2 = 4 * a ^ 2 ∧ (9 * b ^ 2 - 4) * y ^ 2 - mu ^ 2 = 4 * b ^ 2)

noncomputable def BGS.Markoff.incidenceAuxPolynomial1 {K : Type u} [Field K] (a : K) : MvPolynomial (Fin 3) K

The first equation of the auxiliary curve, with variables (y, lambda, mu).

Equations

• BGS.Markoff.incidenceAuxPolynomial1 a = MvPolynomial.C (9 * a ^ 2 - 4) * MvPolynomial.X 0 ^ 2 - MvPolynomial.X 1 ^ 2 - MvPolynomial.C (4 * a ^ 2)

noncomputable def BGS.Markoff.incidenceAuxPolynomial2 {K : Type u} [Field K] (b : K) : MvPolynomial (Fin 3) K

The second equation of the auxiliary curve, with variables (y, lambda, mu).

Equations

• BGS.Markoff.incidenceAuxPolynomial2 b = MvPolynomial.C (9 * b ^ 2 - 4) * MvPolynomial.X 0 ^ 2 - MvPolynomial.X 2 ^ 2 - MvPolynomial.C (4 * b ^ 2)

noncomputable def BGS.Markoff.incidenceAuxIdeal {K : Type u} [Field K] (a b : K) : Ideal (MvPolynomial (Fin 3) K)

The ideal cutting out the affine auxiliary curve from Proposition 6.

Equations

• BGS.Markoff.incidenceAuxIdeal a b = Ideal.span {BGS.Markoff.incidenceAuxPolynomial1 a, BGS.Markoff.incidenceAuxPolynomial2 b}

@[reducible, inline]

abbrev BGS.Markoff.IncidenceAuxCoordinateRing (K : Type u) [Field K] (a b : K) : Type u

The affine coordinate ring of the auxiliary curve.

Equations

• BGS.Markoff.IncidenceAuxCoordinateRing K a b = (MvPolynomial (Fin 3) K ⧸ BGS.Markoff.incidenceAuxIdeal a b)

def BGS.Markoff.IncidenceAuxGeometricallyIntegral {K : Type u} [Field K] (a b : K) : Prop

The actual geometric-integrality condition required before applying a Weil bound.

Equations

• BGS.Markoff.IncidenceAuxGeometricallyIntegral a b = IsDomain (TensorProduct K (AlgebraicClosure K) (BGS.Markoff.IncidenceAuxCoordinateRing K a b))

theorem BGS.Markoff.eval_incidenceAuxPolynomial1_vec {K : Type u} [Field K] (a y lambda mu : K) : (MvPolynomial.aeval ![y, lambda, mu]) (incidenceAuxPolynomial1 a) = (9 * a ^ 2 - 4) * y ^ 2 - lambda ^ 2 - 4 * a ^ 2

theorem BGS.Markoff.eval_incidenceAuxPolynomial2_vec {K : Type u} [Field K] (b y lambda mu : K) : (MvPolynomial.aeval ![y, lambda, mu]) (incidenceAuxPolynomial2 b) = (9 * b ^ 2 - 4) * y ^ 2 - mu ^ 2 - 4 * b ^ 2

theorem BGS.Markoff.incidenceAux_iff_aeval_eq_zero {K : Type u} [Field K] (a b y lambda mu : K) : IncidenceAux a b y lambda mu ↔ (MvPolynomial.aeval ![y, lambda, mu]) (incidenceAuxPolynomial1 a) = 0 ∧ (MvPolynomial.aeval ![y, lambda, mu]) (incidenceAuxPolynomial2 b) = 0

The coordinate-ring equations are exactly the two scalar equations used in the incidence argument.

def BGS.Markoff.conicRoot {F : Type u} [Field F] (a y discriminantRoot : F) : F

A chosen root of the quadratic defining the intersection of two coordinate fibers.

Equations

• BGS.Markoff.conicRoot a y discriminantRoot = (3 * a * y + discriminantRoot) / 2

theorem BGS.Markoff.markoffPolynomial_conicRoot {F : Type u} [Field F] (h2 : 2 ≠ 0) {a y discriminantRoot : F} (h : (9 * a ^ 2 - 4) * y ^ 2 - discriminantRoot ^ 2 = 4 * a ^ 2) : markoffPolynomial { x1 := a, x2 := conicRoot a y discriminantRoot, x3 := y } = 0

theorem BGS.Markoff.point_mem_fiber1_inter_fiber3 {F : Type u} [Field F] (h2 : 2 ≠ 0) {a y discriminantRoot : F} (h : (9 * a ^ 2 - 4) * y ^ 2 - discriminantRoot ^ 2 = 4 * a ^ 2) : { x1 := a, x2 := conicRoot a y discriminantRoot, x3 := y } ∈ fiber1 a ∩ fiber3 y

theorem BGS.Markoff.point_mem_fiber2_inter_fiber3 {F : Type u} [Field F] (h2 : 2 ≠ 0) {b y discriminantRoot : F} (h : (9 * b ^ 2 - 4) * y ^ 2 - discriminantRoot ^ 2 = 4 * b ^ 2) : { x1 := conicRoot b y discriminantRoot, x2 := b, x3 := y } ∈ fiber2 b ∩ fiber3 y

theorem BGS.Markoff.incidenceAux_implies_common_fiber {F : Type u} [Field F] (h2 : 2 ≠ 0) {a b y lambda mu : F} (h : IncidenceAux a b y lambda mu) : FibersMeet (fiber1 a) (fiber3 y) ∧ FibersMeet (fiber2 b) (fiber3 y)

theorem BGS.Markoff.incidenceAux_exists_implies_common_fiber_with {F : Type u} [Field F] (h2 : 2 ≠ 0) {P : F → Prop} {a b : F} (h : ∃ (y : F) (lambda : F) (mu : F), P y ∧ IncidenceAux a b y lambda mu) : ∃ (y : F), P y ∧ FibersMeet (fiber1 a) (fiber3 y) ∧ FibersMeet (fiber2 b) (fiber3 y)

A point on the auxiliary curve gives a common fiber, while retaining any extra predicate required of its y-coordinate.

theorem BGS.Markoff.diagonal_incidenceAux_of_firstEquation {F : Type u} [Field F] {a b y lambda : F} (hab : a ^ 2 = b ^ 2) (h : (9 * a ^ 2 - 4) * y ^ 2 - lambda ^ 2 = 4 * a ^ 2) : IncidenceAux a b y lambda lambda

On the diagonal a² = b², one equation supplies both auxiliary square roots.

theorem BGS.Markoff.auxPointExists_of_diagonal_offDiagonal {F : Type u} [Field F] {P : F → Prop} (hdiag : ∀ (a : F), P a → ∃ (y : F) (lambda : F), P y ∧ (9 * a ^ 2 - 4) * y ^ 2 - lambda ^ 2 = 4 * a ^ 2) (hoff : ∀ (a b : F), P a → P b → a ^ 2 ≠ b ^ 2 → ∃ (y : F) (lambda : F) (mu : F), P y ∧ IncidenceAux a b y lambda mu) (a b : F) : P a → P b → ∃ (y : F) (lambda : F) (mu : F), P y ∧ IncidenceAux a b y lambda mu

Combine the diagonal and off-diagonal point-existence problems.

def BGS.Markoff.IsAdmissibleCoordinate {p : ℕ} (a : ZMod p) : Prop

Coordinates retained as vertices of the paper's incidence graph.

Equations

• BGS.Markoff.IsAdmissibleCoordinate a = (a ≠ 0 ∧ (3 * a) ^ 2 ≠ 4)

def BGS.Markoff.forbiddenIntermediateCoordinates (p : ℕ) [Fact (Nat.Prime p)] : Finset (ZMod p)

The three first-coordinate values excluded from the incidence graph.

Equations

• BGS.Markoff.forbiddenIntermediateCoordinates p = {0, 2 / 3, -(2 / 3)}

theorem BGS.Markoff.forbiddenIntermediateCoordinates_card_le_three (p : ℕ) [Fact (Nat.Prime p)] : (forbiddenIntermediateCoordinates p).card ≤ 3

theorem BGS.Markoff.natCast_ne_zero_zmod_of_pos_of_lt {n p : ℕ} (hn : 0 < n) (hnp : n < p) : ↑n ≠ 0

A natural number smaller than the modulus remains nonzero in ZMod p.

theorem BGS.Markoff.admissible_of_not_mem_forbiddenIntermediateCoordinates {p : ℕ} [Fact (Nat.Prime p)] (h3 : 3 ≠ 0) {y : ZMod p} (hy : y ∉ forbiddenIntermediateCoordinates p) : IsAdmissibleCoordinate y

Outside the three forbidden values, a coordinate is admissible.

def BGS.Markoff.IncidenceAuxPointAt (p : ℕ) (hp : Nat.Prime p) : Prop

The exact auxiliary-point conclusion, including the condition that the new fiber remains a vertex of the incidence graph.

Equations

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

def BGS.Markoff.IncidenceBridgeAt (p : ℕ) (hp : Nat.Prime p) : Prop

The common-fiber conclusion actually needed for the diameter-two incidence argument.

Equations

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

theorem BGS.Markoff.incidenceAux_diagonal_point : ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → ∀ (a : ZMod p), IsAdmissibleCoordinate a → ∃ (y : ZMod p) (lambda : ZMod p), IsAdmissibleCoordinate y ∧ (9 * a ^ 2 - 4) * y ^ 2 - lambda ^ 2 = 4 * a ^ 2

The diagonal finite-field point problem suppressed in line 661 of the paper.

Besides finding an affine conic point, the proof must avoid the three possible forbidden coordinates y = 0, ±2/3.

def BGS.Markoff.IncidenceAuxOffDiagonalGeometryAt (p : ℕ) (hp : Nat.Prime p) : Prop

The geometric-integrality assertion needed in the off-diagonal case.

The paper merely calls the affine curve irreducible. A Weil argument needs geometric integrality of an appropriate model, and the assertion still requires a proof.

Equations

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

def BGS.Markoff.IncidenceAuxOffDiagonalPointAt (p : ℕ) (hp : Nat.Prime p) : Prop

The off-diagonal auxiliary-point statement reduced to the explicit elliptic character sum.

Equations

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

def BGS.Markoff.ZModLegendrePointCardHasseBound : Prop

Optional Legendre Hasse premise for the incidence-diameter route. The selected Theorem 1 proof does not use this route.

Equations

• BGS.Markoff.ZModLegendrePointCardHasseBound = ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], BGS.FiniteField.LegendrePointCardHasseBound (ZMod p)

theorem BGS.Markoff.incidenceAux_offDiagonal_point (hHasse : ZModLegendrePointCardHasseBound) : ∃ (p0 : ℕ), ∀ (p : ℕ) (_hp : Nat.Prime p), p0 ≤ p → IncidenceAuxOffDiagonalPointAt p _hp

The off-diagonal auxiliary point follows from the narrow Hasse bound for Y² = X (X - u) (X - v). This direct route does not pretend that geometric integrality alone contains the missing genus and point-count estimates.

theorem BGS.Markoff.incidenceAuxPoint_eventually (hHasse : ZModLegendrePointCardHasseBound) : ∃ (p0 : ℕ), ∀ (p : ℕ) (hp : Nat.Prime p), p0 ≤ p → IncidenceAuxPointAt p hp

For all sufficiently large primes, the explicit auxiliary equations have an admissible solution for every pair of admissible coordinates.

theorem BGS.Markoff.two_ne_zero_zmod {p : ℕ} (hp : 2 < p) : 2 ≠ 0

A prime larger than two has 2 ≠ 0 in its prime field.

theorem BGS.Markoff.incidenceBridgeAt_of_auxPoint (p : ℕ) (hp : Nat.Prime p) (h2 : 2 ≠ 0) (haux : IncidenceAuxPointAt p hp) : IncidenceBridgeAt p hp

An admissible solution of the auxiliary equations gives the required graph bridge.

theorem BGS.Markoff.incidenceBridge_eventually (hHasse : ZModLegendrePointCardHasseBound) : ∃ (p0 : ℕ), ∀ (p : ℕ) (hp : Nat.Prime p), p0 ≤ p → IncidenceBridgeAt p hp

The bridge is a consequence of the exposed point-existence problems, not an assumption.

theorem BGS.Markoff.incidenceBridge_mod_three (hHasse : ZModLegendrePointCardHasseBound) : ∃ (p0 : ℕ), ∀ (p : ℕ) (hp : Nat.Prime p), p0 ≤ p → p % 4 = 3 → IncidenceBridgeAt p hp

The bridge specialized to primes congruent to three modulo four.

theorem BGS.Markoff.incidenceBridge_mod_one_admissible (hHasse : ZModLegendrePointCardHasseBound) : ∃ (p0 : ℕ), ∀ (p : ℕ) (hp : Nat.Prime p), p0 ≤ p → p % 4 = 1 → IncidenceBridgeAt p hp

The admissible-fiber bridge specialized to primes congruent to one modulo four.