Documentation

LeanPool.MarkoffModP.BGS.Markoff.ExplicitEstimates

Fixed point-count estimates for explicit strong approximation #

The general affine Hasse--Weil theorem in this repository has coefficient 8. This file records, without existentially choosing any constants, the four numerical specializations used by the explicit Markoff argument.

source
theorem BGS.Markoff.weightedSplitTraceWeilBoundAssumption_thirtyThree :
WeightedSplitTraceWeilBoundAssumption 33

The fixed split trace estimate obtained from affine coefficient 8.

source
theorem BGS.Markoff.seededNonsplitTraceWeilBoundAssumption_thirtyFour :
SeededNonsplitTraceWeilBoundAssumption 34

The fixed nonsplit trace estimate obtained from affine coefficient 8.

source
theorem BGS.Markoff.cagePlanePointEstimate_twoHundredFiftySix :
CagePlanePointEstimate 256

The fixed cage-plane estimate obtained from affine coefficient 8.

source
theorem BGS.Markoff.cageWitnessPointEstimate_oneHundredThousandFiveHundredTwentyTwo :
CageWitnessPointEstimate 100522

The resulting fixed cage-witness estimate.