The brute-force reference finds exactly the points

Ratpoints.bruteForce c H lists every normalized point of height at most H on y ^ 2 = F(x, z), and nothing else, each once; comparator certifies this (comparator/Challenge.lean).

Main statements

• Ratpoints.mem_bruteForce_iff: a triple lies in Ratpoints.bruteForce c H exactly when it is a normalized point of height at most H.
• Ratpoints.nodup_bruteForce: the list has no duplicates.
• Ratpoints.toFinset_bruteForce: its set of elements is Ratpoints.points c H.
• Ratpoints.bruteForce_eq_append, Ratpoints.filter_bruteForce_eq_append: the list is the points at infinity followed by those of the denominators 1, …, H, and its points at infinity and those of the denominators bLow, …, bHigh are those of these candidates; Ratpoints.filter_bruteForce_eq_self: its points at infinity and those of the denominators 1, …, B for B ≥ H are all its points.
• Ratpoints.ite_pointsAbove_eq_filter: the points of one candidate are those that the specification of the order lists, (x, y, z) before (x, -y, z).

Proof

The evaluation of the model, Horner's rule on the products cₖ z^(d - k) with one more factor z for odd d, is Ratpoints.binaryForm (Ratpoints.BruteForce.horner_scaledCoeffs_mul); v is the square of y exactly when the model's test of ⌊√v⌋ succeeds and y = ±⌊√v⌋ (Ratpoints.BruteForce.mem_pointsAbove_iff); and the candidates are the pairs that the normalization allows. The triples of different candidates differ in x or in z, so the list has no duplicates.

theorem Ratpoints.BruteForce.degree_eq (c : List ℤ) : degree c = Ratpoints.degree c

theorem Ratpoints.BruteForce.horner_eq_sum (w : List ℤ) (x : ℤ) : horner w x = ∑ k ∈ Finset.range w.length, w.getD k 0 * x ^ k

theorem Ratpoints.BruteForce.horner_scaledCoeffs (c : List ℤ) (d : ℕ) (x z : ℤ) : horner (scaledCoeffs c d z) x = ∑ k ∈ Finset.range (d + 1), c.getD k 0 * z ^ (d - k) * x ^ k

theorem Ratpoints.BruteForce.horner_scaledCoeffs_mul (c : List ℤ) (x z : ℤ) : (horner (scaledCoeffs c (degree c) z) x * if degree c % 2 = 1 then z else 1) = binaryForm c x z

theorem Ratpoints.BruteForce.mem_pointsAbove_iff {x z v : ℤ} {p : ℤ × ℤ × ℤ} : p ∈ pointsAbove x z v ↔ p.1 = x ∧ p.2.2 = z ∧ p.2.1 ^ 2 = v

theorem Ratpoints.BruteForce.mem_pointsOfDen_iff {c : List ℤ} {d : ℕ} {z : ℤ} {xs : List ℤ} {p : ℤ × ℤ × ℤ} : p ∈ pointsOfDen c d z xs ↔ p.1 ∈ xs ∧ p.2.2 = z ∧ p.1.gcd z = 1 ∧ p.2.1 ^ 2 = horner (scaledCoeffs c d z) p.1 * if d % 2 = 1 then z else 1

theorem Ratpoints.BruteForce.exists_sq_eq_of_pointsOfDen_ne_nil {c : List ℤ} {b : ℕ} {xs : List ℤ} (h : pointsOfDen c (degree c) (↑b) xs ≠ []) : ∃ a ∈ xs, ∃ (y : ℤ), a.gcd ↑b = 1 ∧ y ^ 2 = binaryForm c a ↑b

theorem Ratpoints.BruteForce.pointsOfDen_filter_of_ne {c : List ℤ} {d : ℕ} {z : ℤ} {xs : List ℤ} {keep : ℤ → Bool} (h : ∀ x ∈ xs, pointsOfDen c d z [x] ≠ [] → keep x = true) : pointsOfDen c d z (List.filter keep xs) = pointsOfDen c d z xs

theorem Ratpoints.BruteForce.pointsOfDen_ne_nil_of_mem {c : List ℤ} {d : ℕ} {z : ℤ} {xs : List ℤ} {x : ℤ} (hx : x ∈ xs) (h : pointsOfDen c d z [x] ≠ []) : pointsOfDen c d z xs ≠ []

theorem Ratpoints.BruteForce.mem_numerators_iff {x : ℤ} {H : ℕ} : x ∈ numerators H ↔ |x| ≤ ↑H

theorem Ratpoints.BruteForce.nodup_pointsAbove (x z v : ℤ) : (pointsAbove x z v).Nodup

theorem Ratpoints.BruteForce.pointsAbove_eq_ite (x z v : ℤ) : pointsAbove x z v = if Int.sqrt v ^ 2 = v then if Int.sqrt v = 0 then [(x, 0, z)] else [(x, Int.sqrt v, z), (x, -Int.sqrt v, z)] else []

The test of Ratpoints.BruteForce.pointsAbove is that ⌊√v⌋ ^ 2 = v, with Int.sqrt.

theorem Ratpoints.BruteForce.nodup_numerators (H : ℕ) : (numerators H).Nodup

theorem Ratpoints.BruteForce.nodup_pointsOfDen (c : List ℤ) (d : ℕ) (z : ℤ) {xs : List ℤ} (hxs : xs.Nodup) : (pointsOfDen c d z xs).Nodup

theorem Ratpoints.mem_bruteForce_iff {c : List ℤ} {H : ℕ} {p : ℤ × ℤ × ℤ} : p ∈ bruteForce c H ↔ IsPoint c H p

The brute-force reference lists exactly the normalized points of height at most H, for every coefficient list and every height; comparator certifies this (comparator/Challenge.lean).

theorem Ratpoints.nodup_bruteForce (c : List ℤ) (H : ℕ) : (bruteForce c H).Nodup

The brute-force reference lists each point once; comparator certifies this (comparator/Challenge.lean).

theorem Ratpoints.toFinset_bruteForce (c : List ℤ) (H : ℕ) : (bruteForce c H).toFinset = points c H

theorem Ratpoints.bruteForce_eq_append (c : List ℤ) {H : ℕ} (hH : 1 ≤ H) : bruteForce c H = BruteForce.pointsOfDen c (degree c) 0 [1] ++ List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c (degree c) (↑b) (BruteForce.numerators H)) (List.range' 1 H)

The reference with its points at infinity apart, for H ≥ 1.

theorem Ratpoints.filter_bruteForce_eq_append (c : List ℤ) {H bLow bHigh : ℕ} (hH : 1 ≤ H) (hbLow : 1 ≤ bLow) (hbH : bHigh ≤ H) : List.filter (fun (p : ℤ × ℤ × ℤ) => decide (p.2.2 = 0 ∨ ↑bLow ≤ p.2.2 ∧ p.2.2 ≤ ↑bHigh)) (bruteForce c H) = BruteForce.pointsOfDen c (degree c) 0 [1] ++ List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c (degree c) (↑b) (BruteForce.numerators H)) (List.range' bLow (bHigh + 1 - bLow))

The points of the reference with the denominators from bLow ≥ 1 to bHigh ≤ H, and its points at infinity, are those of these denominators, in increasing order.

theorem Ratpoints.filter_bruteForce_eq_self (c : List ℤ) {H B : ℕ} (hB : H ≤ B) : List.filter (fun (p : ℤ × ℤ × ℤ) => decide (p.2.2 = 0 ∨ 1 ≤ p.2.2 ∧ p.2.2 ≤ ↑B)) (bruteForce c H) = bruteForce c H

The points of height at most H with a denominator of at most B ≥ H are all of them.

The points of one candidate, as the specification of the order lists them

theorem Ratpoints.isPoint_iff_of_le {c : List ℤ} {H : ℕ} {x y z : ℤ} (hn : 0 < z ∨ z = 0 ∧ x = 1) (hx : |x| ≤ ↑H) (hz : z ≤ ↑H) : IsPoint c H (x, y, z) ↔ y ^ 2 = binaryForm c x z ∧ x.gcd z = 1

A triple whose (x, z) is normalized and of height at most H is a point exactly when y ^ 2 = F(x, z) and gcd(x, z) = 1.

theorem Ratpoints.ite_pointsAbove_eq_filter {c : List ℤ} {H : ℕ} {x z : ℤ} (hn : 0 < z ∨ z = 0 ∧ x = 1) (hx : |x| ≤ ↑H) (hz : z ≤ ↑H) : (if x.gcd z = 1 then BruteForce.pointsAbove x z (binaryForm c x z) else []) = List.filter (fun (b : ℤ × ℤ × ℤ) => decide (IsPoint c H b)) (if Int.sqrt (binaryForm c x z) = 0 then [(x, 0, z)] else [(x, Int.sqrt (binaryForm c x z), z), (x, -Int.sqrt (binaryForm c x z), z)])

The points of the brute-force reference over the candidate (x, z), normalized and of height at most H, are those of the specification of the order (Ratpoints.pointsWithDen): (x, y, z) and then (x, -y, z) for y = ⌊√F(x, z)⌋, as far as they are points, one when y = 0.

The axioms of the main theorems