Documentation

Ratpoints.Proof.Order

The order of the points: the specification and the model #

The pieces of the search that the specification of the order (Ratpoints.orderedPoints) spells out, in the terms of the model: the reversal check hands on the polynomial of Ratpoints.searchedPoly; the denominators of Ratpoints.searchDenominators lie in 1, …, H; and the points of the brute-force reference over a denominator, and over the candidate (1, 0), are those of Ratpoints.pointsWithDen. That the denominators of the search are those of Ratpoints.searchDenominators (Ratpoints.searchDens_one_eq_searchDenominators), since the divisor set-up succeeds exactly when ratpoints factors |c_d| completely and finds fewer than Ratpoints.maxDivisors divisors (Ratpoints.Setup.map_snd_run_setupUs1), is in Ratpoints.Proof.SearchDens, and Ratpoints.eq_orderedPoints_of_findPoints_eq_ok, which puts the pieces together, in Ratpoints.Proof.Output.

Main statements #

The polynomial searched #

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

The polynomial that the reversal check hands on, and whether it is reversed, are those of Ratpoints.searchedPoly.

The denominators #

source
theorem Ratpoints.pos_of_mem_binaryDivisors {n H e : ℕ} (he : e ∈ binaryDivisors n H) :
0 < e
source
theorem Ratpoints.le_and_le_of_mem_searchDenominators {maxDiv H b : ℕ} {c : List ℤ} (hb : b ∈ searchDenominators maxDiv c H) :
1 ≤ b ∧ b ≤ H

The points of a denominator #

source
theorem Ratpoints.pointsOfDen_eq_pointsWithDen (c : List ℤ) {H z : ℕ} (hz : 1 ≤ z) (hzH : z ≤ H) :
BruteForce.pointsOfDen c (degree c) (↑z) (BruteForce.numerators H) = pointsWithDen c H z

The points of the brute-force reference with the denominator 1 ≤ z ≤ H are those of Ratpoints.pointsWithDen, in the same order.

source
theorem Ratpoints.pointsOfDen_zero_eq_pointsWithDen (c : List ℤ) {H : ℕ} (hH : 1 ≤ H) :
BruteForce.pointsOfDen c (degree c) 0 [1] = pointsWithDen c H 0

The points at infinity of the brute-force reference, those of the candidate (1, 0), are those of Ratpoints.pointsWithDen with the denominator 0, for H ≥ 1: the numerators other than 1 give none.