The nonsplit endgame estimate from the general affine Hasse--Weil theorem

This file applies the single permitted general Hasse--Weil input to the explicit descended plane curve. The identity point omitted by the Cayley chart is kept visible and bounded separately; it is not folded into a specialized estimate assumption.

theorem BGS.Markoff.seededNonsplitTraceWeilBoundAssumption_of_bivariateAffineHasseWeilBound (generalCoefficient : ℕ) (hgeneral : External.BivariateAffineHasseWeilBound generalCoefficient) : SeededNonsplitTraceWeilBoundAssumption (4 * generalCoefficient + 2)

A fixed-coefficient affine Hasse--Weil bound supplies the correspondingly fixed seeded nonsplit estimate. The coefficient 4*C + 2 records the (2d,2e) bidegree and the at-most 2e Cayley-chart boundary.

theorem BGS.Markoff.exists_seededNonsplitTraceWeilBoundAssumption_of_generalHasseWeil (hHasse : External.GeneralBivariateAffineHasseWeilTheorem) : ∃ (coefficient : ℕ), SeededNonsplitTraceWeilBoundAssumption coefficient

The general affine Hasse--Weil theorem supplies the seeded nonsplit estimate.