Endgame point estimates after quotienting by the power maps

The Weil interfaces count points on the power-cover curves. The paper's inclusion--exclusion argument instead counts solutions on the two power-map images. This file connects those two levels exactly. It proves the source's division by d * e, then divides the point-count error by the same positive factor to obtain the uniform O(sqrt q) error used in equations (34)--(36).

Both split and corrected seeded nonsplit branches are covered. The nonsplit equivalence uses the actual base-field solution finset on the norm-one torus; it never replaces that finset by all quadratic-field points.

theorem BGS.Markoff.rangeCount_error_le_of_coverCount_error_and_exactMultiplicity (coverCount rangeCount fieldCard coefficient d e : ℕ) (hd : 0 < d) (he : 0 < e) (hcover : coverCount = d * e * rangeCount) (herror : |↑coverCount - ↑fieldCard| ≤ ↑coefficient * √↑fieldCard * ↑d * ↑e) : |↑rangeCount - ↑fieldCard / (↑d * ↑e)| ≤ ↑coefficient * √↑fieldCard

Dividing an exact d * e-sheeted cover count divides its Weil error by the same factor.

@[reducible, inline]

abbrev BGS.Markoff.splitTracePowerRangeSolutions (K : Type) [Field K] (alpha beta : K) (d e : ℕ) : Type

Solutions on the two power-map images for the weighted split trace equation.

Equations

• BGS.Markoff.splitTracePowerRangeSolutions K alpha beta d e = BGS.Markoff.powerTraceRangeSolutions BGS.Markoff.splitTorusTrace (BGS.Markoff.weightedSplitTorusTrace alpha beta) d e

def BGS.Markoff.splitTraceCurveSolutionsEquivPowerTraceCoverSolutions (K : Type) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) : ↥(splitTraceCurveSolutions K alpha beta d e) ≃ powerTraceCoverSolutions splitTorusTrace (weightedSplitTorusTrace alpha beta) d e

The finite-set model of the split trace cover is definitionally the same equation as the generic two-power cover, up to reversing the displayed equality.

Equations

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

theorem BGS.Markoff.splitTraceCurveSolutions_card_eq_mul_natCard_powerTraceRangeSolutions (K : Type) [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (d e : ℕ) (hdvd : d ∣ Nat.card Kˣ) (hedvd : e ∣ Nat.card Kˣ) : (splitTraceCurveSolutions K alpha beta d e).card = d * e * Nat.card (splitTracePowerRangeSolutions K alpha beta d e)

Exact source equation (32) for the split trace cover.

theorem BGS.Markoff.splitTracePowerRangeSolutions_count_error_le_of_weilBoundAssumption (K : Type) [Field K] [Fintype K] (coefficient : ℕ) (hWeil : WeightedSplitTraceWeilBoundAssumption coefficient) (alpha beta : K) (d e : ℕ) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) (hd : 0 < d) (he : 0 < e) (heChar : ↑e ≠ 0) (hdvd : d ∣ Nat.card Kˣ) (hedvd : e ∣ Nat.card Kˣ) : |↑(Nat.card (splitTracePowerRangeSolutions K alpha beta d e)) - ↑(Fintype.card K) / (↑d * ↑e)| ≤ ↑coefficient * √↑(Fintype.card K)

Equation (34) for a concrete weighted split trace cover, derived from the explicit Weil assumption only after Lean proves the cover's absolute irreducibility.

noncomputable def BGS.Markoff.existingConicSeedNonsplitTorusTrace (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (w : ↥(quadraticNormOneTorus p)) : ZMod p

The unpowered left trace in the corrected seeded nonsplit equation.

Equations

• BGS.Markoff.existingConicSeedNonsplitTorusTrace p t ht ht0 s w = (Algebra.trace (ZMod p) (BGS.Markoff.quadraticFiniteField p)) (↑↑s * ↑↑w)

@[reducible, inline]

abbrev BGS.Markoff.existingConicSeedNonsplitPowerRangeSolutions (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (d e : ℕ) : Type

Solutions on the two power-map images for the corrected seeded nonsplit equation.

Equations

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

def BGS.Markoff.existingConicSeedNonsplitTraceCurveSolutionsEquivPowerTraceCoverSolutions (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (d e : ℕ) : ↥(existingConicSeedNonsplitTraceCurveSolutions p t ht ht0 s d e) ≃ powerTraceCoverSolutions (existingConicSeedNonsplitTorusTrace p t ht ht0 s) splitTorusTrace d e

The corrected nonsplit solution finset is exactly the corresponding generic two-power cover over the norm-one torus and the base-field unit group.

Equations

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

theorem BGS.Markoff.existingConicSeedNonsplitTraceCurveSolutions_card_eq_mul_natCard_powerTraceRangeSolutions (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (d e : ℕ) (hdvd : d ∣ Nat.card ↥(quadraticNormOneTorus p)) (hedvd : e ∣ Nat.card (ZMod p)ˣ) : (existingConicSeedNonsplitTraceCurveSolutions p t ht ht0 s d e).card = d * e * Nat.card (existingConicSeedNonsplitPowerRangeSolutions p t ht ht0 s d e)

Exact source equation (32) for the corrected seeded nonsplit trace cover.

theorem BGS.Markoff.existingConicSeedNonsplitPowerRangeSolutions_count_error_le_of_weilBoundAssumption (p : ℕ) [Fact (Nat.Prime p)] (coefficient : ℕ) (hWeil : SeededNonsplitTraceWeilBoundAssumption coefficient) (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (d e : ℕ) (hd : 0 < d) (he : 0 < e) (hdChar : ↑d ≠ 0) (hdvd : d ∣ Nat.card ↥(quadraticNormOneTorus p)) (hedvd : e ∣ Nat.card (ZMod p)ˣ) : |↑(Nat.card (existingConicSeedNonsplitPowerRangeSolutions p t ht ht0 s d e)) - ↑p / (↑d * ↑e)| ≤ ↑coefficient * √↑p

Equation (34) for the corrected seeded nonsplit cover. Its main term is p / (d * e) because the counted solution set is over the base field.