Documentation

LeanPool.MarkoffModP.BGS.Markoff.Cage.EstimateFromPlane

Transferring plane estimates to the cage witness count #

This file combines the geometric Hasse--Weil estimates, the explicit plane comparison, the exact d-fold power-cover multiplicity, and the all-axis equivalence.

source
theorem BGS.Markoff.cagePulledRadicand_eq_of_sq_eq {K : Type u_1} [Field K] {xi eta : K} (d : ℕ) (h : xi ^ 2 = eta ^ 2) :
cagePulledRadicand xi d = cagePulledRadicand eta d

The pulled cage radicand depends on a trace only through its square.

source
def BGS.Markoff.cagePulledRootPairEquivOfSqEq (p : ℕ) [Fact (Nat.Prime p)] (xi eta eta' : ZMod p) (d : ℕ) (h : eta ^ 2 = eta' ^ 2) :
CagePulledRootPair p xi eta d ≃ CagePulledRootPair p xi eta' d

Replacing either cage trace by another trace with the same square does not change the pulled root-pair cover.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem BGS.Markoff.natCard_cagePulledRootPair_eq_of_sq_eq (p : ℕ) [Fact (Nat.Prime p)] (xi eta eta' : ZMod p) (d : ℕ) (h : eta ^ 2 = eta' ^ 2) :
    Nat.card (CagePulledRootPair p xi eta d) = Nat.card (CagePulledRootPair p xi eta' d)
    source
    theorem BGS.Markoff.canonicalDiagonalCageRangeEstimate (planeCoefficient : ℕ) (hPlane : CagePlanePointEstimate planeCoefficient) (p : ℕ) [Fact (Nat.Prime p)] (hpSeven : 7 ≤ p) (xi : ZMod p) (hxi : IsSplitMaximalTrace p xi) (d : ℕ) (hd : d ∣ Nat.card (ZMod p)ˣ) (hdPositive : 0 < d) :
    |↑(Nat.card (cageMiddleWitnessPowerRangeSolutions p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi xi d)) - 2 * ↑p / ↑d| ≤ ↑(2 * planeCoefficient + 8) * √↑p

    The diagonal plane estimate gives the canonical cage range estimate with the correct geometric multiplicity two.

    source
    theorem BGS.Markoff.canonicalEqualSquareCageRangeEstimate (planeCoefficient : ℕ) (hPlane : CagePlanePointEstimate planeCoefficient) (p : ℕ) [Fact (Nat.Prime p)] (hpSeven : 7 ≤ p) (xi eta : ZMod p) (hxi : IsSplitMaximalTrace p xi) (hsquare : xi ^ 2 = eta ^ 2) (d : ℕ) (hd : d ∣ Nat.card (ZMod p)ˣ) (hdPositive : 0 < d) :
    |↑(Nat.card (cageMiddleWitnessPowerRangeSolutions p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta d)) - 2 * ↑p / ↑d| ≤ ↑(2 * planeCoefficient + 8) * √↑p

    When the two cage traces have the same square, their pulled radicands coincide and the diagonal multiplicity-two estimate applies unchanged.

    source
    theorem BGS.Markoff.canonicalOffDiagonalCageRangeEstimate (planeCoefficient : ℕ) (hPlane : CagePlanePointEstimate planeCoefficient) (p : ℕ) [Fact (Nat.Prime p)] (hpSeven : 7 ≤ p) (xi eta : ZMod p) (hxi : IsSplitMaximalTrace p xi) (heta : IsSplitMaximalTrace p eta) (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) (d : ℕ) (hd : d ∣ Nat.card (ZMod p)ˣ) (hdPositive : 0 < d) :
    |↑(Nat.card (cageMiddleWitnessPowerRangeSolutions p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta d)) - ↑p / ↑d| ≤ ↑(planeCoefficient + 10) * √↑p

    Away from the equal-square diagonal, the primitive quartic plane model has the same main term as the pulled root-pair cover, up to its explicitly bounded exceptional fibers.

    source
    theorem BGS.Markoff.cageWitnessPointEstimate_of_cagePlanePointEstimate (planeCoefficient : ℕ) (hPlane : CagePlanePointEstimate planeCoefficient) :
    CageWitnessPointEstimate (100000 + 2 * planeCoefficient + 10)

    A fixed cage-plane estimate supplies the corresponding fixed witness estimate. The proof chooses the geometric multiplicity only after splitting the genuine equal-square and off-diagonal cases.

    source
    theorem BGS.Markoff.exists_cageWitnessPointEstimate_of_generalHasseWeil (hHasse : External.GeneralBivariateAffineHasseWeilTheorem) :
    ∃ (coefficient : ℕ), 0 < coefficient ∧ CageWitnessPointEstimate coefficient

    The single allowed general affine Hasse--Weil theorem supplies the full cage witness estimate.