The set-up of a search: the polynomial of a coefficient list, the remainder chain, the reversal

The C code works with the polynomial f = ∑ cᵢ Xⁱ of the coefficient list c and its degree d, the refusals speak about the binary form Φ_c of degree N = 2 ⌈n / 2⌉ (Ratpoints.binaryFormPoly), where n + 1 is the length of c. Φ_c is the homogenization of f of degree N, so it is squarefree exactly when f is squarefree and N ≤ d + 1: the two conditions that the C code tests, the second when it drops the leading zeros, the first with the remainder chain of its Sturm step. The rows of the chain, as polynomials over ℚ, form a generalized Sturm sequence, positive rational multiples of the entries of Mathlib's Polynomial.sturmSeq, along which the coprimality of f and f' passes down to the last two rows, so that the chain detects a repeated factor of f. In each of its three cases the reversal check replaces c by its reflection in the even degree D = d + d % 2 of the binary form, which exchanges x and z in the binary form and so does not change whether it is squarefree, and its refusal, of c₀ = c₁ = 0 for even d, stands for X ^ 2 ∣ Φ_c; so once the test of the leading zeros has passed, the remainder chain of the polynomial that the check hands on detects exactly the forms that are not squarefree. The map of the points of the reversed curve to those of the caller's curve (Ratpoints.Sieve.swapPoint) is a bijection between the points of height at most H.

Main definitions

• Ratpoints.poly: the polynomial f = ∑ cᵢ Xⁱ over ℚ of a coefficient list c.

Main statements

• Ratpoints.getD_degree_ne_zero_of_pos, Ratpoints.natDegree_poly: the entry of c at a positive degree is not zero, and the degree of f is Ratpoints.degree c.
• Ratpoints.poly_take_of_degree_lt: the entries of c above its degree do not change f.
• Ratpoints.binaryForm_eq_mul_eval: F(a, b) = b ^ D f(a / b) for b ≠ 0, with the even degree D = d + d % 2.
• Ratpoints.binaryFormPoly_eq_homogenize: Φ_c is the homogenization of f of degree N.
• Ratpoints.squarefree_binaryFormPoly_iff: Φ_c is squarefree if and only if f is squarefree and N ≤ d + 1.
• Ratpoints.not_squarefree_binaryFormPoly_of_lt, Ratpoints.not_squarefree_binaryFormPoly_of_getD_zero: a drop of ⌈n / 2⌉ by the leading zeros, and c₀ = c₁ = 0, leave a form that is not squarefree.
• Ratpoints.Sturm.IsChain.exists_mul_eq, Ratpoints.Sturm.IsChain.natDegree_lt: three consecutive rows s_k, s_(k+1), s_(k+2) of a remainder chain satisfy A s_k = Q s_(k+1) - g s_(k+2) with integers A, g > 0, and the degrees decrease from f' on.
• Ratpoints.Sturm.run_chain_eq_none_iff: for d ≥ 1 and c_d ≠ 0, the remainder chain of the model is none exactly when the polynomial of c₀, …, c_d is not squarefree.
• Ratpoints.Setup.getD_eq_of_reversal_eq_ok, Ratpoints.Setup.binaryForm_eq_of_reversal_eq_ok: the list that the reversal check reverses c to is the reflection of c in the degree D, and its binary form is that of c with x and z exchanged.
• Ratpoints.Setup.degree_eq_of_reversal_eq_ok, Ratpoints.Setup.eq_of_reversal_eq_ok_false: the degree that the check returns is that of the list it returns, and without a reversal these are c and its degree.
• Ratpoints.Setup.one_le_of_reversal_eq_ok, Ratpoints.Setup.degree_le_of_reversal_eq_ok: the check keeps the degree at least 1, and does not raise it.
• Ratpoints.Setup.squarefree_binaryFormPoly_iff_of_reversal_eq_ok: once the test of the leading zeros has passed, Φ_c is squarefree exactly when the polynomial that the check hands on is.
• Ratpoints.Setup.exists_reversal_eq_error_iff, Ratpoints.Setup.not_squarefree_binaryFormPoly_of_reversal_eq_error: the check refuses exactly the even degrees with c₀ = c₁ = 0 when its switch lets it run, and only forms that are not squarefree.
• Ratpoints.Sturm.run_chain_eq_none_iff_of_reversal_eq_ok: once the test of the leading zeros has passed, the remainder chain of the polynomial that the check hands on is none exactly when Φ_c is not squarefree.
• Ratpoints.Sieve.isPoint_swapPoint, Ratpoints.Sieve.perm_map_swapPoint_bruteForce: the map of a reversed search sends the points of the reversed curve to points of the caller's curve, and the brute-force reference of the one, mapped, is a permutation of that of the other.
• Ratpoints.IsNormalizedPair.swapPoint, Ratpoints.Sieve.swapPoint_inj: the map keeps the pairs (x, z) of normalized points of height at most H (Ratpoints.IsNormalizedPair), with or without the equation, and it is injective on the normalized triples.

noncomputable def Ratpoints.poly (c : List ℤ) : Polynomial ℚ

The polynomial f = ∑ cᵢ Xⁱ over ℚ with the coefficient list c, constant term first, which the C code works with; Ratpoints.binaryFormPoly c is its homogenization of degree 2 ⌈n / 2⌉, where n + 1 is the length of c (Ratpoints.binaryFormPoly_eq_homogenize). Mathlib's Polynomial.ofCoeffList builds the same polynomial from the list c.map (↑); the sum here has the shape of Ratpoints.binaryFormPoly, so that Ratpoints.binaryFormPoly_eq_homogenize holds term by term.

Equations

• Ratpoints.poly c = ∑ i ∈ Finset.range c.length, Polynomial.C ↑(c.getD i 0) * Polynomial.X ^ i

@[simp]

theorem Ratpoints.coeff_poly (c : List ℤ) (i : ℕ) : (poly c).coeff i = ↑(c.getD i 0)

theorem Ratpoints.getD_degree_ne_zero_of_pos {c : List ℤ} (h : 0 < degree c) : c.getD (degree c) 0 ≠ 0

theorem Ratpoints.natDegree_poly (c : List ℤ) : (poly c).natDegree = degree c

theorem Ratpoints.poly_take_of_degree_lt {c : List ℤ} {n : ℕ} (h : degree c < n) : poly (List.take n c) = poly c

The entries of c above its degree are zero, so dropping them does not change the polynomial Ratpoints.poly c; with n = d + 1 for the degree d of c, this turns the polynomial of Ratpoints.Sturm.run_chain_eq_none_iff into Ratpoints.poly c.

theorem Ratpoints.binaryForm_eq_mul_eval {c : List ℤ} (a : ℤ) {b : ℤ} (hb : b ≠ 0) : ↑(binaryForm c a b) = ↑b ^ (degree c + degree c % 2) * Polynomial.eval (↑a / ↑b) (poly c)

The binary form of c at (a, b), b ≠ 0, is b ^ D times the value of the polynomial of c at a / b, D = d + d % 2 its even degree.

theorem Ratpoints.binaryFormPoly_eq_homogenize (c : List ℤ) : binaryFormPoly c = (poly c).homogenize (2 * (c.length / 2))

theorem Ratpoints.squarefree_binaryFormPoly_iff (c : List ℤ) : Squarefree (binaryFormPoly c) ↔ Squarefree (poly c) ∧ 2 * (c.length / 2) ≤ degree c + 1

The binary form Ratpoints.binaryFormPoly c is squarefree exactly when the polynomial Ratpoints.poly c is squarefree and the degree 2 ⌈n / 2⌉ of the form, n + 1 the length of c, exceeds the degree of the polynomial by at most one: the two conditions that the C code tests, the second when it drops the leading zeros, the first with the remainder chain of its Sturm step.

theorem Ratpoints.not_squarefree_binaryFormPoly_of_lt {c : List ℤ} (h : (degree c + 1) / 2 < c.length / 2) : ¬Squarefree (binaryFormPoly c)

When the leading zeros of c lower ⌈n / 2⌉, for n + 1 the length of c, the square of the second variable divides the binary form Ratpoints.binaryFormPoly c.

theorem Ratpoints.not_squarefree_binaryFormPoly_of_getD_zero {c : List ℤ} (h0 : c.getD 0 0 = 0) (h1 : c.getD 1 0 = 0) : ¬Squarefree (binaryFormPoly c)

With c₀ = c₁ = 0, the square of the first variable divides the binary form Ratpoints.binaryFormPoly c, whatever the degree, the zero polynomial included.

The polynomial of an array

theorem Ratpoints.coeff_poly_toList (a : Array ℤ) (i : ℕ) : (poly a.toList).coeff i = ↑a[i]!

theorem Ratpoints.natDegree_poly_toList {a : Array ℤ} (h : a.back! ≠ 0) : (poly a.toList).natDegree = a.size - 1

theorem Ratpoints.leadingCoeff_poly_toList {a : Array ℤ} (h : a.back! ≠ 0) : (poly a.toList).leadingCoeff = ↑a.back!

The steps of the chain as polynomials

Remainder chains

theorem Ratpoints.Sturm.IsChain.poly_toList_getElem!_zero {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) : poly ch[0]!.toList = poly (List.take (d + 1) c)

theorem Ratpoints.Sturm.IsChain.poly_toList_getElem!_one {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) : poly ch[1]!.toList = Polynomial.derivative (poly ch[0]!.toList)

theorem Ratpoints.Sturm.IsChain.exists_mul_eq {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) {k : ℕ} (hk : k + 2 < ch.size) : ∃ (A : ℤ) (g : ℤ), 0 < A ∧ 0 < g ∧ ∃ (Q : Polynomial ℚ), Polynomial.C ↑A * poly ch[k]!.toList = Q * poly ch[k + 1]!.toList - Polynomial.C ↑g * poly ch[k + 2]!.toList

Three consecutive rows s_k, s_(k+1), s_(k+2) of a remainder chain satisfy A s_k = Q s_(k+1) - g s_(k+2) with integers A, g > 0, the relation of a generalized Sturm sequence; compare Mathlib's Polynomial.sturmSeq, which has A = g = 1 and Q the quotient (Polynomial.sturmSeq_cons): the integer factors keep the rows integral, and the rows are positive rational multiples of its entries.

theorem Ratpoints.Sturm.IsChain.natDegree_lt {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) {k : ℕ} (hk : k + 2 < ch.size) : (poly ch[k + 2]!.toList).natDegree < (poly ch[k + 1]!.toList).natDegree

theorem Ratpoints.Sturm.run_chain_eq_none_iff {c : List ℤ} {d : ℕ} (hd : 1 ≤ d) (hc : c.getD d 0 ≠ 0) : (chain c d).run = none ↔ ¬Squarefree (poly (List.take (d + 1) c))

For the coefficients c₀, …, c_d of a polynomial f of degree d ≥ 1, the remainder chain is none, where sturm.c returns -1, exactly when f is not squarefree over ℚ; for the degree d of c, f is Ratpoints.poly c (Ratpoints.poly_take_of_degree_lt).

The reversal

theorem Ratpoints.binaryForm_eq_of_getD_eq_getD_sub {c c' : List ℤ} {N : ℕ} (hN : degree c + degree c % 2 = N) (hN' : degree c' + degree c' % 2 = N) (h : ∀ i ≤ N, c'.getD i 0 = c.getD (N - i) 0) (x z : ℤ) : binaryForm c' x z = binaryForm c z x

Two lists whose degrees round up to the same even number N and whose entries are reflected at N have binary forms with x and z exchanged.

theorem Ratpoints.Setup.isSquare_eq_true_iff (a : ℤ) : isSquare a = true ↔ IsSquare a

The square test of the set-up, as GMP decides it, is IsSquare.

theorem Ratpoints.Setup.isSquare_eq_false_iff (a : ℤ) : isSquare a = false ↔ ¬IsSquare a

@[simp]

theorem Ratpoints.Setup.reversal_false (c : List ℤ) (d : ℕ) : reversal false c d = Except.ok (c, d, false)

theorem Ratpoints.Setup.getD_eq_of_reversal_eq_ok {allow : Bool} {c c' : List ℤ} {d' : ℕ} (h : reversal allow c (degree c) = Except.ok (c', d', true)) (i : ℕ) : c'.getD i 0 = if i ≤ degree c + degree c % 2 then c.getD (degree c + degree c % 2 - i) 0 else 0

In each of the three cases of the reversal check Ratpoints.Setup.reversal, the reversed list is the reflection of c in the even degree d + d % 2 of the binary form (with c_(d+1) = 0 in its third case, of odd d).

theorem Ratpoints.Setup.eq_of_reversal_eq_ok_false {allow : Bool} {c c' : List ℤ} {d d' : ℕ} (h : reversal allow c d = Except.ok (c', d', false)) : c' = c ∧ d' = d

theorem Ratpoints.Setup.exists_reversal_eq_error_iff {allow : Bool} {c : List ℤ} {d : ℕ} : (∃ (e : Refusal), reversal allow c d = Except.error e) ↔ allow = true ∧ d % 2 = 0 ∧ c.getD 0 0 = 0 ∧ c.getD 1 0 = 0

theorem Ratpoints.Setup.degree_eq_of_reversal_eq_ok {allow rev : Bool} {c c' : List ℤ} {d' : ℕ} (h : reversal allow c (degree c) = Except.ok (c', d', rev)) : degree c' = d'

The new leading coefficient of a reversal by Ratpoints.Setup.reversal, c₁ when c₀ = 0 and c₀ otherwise, is not zero, so the degree that the check returns is that of its list, also without a reversal.

theorem Ratpoints.Setup.one_le_of_reversal_eq_ok {allow rev : Bool} {c c' : List ℤ} {d d' : ℕ} (h : reversal allow c d = Except.ok (c', d', rev)) (h1 : 1 ≤ d) : 1 ≤ d'

The reversal check Ratpoints.Setup.reversal keeps the degree at least 1: it lowers only an even degree d ≥ 2, to d - 1, when c₀ = 0, and keeps it otherwise.

theorem Ratpoints.Setup.degree_le_of_reversal_eq_ok {allow rev : Bool} {c c' : List ℤ} {d d' : ℕ} (h : reversal allow c d = Except.ok (c', d', rev)) : d' ≤ d

The reversal check Ratpoints.Setup.reversal does not raise the degree: it lowers only an even degree d ≥ 2, to d - 1, when c₀ = 0, and keeps it otherwise.

theorem Ratpoints.Setup.binaryForm_eq_of_reversal_eq_ok {allow : Bool} {c c' : List ℤ} {d' : ℕ} (h : reversal allow c (degree c) = Except.ok (c', d', true)) (x z : ℤ) : binaryForm c' x z = binaryForm c z x

The binary form of the reversed list is that of c with x and z exchanged, since the list is the reflection of c in the even degree d + d % 2 of the binary form.

theorem Ratpoints.Setup.squarefree_binaryFormPoly_iff_of_reversal_eq_ok {allow rev : Bool} {c c' : List ℤ} {d' : ℕ} (hc : c.length / 2 ≤ (degree c + 1) / 2) (h : reversal allow c (degree c) = Except.ok (c', d', rev)) : Squarefree (binaryFormPoly c) ↔ Squarefree (poly c')

Once the test of the leading zeros has passed, the binary form Ratpoints.binaryFormPoly c is squarefree exactly when the polynomial of the list that the reversal check hands on is, whether it reverses or not: the reflection does not change whether the homogenization of degree d + d % 2 is squarefree (Polynomial.squarefree_homogenize_iff_squarefree_reflect).

theorem Ratpoints.Setup.not_squarefree_binaryFormPoly_of_reversal_eq_error {allow : Bool} {c : List ℤ} {d : ℕ} {e : Refusal} (h : reversal allow c d = Except.error e) : ¬Squarefree (binaryFormPoly c)

The refusal of the reversal check is sound: it refuses only when the square of the first variable divides Ratpoints.binaryFormPoly c (Ratpoints.not_squarefree_binaryFormPoly_of_getD_zero).

theorem Ratpoints.Sturm.run_chain_eq_none_iff_of_reversal_eq_ok {allow rev : Bool} {c c' : List ℤ} {d' : ℕ} (h2 : 2 ≤ c.length) (hc : c.length / 2 ≤ (degree c + 1) / 2) (h : Setup.reversal allow c (degree c) = Except.ok (c', d', rev)) : (chain c' d').run = none ↔ ¬Squarefree (binaryFormPoly c)

Once the test of the leading zeros has passed, the remainder chain of the polynomial that the reversal check hands on is none exactly when Ratpoints.binaryFormPoly c is not squarefree, whether the check reverses or not: the polynomial has the degree d' ≥ 1 that the check returns (Ratpoints.Setup.one_le_of_reversal_eq_ok), so that the chain detects its repeated factors (Ratpoints.Sturm.run_chain_eq_none_iff), and it is squarefree exactly when Ratpoints.binaryFormPoly c is (Ratpoints.Setup.squarefree_binaryFormPoly_iff_of_reversal_eq_ok).

The map of a reversed search

theorem Ratpoints.Sieve.swapPoint_swapPoint {q : ℤ × ℤ × ℤ} (hn : 0 < q.2.2 ∨ q.2.2 = 0 ∧ q.1 = 1) : swapPoint (swapPoint q) = q

The map of the reversal is an involution on the triples (x, y, z) with z > 0 or (x, z) = (1, 0), among them the normalized points.

theorem Ratpoints.Sieve.swapPoint_inj {q q' : ℤ × ℤ × ℤ} (hn : 0 < q.2.2 ∨ q.2.2 = 0 ∧ q.1 = 1) (hn' : 0 < q'.2.2 ∨ q'.2.2 = 0 ∧ q'.1 = 1) : swapPoint q = swapPoint q' ↔ q = q'

The map of the reversal is injective on the triples (x, y, z) with z > 0 or (x, z) = (1, 0) (Ratpoints.Sieve.swapPoint_swapPoint).

theorem Ratpoints.IsNormalizedPair.swapPoint {H : ℕ} {q : ℤ × ℤ × ℤ} (h : IsNormalizedPair H q.1 q.2.2) : IsNormalizedPair H (Sieve.swapPoint q).1 (Sieve.swapPoint q).2.2

The map of the reversal keeps the pairs (x, z) of normalized points of height at most H: it exchanges x and z, negating both for x < 0.

theorem Ratpoints.Sieve.isPoint_swapPoint {c c' : List ℤ} (hsw : ∀ (x z : ℤ), binaryForm c' x z = binaryForm c z x) {H : ℕ} {q : ℤ × ℤ × ℤ} (hq : IsPoint c' H q) : IsPoint c H (swapPoint q)

A point of a curve whose binary form is that of c with x and z exchanged gives a point of the curve of c: since the degree of Ratpoints.binaryForm is even, F(-x, -z) = F(x, z), and the map keeps the normalized pairs (Ratpoints.IsNormalizedPair.swapPoint).

theorem Ratpoints.Sieve.perm_map_swapPoint_bruteForce {c c' : List ℤ} (hsw : ∀ (x z : ℤ), binaryForm c' x z = binaryForm c z x) (H : ℕ) : (List.map swapPoint (bruteForce c' H)).Perm (bruteForce c H)

The brute-force reference of a curve whose binary form is that of c with x and z exchanged, mapped by Ratpoints.Sieve.swapPoint, is a permutation of the reference of c: the map sends the points of the one curve one to one onto those of the other, and neither list has duplicates.