The brute-force reference

Ratpoints.bruteForce c H lists the normalized points of height at most H on y ^ 2 = F(x, z) by testing every candidate: first (x, z) = (1, 0), the point at infinity, then every coprime pair with 1 ≤ z ≤ H and -H ≤ x ≤ H, by ascending z and, for each z, by ascending x. It is the core of verify-test4.py of the C repository, written in the model (Lean core, no Mathlib); Ratpoints.mem_bruteForce_iff and Ratpoints.nodup_bruteForce prove that it lists exactly the points of the specification, each once. It models no C code, but it evaluates the binary form as the exact check of the C code does: by Horner's rule in x on the products cₖ z^(d - k), computed once per z, with one more factor z when the degree d is odd. For the candidate (1, 0) this gives c_d for even d and 0 for odd d, the value of the form at the point at infinity, so that it needs no case of its own.

Main definitions

• Ratpoints.bruteForce: the points by brute force, in the order described above.

def Ratpoints.BruteForce.degree (c : List Int) : Nat

The degree of the polynomial ∑ cᵢ Xⁱ: the largest index of a nonzero entry of c, or 0 if there is none. The expression of the specification's Ratpoints.degree, which the model cannot import.

Equations

• Ratpoints.BruteForce.degree c = (List.dropWhile (fun (x : Int) => x == 0) c.reverse).length - 1

def Ratpoints.BruteForce.scaledCoeffs (c : List Int) (d : Nat) (z : Int) : List Int

The products cₖ z^(d - k) for k = 0, …, d: the coefficients of the polynomial in x that the exact check of the C code evaluates for the denominator z.

Equations

• Ratpoints.BruteForce.scaledCoeffs c d z = List.map (fun (k : Nat) => c.getD k 0 * z ^ (d - k)) (List.range (d + 1))

def Ratpoints.BruteForce.horner (w : List Int) (x : Int) : Int

Horner's rule: the value w₀ + x (w₁ + x (w₂ + ⋯)) of the polynomial with coefficient list w.

Equations

• Ratpoints.BruteForce.horner w x = List.foldr (fun (a v : Int) => a + x * v) 0 w

def Ratpoints.BruteForce.pointsAbove (x z v : Int) : List (Int × Int × Int)

The triples (x, y, z) with y ^ 2 = v: (x, y, z) and then (x, -y, z) for y = ⌊√v⌋ > 0, the one triple (x, 0, z) for v = 0, and none when v is negative or not a square.

Equations

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

def Ratpoints.BruteForce.pointsOfDen (c : List Int) (d : Nat) (z : Int) (xs : List Int) : List (Int × Int × Int)

The points (x, y, z) with the denominator z and a numerator x from xs coprime to z, for the binary form of degree d of c: the values F(x, z) come by Horner's rule from the products Ratpoints.BruteForce.scaledCoeffs c d z, computed once, and one more factor z when d is odd.

Equations

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

def Ratpoints.BruteForce.numerators (H : Nat) : List Int

The numerators -H, …, H, in ascending order.

Equations

• Ratpoints.BruteForce.numerators H = List.map (fun (i : Nat) => ↑i - ↑H) (List.range (2 * H + 1))

def Ratpoints.bruteForce (c : List Int) (H : Nat) : List (Int × Int × Int)

The normalized points of height at most H on y ^ 2 = F(x, z), by brute force: the candidate (1, 0) if 1 ≤ H, then the pairs (x, z) with 1 ≤ z ≤ H, -H ≤ x ≤ H and gcd(x, z) = 1, by ascending z and then ascending x; for each, (x, y, z) and (x, -y, z) when F(x, z) = y ^ 2 with y > 0, and (x, 0, z) when F(x, z) = 0.

Equations

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

Examples from the C program at the pin (ratpoints c H -q)