Comparing the pulled cage cover with its affine plane models

The plane models retain the power parameter t, whereas the pulled cover requires t ≠ 0. On the diagonal the plane model also forgets the choice between the two equal radicand roots. This file isolates those two losses and bounds them by the roots of explicit univariate polynomials.

theorem BGS.Markoff.cagePulledRadicand_natDegree_le (K : Type u_1) [Field K] (xi : K) (d : ℕ) : (cagePulledRadicand xi d).natDegree ≤ 4 * d

The pulled radicand has degree at most 4d.

@[reducible, inline]

abbrev BGS.Markoff.CageDiagonalPlanePoint (p : ℕ) [Fact (Nat.Prime p)] (xi : ZMod p) (d : ℕ) : Type

Rational points of the diagonal plane model.

Equations

• BGS.Markoff.CageDiagonalPlanePoint p xi d = ↥(BGS.External.affinePlaneCurveZeros (ZMod p) (BGS.Markoff.cageDiagonalPlanePolynomial xi d))

@[reducible, inline]

abbrev BGS.Markoff.CageDiagonalTaggedPlanePoint (p : ℕ) [Fact (Nat.Prime p)] (xi : ZMod p) (d : ℕ) : Type

A plane point together with the sign used to recover the second root.

Equations

• BGS.Markoff.CageDiagonalTaggedPlanePoint p xi d = (BGS.Markoff.CageDiagonalPlanePoint p xi d × Bool)

def BGS.Markoff.IsGoodDiagonalTaggedPoint {p : ℕ} [Fact (Nat.Prime p)] {xi : ZMod p} {d : ℕ} (z : CageDiagonalTaggedPlanePoint p xi d) : Prop

The tagged points which recover a unique pulled pair. At a zero root, the two signs coincide, so only false is retained.

Equations

• BGS.Markoff.IsGoodDiagonalTaggedPoint z = ((↑z.1).2 ≠ 0 ∧ ((↑z.1).1 ≠ 0 ∨ z.2 = false))

def BGS.Markoff.goodDiagonalTaggedPointEquivPulled (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi : ZMod p) (d : ℕ) : { z : CageDiagonalTaggedPlanePoint p xi d // IsGoodDiagonalTaggedPoint z } ≃ CagePulledRootPair p xi xi d

Away from the explicit exceptional set, a signed diagonal plane point is exactly a pulled pair of roots.

Equations

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

def BGS.Markoff.badDiagonalTaggedPointEmbedding (p : ℕ) [Fact (Nat.Prime p)] (xi : ZMod p) {d : ℕ} (hd : 0 < d) : { z : CageDiagonalTaggedPlanePoint p xi d // ¬IsGoodDiagonalTaggedPoint z } ↪ { root : ZMod p // root ^ 2 = xi ^ 2 - 4 } × Bool ⊕ { parameter : ZMod p // Polynomial.eval parameter (cagePulledRadicand xi d) = 0 }

The bad signed diagonal points inject into either the two signs above t = 0, or a root of the pulled radicand with the duplicated sign.

Equations

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

theorem BGS.Markoff.natCard_badDiagonalTaggedPoint_le (p : ℕ) [Fact (Nat.Prime p)] (xi : ZMod p) {d : ℕ} (hd : 0 < d) (hXi : xi ^ 2 - 4 ≠ 0) : Nat.card { z : CageDiagonalTaggedPlanePoint p xi d // ¬IsGoodDiagonalTaggedPoint z } ≤ 4 * d + 4

The diagonal exceptional set has size at most 4d + 4: four signed points can lie above t = 0, and every remaining exception is a zero of the degree-4d pulled radicand.

theorem BGS.Markoff.two_mul_diagonalPlanePoint_card_eq_pulled_add_bad (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi : ZMod p) (d : ℕ) : 2 * (External.affinePlaneCurveZeros (ZMod p) (cageDiagonalPlanePolynomial xi d)).card = Nat.card (CagePulledRootPair p xi xi d) + Nat.card { z : CageDiagonalTaggedPlanePoint p xi d // ¬IsGoodDiagonalTaggedPoint z }

Exact bookkeeping identity behind the diagonal comparison.

theorem BGS.Markoff.cagePulledRootPair_diagonal_card_comparison (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi : ZMod p) {d : ℕ} (hd : 0 < d) (hXi : xi ^ 2 - 4 ≠ 0) : |↑(Nat.card (CagePulledRootPair p xi xi d)) - 2 * ↑(External.affinePlaneCurveZeros (ZMod p) (cageDiagonalPlanePolynomial xi d)).card| ≤ 4 * ↑d + 4

The pulled diagonal cover differs from twice its plane-model count by at most the explicit exceptional contribution 4d + 4.

@[reducible, inline]

abbrev BGS.Markoff.CageOffDiagonalPlanePoint (p : ℕ) [Fact (Nat.Prime p)] (xi eta : ZMod p) (d : ℕ) : Type

A point on the off-diagonal plane curve used in the cage count.

Equations

• BGS.Markoff.CageOffDiagonalPlanePoint p xi eta d = ↥(BGS.External.affinePlaneCurveZeros (ZMod p) (BGS.Markoff.cageOffDiagonalPlanePolynomial xi eta d))

def BGS.Markoff.IsGoodOffDiagonalPlanePoint {p : ℕ} [Fact (Nat.Prime p)] {xi eta : ZMod p} {d : ℕ} (z : CageOffDiagonalPlanePoint p xi eta d) : Prop

The condition that both coordinates of an off-diagonal plane point are nonzero.

Equations

• BGS.Markoff.IsGoodOffDiagonalPlanePoint z = ((↑z).1 ≠ 0 ∧ (↑z).2 ≠ 0)

def BGS.Markoff.IsGoodOffDiagonalPulledPair {p : ℕ} [Fact (Nat.Prime p)] {xi eta : ZMod p} {d : ℕ} (z : CagePulledRootPair p xi eta d) : Prop

The condition that the two pulled roots have nonzero sum.

Equations

• BGS.Markoff.IsGoodOffDiagonalPulledPair z = (z.firstRoot + z.secondRoot ≠ 0)

def BGS.Markoff.goodOffDiagonalPulledToPlane (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) (d : ℕ) : { z : CagePulledRootPair p xi eta d // IsGoodOffDiagonalPulledPair z } → { z : CageOffDiagonalPlanePoint p xi eta d // IsGoodOffDiagonalPlanePoint z }

The map from a good pulled root pair to its off-diagonal plane point.

Equations

• BGS.Markoff.goodOffDiagonalPulledToPlane p hpTwo xi eta d z = ⟨⟨((↑z).firstRoot + (↑z).secondRoot, ↑(↑z).parameter), ⋯⟩, ⋯⟩

theorem BGS.Markoff.goodOffDiagonalPulledToPlane_bijective (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) (d : ℕ) : Function.Bijective (goodOffDiagonalPulledToPlane p hpTwo xi eta d)

noncomputable def BGS.Markoff.goodOffDiagonalPulledEquivPlane (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) (d : ℕ) : { z : CagePulledRootPair p xi eta d // IsGoodOffDiagonalPulledPair z } ≃ { z : CageOffDiagonalPlanePoint p xi eta d // IsGoodOffDiagonalPlanePoint z }

The equivalence between good pulled pairs and good off-diagonal plane points.

Equations

• BGS.Markoff.goodOffDiagonalPulledEquivPlane p hpTwo xi eta d = Equiv.ofBijective (BGS.Markoff.goodOffDiagonalPulledToPlane p hpTwo xi eta d) ⋯

def BGS.Markoff.badOffDiagonalPulledEmbedding (p : ℕ) [Fact (Nat.Prime p)] (_hpTwo : p ≠ 2) (xi eta : ZMod p) {d : ℕ} (_hd : 0 < d) (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) : { z : CagePulledRootPair p xi eta d // ¬IsGoodOffDiagonalPulledPair z } ↪ (parameter : { t : ZMod p // t ^ (2 * d) = 1 }) × { root : ZMod p // root ^ 2 = Polynomial.eval (↑parameter) (cagePulledRadicand xi d) }

An embedding of bad pulled pairs into the exceptional plane-point set.

Equations

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

theorem BGS.Markoff.badOffDiagonalPulled_card_le (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) {d : ℕ} (hd : 0 < d) (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) : Nat.card { z : CagePulledRootPair p xi eta d // ¬IsGoodOffDiagonalPulledPair z } ≤ 4 * d

noncomputable def BGS.Markoff.cageOffDiagonalZeroParameterPolynomial {K : Type u_1} [Field K] (xi eta : K) (d : ℕ) : Polynomial K

The specialized off-diagonal plane polynomial when its parameter is zero.

Equations

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

theorem BGS.Markoff.eval_cageOffDiagonalZeroParameterPolynomial {K : Type u_1} [Field K] (xi eta sumRoot : K) (d : ℕ) : Polynomial.eval sumRoot (cageOffDiagonalZeroParameterPolynomial xi eta d) = (MvPolynomial.eval ![sumRoot, 0]) (cageOffDiagonalPlanePolynomial xi eta d)

theorem BGS.Markoff.cageOffDiagonalZeroParameterPolynomial_natDegree_le {K : Type u_1} [Field K] (xi eta : K) (d : ℕ) : (cageOffDiagonalZeroParameterPolynomial xi eta d).natDegree ≤ 4

theorem BGS.Markoff.cageOffDiagonalZeroParameterPolynomial_ne_zero {K : Type u_1} [Field K] (xi eta : K) (d : ℕ) : cageOffDiagonalZeroParameterPolynomial xi eta d ≠ 0

def BGS.Markoff.badOffDiagonalPlaneEmbedding (p : ℕ) [Fact (Nat.Prime p)] (xi eta : ZMod p) {d : ℕ} (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) : { z : CageOffDiagonalPlanePoint p xi eta d // ¬IsGoodOffDiagonalPlanePoint z } ↪ { sumRoot : ZMod p // Polynomial.eval sumRoot (cageOffDiagonalZeroParameterPolynomial xi eta d) = 0 } ⊕ { parameter : ZMod p // parameter ^ (2 * d) = 1 }

An embedding of bad off-diagonal plane points into the exceptional set.

Equations

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

theorem BGS.Markoff.badOffDiagonalPlane_card_le (p : ℕ) [Fact (Nat.Prime p)] (xi eta : ZMod p) {d : ℕ} (hd : 0 < d) (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) : Nat.card { z : CageOffDiagonalPlanePoint p xi eta d // ¬IsGoodOffDiagonalPlanePoint z } ≤ 2 * d + 4

theorem BGS.Markoff.cagePulledRootPair_offDiagonal_card_comparison (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) {d : ℕ} (hd : 0 < d) (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) : |↑(Nat.card (CagePulledRootPair p xi eta d)) - ↑(External.affinePlaneCurveZeros (ZMod p) (cageOffDiagonalPlanePolynomial xi eta d)).card| ≤ 6 * ↑d + 4