The explicit elliptic character sum needed by the incidence argument

This file reduces the needed Legendre character-sum estimate to a narrow point-cardinality target. The target is an explicit proposition parameter, not a sorry or axiom; the selected Theorem 1 route does not use it.

def BGS.FiniteField.ellipticCubicCharacterSum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (u v : F) : ℤ

The quadratic-character trace sum of Y² = X (X - u) (X - v).

Equations

• BGS.FiniteField.ellipticCubicCharacterSum u v = ∑ x : F, (quadraticChar F) (x * (x - u) * (x - v))

def BGS.FiniteField.legendreWeierstrassCurve {F : Type u_1} [Field F] (u v : F) : WeierstrassCurve F

The Weierstrass model Y² = X (X - u) (X - v).

Equations

• BGS.FiniteField.legendreWeierstrassCurve u v = { a₁ := 0, a₂ := -(u + v), a₃ := 0, a₄ := u * v, a₆ := 0 }

theorem BGS.FiniteField.legendreWeierstrassCurve_equation_iff {F : Type u_1} [Field F] (u v x y : F) : (legendreWeierstrassCurve u v).toAffine.Equation x y ↔ y ^ 2 = x * (x - u) * (x - v)

theorem BGS.FiniteField.legendreWeierstrassCurve_discriminant {F : Type u_1} [Field F] (u v : F) : (legendreWeierstrassCurve u v).Δ = 16 * u ^ 2 * v ^ 2 * (u - v) ^ 2

theorem BGS.FiniteField.legendreWeierstrassCurve_discriminant_ne_zero {F : Type u_1} [Field F] {u v : F} (hu : u ≠ 0) (hv : v ≠ 0) (huv : u ≠ v) (hF : ringChar F ≠ 2) : (legendreWeierstrassCurve u v).Δ ≠ 0

def BGS.FiniteField.affineCubicSolutionEquivSigma {F : Type u_1} [Field F] (u v : F) : { xy : F × F // xy.2 ^ 2 = xy.1 * (xy.1 - u) * (xy.1 - v) } ≃ (x : F) × { y : F // y ^ 2 = x * (x - u) * (x - v) }

Affine solutions, rearranged into fibers of the X-coordinate.

Equations

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

def BGS.FiniteField.legendreAffineEquationEquiv {F : Type u_1} [Field F] (u v : F) : { xy : F × F // (legendreWeierstrassCurve u v).toAffine.Equation xy.1 xy.2 } ≃ { xy : F × F // xy.2 ^ 2 = xy.1 * (xy.1 - u) * (xy.1 - v) }

The affine Weierstrass equation is exactly the displayed cubic equation.

Equations

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

theorem BGS.FiniteField.affineCubicSolution_card_eq_card_add_characterSum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (u v : F) : ↑(Fintype.card { xy : F × F // xy.2 ^ 2 = xy.1 * (xy.1 - u) * (xy.1 - v) }) = ↑(Fintype.card F) + ellipticCubicCharacterSum u v

theorem BGS.FiniteField.legendreWeierstrassCurveIsElliptic {F : Type u_1} [Field F] {u v : F} (hF : ringChar F ≠ 2) (hu : u ≠ 0) (hv : v ≠ 0) (huv : u ≠ v) : (legendreWeierstrassCurve u v).IsElliptic

The nonsingularity hypotheses give an honest elliptic-curve instance for the Legendre model.

theorem BGS.FiniteField.legendreWeierstrassCurve_point_card_eq_card_add_one_add_characterSum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {u v : F} (hu : u ≠ 0) (hv : v ≠ 0) (huv : u ≠ v) : ↑(Nat.card (legendreWeierstrassCurve u v).toAffine.Point) = ↑(Fintype.card F) + 1 + ellipticCubicCharacterSum u v

The exact rational-point identity behind the cubic character sum.

theorem BGS.FiniteField.ellipticCubicCharacterSum_eq_point_card_sub_card_sub_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {u v : F} (hu : u ≠ 0) (hv : v ≠ 0) (huv : u ≠ v) : ellipticCubicCharacterSum u v = ↑(Nat.card (legendreWeierstrassCurve u v).toAffine.Point) - ↑(Fintype.card F) - 1

The cubic sum is the negative of the usual Frobenius trace q + 1 - #E(F).

theorem BGS.FiniteField.ellipticCubicCharacterSum_sq_le_four_mul_card_iff_point_card_hasse {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {u v : F} (hu : u ≠ 0) (hv : v ≠ 0) (huv : u ≠ v) : ellipticCubicCharacterSum u v ^ 2 ≤ 4 * ↑(Fintype.card F) ↔ (↑(Nat.card (legendreWeierstrassCurve u v).toAffine.Point) - ↑(Fintype.card F) - 1) ^ 2 ≤ 4 * ↑(Fintype.card F)

The desired character-sum estimate is exactly the Hasse rational-point bound for this model.

def BGS.FiniteField.LegendrePointCardHasseBound (F : Type u_2) [Field F] [Fintype F] : Prop

The exact Legendre-family Hasse target. It is retained only as an explicit premise for the optional incidence-diameter route.

Equations

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

theorem BGS.FiniteField.ellipticCubicCharacterSum_sq_le_four_mul_card {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hHasse : LegendrePointCardHasseBound F) (hF : ringChar F ≠ 2) {u v : F} (hu : u ≠ 0) (hv : v ≠ 0) (huv : u ≠ v) : ellipticCubicCharacterSum u v ^ 2 ≤ 4 * ↑(Fintype.card F)

The exact Hasse character-sum input needed in Proposition 6. Unlike the point-cardinality bound above, this is now a proved reduction rather than a second gap.

theorem BGS.FiniteField.fifteen_sub_card_lt_ellipticCubicCharacterSum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hHasse : LegendrePointCardHasseBound F) (hF : ringChar F ≠ 2) (hcard : 26 ≤ Fintype.card F) {u v : F} (hu : u ≠ 0) (hv : v ≠ 0) (huv : u ≠ v) : 15 - ↑(Fintype.card F) < ellipticCubicCharacterSum u v

For fields of cardinality at least 26, Hasse's square bound is strong enough to leave more than twelve points after the three forbidden fibers are removed.