Hasse--Weil estimates for the direct cage plane models

This file applies the single allowed general affine Hasse--Weil theorem to the two explicit cage models. It also proves that the divisor exponents used by the cage are prime to the characteristic; that condition is not left as a specialized assumption.

def BGS.Markoff.CagePlanePointEstimate (coefficient : ℕ) : Prop

A uniform point estimate for both direct cage plane models.

Equations

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

theorem BGS.Markoff.divisor_pred_lt_prime {p d : ℕ} (hpTwo : 2 ≤ p) (hd : d ∣ p - 1) : d < p

A positive divisor of p-1 is strictly smaller than p.

theorem BGS.Markoff.two_mul_divisor_pred_ne_zero_zmod (p : ℕ) [Fact (Nat.Prime p)] (hpSeven : 7 ≤ p) {d : ℕ} (hd : d ∣ p - 1) (hdPositive : 0 < d) : ↑(2 * d) ≠ 0

The pulled-cover exponent 2d is nonzero in ZMod p for every positive divisor d of p-1 and every prime p ≥ 7.

theorem BGS.Markoff.cagePlanePointEstimate_of_bivariateAffineHasseWeilBound (generalCoefficient : ℕ) (hgeneral : External.BivariateAffineHasseWeilBound generalCoefficient) : CagePlanePointEstimate (32 * generalCoefficient)

A fixed-coefficient affine Hasse--Weil bound gives fixed uniform estimates for both cage plane models.

theorem BGS.Markoff.exists_cagePlanePointEstimate_of_generalHasseWeil (hHasse : External.GeneralBivariateAffineHasseWeilTheorem) : ∃ (coefficient : ℕ), 0 < coefficient ∧ CagePlanePointEstimate coefficient

The allowed general Hasse--Weil theorem gives uniform estimates for both the diagonal and off-diagonal cage plane models.

theorem BGS.Markoff.range_count_error_of_exact_cover {coverCard rangeCard p d multiplicity : ℕ} {error : ℝ} (hd : 0 < d) (hcover : coverCard = d * rangeCard) (herror : |↑coverCard - ↑multiplicity * ↑p| ≤ error * ↑d) : |↑rangeCard - ↑multiplicity * ↑p / ↑d| ≤ error

Divide an exact d-fold cover estimate by its fiber multiplicity. This is the numerical step used after the geometric count comparison.