Numerical transfer from normalization counts to affine counts

The geometric comparison between an affine plane curve and its normalization is naturally expressed by two inequalities between natural-number cardinalities. This file isolates the real absolute-value bookkeeping needed to combine those inequalities with the closed Hasse--Weil bound.

theorem BGS.HasseWeil.abs_affine_sub_card_le_of_two_sided_count_comparison (affine normalization fieldCard error : ℕ) (upper : affine ≤ normalization + error) (lower : normalization ≤ affine + error) (bound : ℝ) (hnormalization : |↑normalization - ↑fieldCard - 1| ≤ bound) : |↑affine - ↑fieldCard| ≤ bound + ↑error + 1

If the affine and normalization counts differ by at most error in both directions, then a Hasse--Weil bound for the normalization transfers to the affine count, with the affine/projective constant 1 and error added.

theorem BGS.HasseWeil.abs_pointCount_sub_card_le_two_mul_sqrt_of_fiber_bound (pointCount fieldCard smallDegree largeDegree : ℕ) (hsmall : 0 < smallDegree) (hcount : pointCount ≤ fieldCard * smallDegree) (hlarge : √↑fieldCard ≤ ↑largeDegree) : |↑pointCount - ↑fieldCard| ≤ 2 * √↑fieldCard * ↑smallDegree * ↑largeDegree

Large-degree branch of the affine estimate. A trivial fiber bound by fieldCard * smallDegree already has Hasse--Weil scale whenever the other coordinate degree is at least sqrt fieldCard.

theorem BGS.HasseWeil.criticalCount_le_two_mul_sqrt (criticalCount fieldCard firstDegree secondDegree : ℕ) (hcritical : criticalCount ≤ (2 * secondDegree - 1) * firstDegree * secondDegree) (hsecond : ↑secondDegree ≤ √↑fieldCard) : ↑criticalCount ≤ 2 * √↑fieldCard * ↑firstDegree * ↑secondDegree

In the small-degree branch, the explicit resultant bound for the second-coordinate critical locus is already of Hasse--Weil scale.

theorem BGS.HasseWeil.zetaDegree_mul_sqrt_le_three_mul_bidegree (zetaDegree fieldCard firstDegree secondDegree : ℕ) (hfirst : 0 < firstDegree) (hsecond : 0 < secondDegree) (hdegree : zetaDegree ≤ 2 * ((firstDegree - 1) * (secondDegree - 1)) + 1) : ↑zetaDegree * √↑fieldCard ≤ 3 * √↑fieldCard * ↑firstDegree * ↑secondDegree

The coarse zeta numerator degree budget is bounded by three times the bidegree product, which is sufficient for a universal affine coefficient.

theorem BGS.HasseWeil.one_le_sqrt_mul_bidegree (fieldCard firstDegree secondDegree : ℕ) (hfield : 1 ≤ fieldCard) (hfirst : 0 < firstDegree) (hsecond : 0 < secondDegree) : 1 ≤ √↑fieldCard * ↑firstDegree * ↑secondDegree

The constant affine/projective correction 1 is absorbed by the square-root bidegree scale over every nontrivial finite field.