The specification

The points that ratpoints finds, for a coefficient list c (constant term first) and a height bound H: the binary form F of c and the normalized points (x, y, z) of height at most H on y ^ 2 = F(x, z); and the binary form over ℚ that the refusals of the program speak about. The specification uses Mathlib and nothing of the model, so that it can be read on its own; the comparator challenge restates Ratpoints.degree, Ratpoints.binaryForm, Ratpoints.IsNormalizedPair, Ratpoints.IsPoint and Ratpoints.binaryFormPoly verbatim.

Main definitions

• Ratpoints.degree: the degree of the polynomial with coefficient list c.
• Ratpoints.binaryForm: the binary form F(x, z) of even degree that the program evaluates.
• Ratpoints.binaryFormPoly: the binary form over ℚ of degree 2 ⌈n / 2⌉, where n + 1 is the length of c, whose squarefreeness decides the refusals.
• Ratpoints.IsNormalizedPair: the pair (x, z) is normalized and of height at most H.
• Ratpoints.IsPoint: (x, y, z) is a normalized point of height at most H.
• Ratpoints.points: the finite set of these points.

Main statements

• Ratpoints.eval_binaryFormPoly: on every input that the program does not refuse, the two forms agree.
• Ratpoints.finite_setOf_isPoint, Ratpoints.mem_points: the points form a finite set.

Implementation notes

The coefficients are written c.getD i 0: Mathlib's notation c[...] for cycles makes c[i] fail for a list named c wherever all of Mathlib is imported.

The file imports Mathlib.Algebra.Squarefree.Basic, which its definitions do not need, for the refusal theorems, which say that Ratpoints.binaryFormPoly c is not Squarefree: the comparator challenge imports, besides the model, which uses no Mathlib, exactly the Mathlib modules among the public imports of the files of the specification that it restates (this file, Ratpoints.Spec.Order, Ratpoints.Spec.Region and Ratpoints.Spec.Sturm), so that the definitions that it restates elaborate to the same terms as here.

def Ratpoints.degree (c : List ℤ) : ℕ

The degree of the polynomial ∑ cᵢ Xⁱ: the largest index of a nonzero entry of c, or 0 if there is none.

Equations

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

def Ratpoints.binaryForm (c : List ℤ) (x z : ℤ) : ℤ

The binary form F(x, z) = ∑ cᵢ xⁱ z^(D - i) of even degree D = d + d % 2 of the polynomial of degree d with coefficient list c.

Equations

• Ratpoints.binaryForm c x z = ∑ i ∈ Finset.range (Ratpoints.degree c + 1), c.getD i 0 * x ^ i * z ^ (Ratpoints.degree c + Ratpoints.degree c % 2 - i)

noncomputable def Ratpoints.binaryFormPoly (c : List ℤ) : MvPolynomial (Fin 2) ℚ

The binary form Φ = ∑ cᵢ Xⁱ Z^(N - i) over ℚ of degree N = 2 ⌈n / 2⌉, where n + 1 is the length of c: the polynomial made homogeneous of the even degree that the length of its coefficient list allows. The refusals of the program speak about this form; on every input that is not refused, it agrees with Ratpoints.binaryForm (Ratpoints.eval_binaryFormPoly).

Equations

• Ratpoints.binaryFormPoly c = ∑ i ∈ Finset.range c.length, MvPolynomial.C ↑(c.getD i 0) * MvPolynomial.X 0 ^ i * MvPolynomial.X 1 ^ (2 * (c.length / 2) - i)

theorem Ratpoints.degree_def (c : List ℤ) : degree c = (List.dropWhile (fun (x : ℤ) => x == 0) c.reverse).length - 1

@[simp]

theorem Ratpoints.degree_nil : degree [] = 0

theorem Ratpoints.degree_le_length_sub_one (c : List ℤ) : degree c ≤ c.length - 1

theorem Ratpoints.getD_eq_zero_of_degree_lt {c : List ℤ} {i : ℕ} (hi : degree c < i) : c.getD i 0 = 0

theorem Ratpoints.eval_binaryFormPoly {c : List ℤ} (h : c.length / 2 ≤ (degree c + 1) / 2) (x z : ℤ) : (MvPolynomial.eval ![↑x, ↑z]) (binaryFormPoly c) = ↑(binaryForm c x z)

On every input that the program does not refuse, Ratpoints.binaryFormPoly evaluates to Ratpoints.binaryForm: the hypothesis, ⌈n / 2⌉ ≤ ⌈d / 2⌉, makes the two degrees equal.

def Ratpoints.IsNormalizedPair (H : ℕ) (x z : ℤ) : Prop

The pair (x, z) is normalized and of height at most H, as the program prints the points: gcd(x, z) = 1, 0 < z or (x, z) = (1, 0), |x| ≤ H and z ≤ H. So is the pair (x, z) of every triple (x, 0, z) that the program prints under RATPOINTS_NO_CHECK, whether the triple is a point or not.

Equations

• Ratpoints.IsNormalizedPair H x z = (x.gcd z = 1 ∧ (0 < z ∨ z = 0 ∧ x = 1) ∧ |x| ≤ ↑H ∧ z ≤ ↑H)

@[instance_reducible]

instance Ratpoints.instDecidableIsNormalizedPair (H : ℕ) (x z : ℤ) : Decidable (IsNormalizedPair H x z)

Equations

• Ratpoints.instDecidableIsNormalizedPair H x z = { decide := decide (x.gcd z = 1) && decide ((0 < z ∨ z = 0 ∧ x = 1) ∧ |x| ≤ ↑H ∧ z ≤ ↑H), reflects_decide := ⋯ }

def Ratpoints.IsPoint (c : List ℤ) (H : ℕ) (p : ℤ × ℤ × ℤ) : Prop

(x, y, z) is a point of height at most H on y ^ 2 = F(x, z), F = Ratpoints.binaryForm c, normalized as the program prints it: the equation holds, and (x, z) is normalized and of height at most H (Ratpoints.IsNormalizedPair).

Equations

• Ratpoints.IsPoint c H p = (p.2.1 ^ 2 = Ratpoints.binaryForm c p.1 p.2.2 ∧ Ratpoints.IsNormalizedPair H p.1 p.2.2)

@[instance_reducible]

instance Ratpoints.instDecidablePredIsPoint (c : List ℤ) (H : ℕ) : DecidablePred (IsPoint c H)

Equations

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

theorem Ratpoints.finite_setOf_isPoint (c : List ℤ) (H : ℕ) : {p : ℤ × ℤ × ℤ | IsPoint c H p}.Finite

noncomputable def Ratpoints.points (c : List ℤ) (H : ℕ) : Finset (ℤ × ℤ × ℤ)

The finite set of the normalized points of height at most H on y ^ 2 = F(x, z).

Equations

• Ratpoints.points c H = ⋯.toFinset

@[simp]

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

Points from the program's output, checked by decide