The bounds of the search intervals

What the library makes of the search intervals of the caller before the Sturm step (Ratpoints.searchIntervals): it refuses them exactly when the specification says (Ratpoints.IntervalsWF), keeps them as they are, and for none takes the default interval [-h, h], which holds a / b for every numerator |a| ≤ H and every denominator b ≥ 1; and the bounds of the search intervals of a run (Ratpoints.Sieve.exactBounds), which give, for each denominator up to the largest, the ranges of the numerators ⌈b l⌉, …, ⌊b u⌋ of the intervals (Ratpoints.Sieve.numeratorRanges, Ratpoints.Sieve.RangesFor) to the sieve of one denominator.

The ends of the bounds are those of exact_end: ±m 2 ^ (-s) with the value of the double, or capped for a tiny end or one beyond 2 ^ 63, with the same numerators for every denominator 1 ≤ b < 2 ^ 63 (Ratpoints.Sieve.lowNumerator_eq_and_highNumerator_eq_run_exactEnd); exact_scale computes min (2 ^ 64 - 1) ⌊(b m + r) / 2 ^ s⌋ on two words (Ratpoints.Sieve.toNat_exactScale), so that interval_bits_exact gives the clamped numerators of the ends (Ratpoints.Sieve.toInt_intervalBitsExact); and the forms (b M + C) >> s of end_form are exact on the longs (Ratpoints.Sieve.lowNumerator_of_endForm, Ratpoints.Sieve.highNumerator_of_endForm), so that interval_bits on an interval taken inline gives them too (Ratpoints.Sieve.IntervalBounds.represents_of_fast).

Main definitions

• Ratpoints.Sieve.IsExactMantissa, Ratpoints.Sieve.IsEnd, Ratpoints.Sieve.ExactEnd.value: the mantissa and the ends that exact_end makes, and the value of an end.
• Ratpoints.Sieve.intervalBoundsOf: the bounds of one search interval, the body of the loop of Ratpoints.Sieve.exactBounds.

Main statements

• Ratpoints.run_searchIntervals_eq_none_iff: the refusal of the search intervals is the negation of Ratpoints.IntervalsWF.
• Ratpoints.run_searchIntervals_of_ne_nil, Ratpoints.exists_run_searchIntervals_nil: the search intervals of the caller, or the default interval, which holds every a / b of the search.
• Ratpoints.Sieve.toNat_exactScale, Ratpoints.Sieve.lowNumerator_eq_and_highNumerator_eq_run_exactEnd: exact_scale and the ends of exact_end.
• Ratpoints.Sieve.represents_intervalBoundsOf: the bounds of one search interval give the range of its numerators, on both paths of interval_bits.
• Ratpoints.Sieve.rangesFor_run_exactBounds: the bounds of the search intervals give the ranges of the numerators of every denominator up to the largest.

theorem Ratpoints.run_searchIntervals_eq {H : ℕ} {domain : List (Double × Double)} (h : domain ≠ []) : (searchIntervals H domain).run = if ((List.range domain.length).any fun (n : ℕ) => !domain[n]!.1.le domain[n]!.2 || decide (0 < n) && !domain[n - 1]!.2.lt domain[n]!.1) = true then none else some domain

theorem Ratpoints.intervalsWF_domainBits_iff_getElem (domain : List (Double × Double)) : IntervalsWF (domainBits domain) ↔ ∀ (n : ℕ) (hn : n < domain.length), domain[n].1.le domain[n].2 = true ∧ ∀ (h : 0 < n), domain[n - 1].2.lt domain[n].1 = true

theorem Ratpoints.run_searchIntervals_eq_none_iff (H : ℕ) (domain : List (Double × Double)) : (searchIntervals H domain).run = none ↔ ¬IntervalsWF (domainBits domain)

theorem Ratpoints.run_searchIntervals_of_ne_nil (H : ℕ) {domain : List (Double × Double)} (h : domain ≠ []) (hwf : IntervalsWF (domainBits domain)) : (searchIntervals H domain).run = some domain

theorem Ratpoints.intervalsWF_and_inIntervals_neg {h : Double} {H : ℕ} (hf : h.isFinite = true) (hv : ↑H ≤ h.toRat) : IntervalsWF (domainBits [(h.neg, h)]) ∧ ∀ (a : ℤ) (b : ℕ), 0 < b → a.natAbs ≤ H → InIntervals (domainValues [(h.neg, h)]) (↑a / ↑b)

The interval [-h, h] for a finite double h ≥ H is well formed and holds a / b for every numerator |a| ≤ H and denominator b ≥ 1.

theorem Ratpoints.exists_run_searchIntervals_nil {H : ℕ} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) : ∃ (dom : List (Double × Double)), (searchIntervals H []).run = some dom ∧ IntervalsWF (domainBits dom) ∧ ∀ (a : ℤ) (b : ℕ), 0 < b → a.natAbs ≤ H → InIntervals (domainValues dom) (↑a / ↑b)

theorem Ratpoints.intervalsWF_of_run_searchIntervals_eq_some {H : ℕ} {domain dom : List (Double × Double)} (h : (searchIntervals H domain).run = some dom) : IntervalsWF (domainBits domain)

The caller's search intervals are well formed when Ratpoints.searchIntervals does not refuse them.

theorem Ratpoints.intervalsWF_run_searchIntervals {H : ℕ} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) {domain : List (Double × Double)} (dom : List (Double × Double)) : dom ∈ (searchIntervals H domain).run → IntervalsWF (domainBits dom)

The search intervals that Ratpoints.searchIntervals returns for 1 ≤ H < 2 ^ 63 are well formed: the caller's, which it refuses otherwise, or the default interval.

theorem Ratpoints.Sieve.toNat_exactScale {b : Int64} {e : ExactEnd} (hs : e.s ≤ 127) (h : b.toUInt64.toNat * e.m.toNat + (e.rh.toNat * 2 ^ 64 + e.rl.toNat) < 2 ^ 128) : (exactScale b e).toNat = min (2 ^ 64 - 1) ((b.toUInt64.toNat * e.m.toNat + (e.rh.toNat * 2 ^ 64 + e.rl.toNat)) / 2 ^ e.s)

exact_scale: min (2 ^ 64 - 1) ⌊(b m + r) / 2 ^ s⌋ whenever b m + r fits 128 bits, with the end ±m 2 ^ (-s) and its rounding r = rh 2 ^ 64 + rl.

theorem Ratpoints.Sieve.toRat_ldexp_mantDig {f : Double} (hf : f.isFinite = true) (hlo : 1 / 2 ≤ f.toRat) (hhi : f.toRat < 1) : (f.ldexp ↑Double.mantDig).toRat = f.toRat * 2 ^ 53

ldexp(f, 53) of a double 1/2 ≤ f < 1, the fraction of frexp, is exact.

theorem Ratpoints.Sieve.toNat_toUInt64_ldexp_mantDig {f : Double} (hf : f.isFinite = true) (hlo : 1 / 2 ≤ f.toRat) (hhi : f.toRat < 1) : ↑(f.ldexp ↑Double.mantDig).toUInt64.toNat = f.toRat * 2 ^ 53

(unsigned long)ldexp(f, 53) of a double 1/2 ≤ f < 1 is f 2 ^ 53, an integer.

def Ratpoints.Sieve.IsExactMantissa (v : ℚ) (ms : UInt64 × ℕ) : Prop

The mantissa and the exponent (m, s) of exact_end for an end of absolute value v > 0: s ≤ 127, 0 < m < 2 ^ 63, and m 2 ^ (-s) = v, or s capped at 127 for a tiny v < 2 ^ (-75) with m < 2 ^ 53, where ⌊b v⌋ = 0 and ⌈b v⌉ = 1 for every b < 2 ^ 63, as for m 2 ^ (-127).

Equations

• Ratpoints.Sieve.IsExactMantissa v ms = (ms.2 ≤ 127 ∧ 0 < ms.1.toNat ∧ ms.1.toNat < 2 ^ 63 ∧ (↑ms.1.toNat / 2 ^ ms.2 = v ∨ ms.2 = 127 ∧ ms.1.toNat < 2 ^ 53 ∧ v < 2 ^ (-75)))

theorem Ratpoints.Sieve.isExactMantissa_of_eq {v : ℚ} {m : UInt64} {s : ℕ} (hs : s ≤ 127) (h0 : 0 < m.toNat) (h63 : m.toNat < 2 ^ 63) (hv : ↑m.toNat / 2 ^ s = v) : IsExactMantissa v (m, s)

theorem Ratpoints.Sieve.isExactMantissa_cap {v : ℚ} {m : UInt64} {s : ℤ} (hs : 127 < s) (h0 : 0 < m.toNat) (h53 : m.toNat < 2 ^ 53) (hv : ↑m.toNat / 2 ^ s = v) : IsExactMantissa v (m, Int.toNat 127)

theorem Ratpoints.Sieve.isExactMantissa_run_exactMantissa {x : Double} (ha : x.fabs.lt Double.twoPow63 = true) (h0 : x.toRat ≠ 0) : IsExactMantissa |x.toRat| (exactMantissa x.fabs).run

The mantissa and the exponent that exact_end makes for the absolute value of a finite end x ≠ 0 with |x| < 2 ^ 63.

theorem Ratpoints.Sieve.m_run_exactEnd (x : Double) (lower : Bool) : (exactEnd x lower).run.m = (if x.fabs.lt Double.twoPow63 = true then (exactMantissa x.fabs).run else (1 <<< 63, 0)).1

theorem Ratpoints.Sieve.s_run_exactEnd (x : Double) (lower : Bool) : (exactEnd x lower).run.s = (if x.fabs.lt Double.twoPow63 = true then (exactMantissa x.fabs).run else (1 <<< 63, 0)).2

theorem Ratpoints.Sieve.neg_run_exactEnd (x : Double) (lower : Bool) : (exactEnd x lower).run.neg = x.lt Double.zero

theorem Ratpoints.Sieve.rounding_run_exactEnd {x : Double} {lower : Bool} (hs : (exactEnd x lower).run.s ≤ 127) : (exactEnd x lower).run.rh.toNat * 2 ^ 64 + (exactEnd x lower).run.rl.toNat = if (lower != x.lt Double.zero) = true then 2 ^ (exactEnd x lower).run.s - 1 else 0

theorem Ratpoints.Sieve.run_exactMantissa_fabs_of_toRat_eq_zero {x : Double} (h : x.toRat = 0) : (exactMantissa x.fabs).run = (0, 0)

def Ratpoints.Sieve.ExactEnd.value (e : ExactEnd) : ℚ

The value ±m 2 ^ (-s) of an end of a search interval as exact_end makes it.

Equations

• e.value = (if e.neg = true then -1 else 1) * (↑e.m.toNat / 2 ^ e.s)

theorem Ratpoints.Sieve.lowNumerator_eq_and_highNumerator_eq_of_ceil_eq_of_floor_eq {b H : ℕ} {q q' : ℚ} (hc : ⌈↑b * q⌉ = ⌈↑b * q'⌉) (hf : ⌊↑b * q⌋ = ⌊↑b * q'⌋) : lowNumerator b H (WithBotTop.coe q) = lowNumerator b H (WithBotTop.coe q') ∧ highNumerator b H (WithBotTop.coe q) = highNumerator b H (WithBotTop.coe q')

theorem Ratpoints.Sieve.lowNumerator_eq_and_highNumerator_eq_of_two_pow_le {b H : ℕ} (hb : 1 ≤ b) (hH : H < 2 ^ 63) {x : WithBotTop ℚ} (hx : WithBotTop.coe (2 ^ 63) ≤ x) : lowNumerator b H x = ↑H + 1 ∧ highNumerator b H x = ↑H

theorem Ratpoints.Sieve.lowNumerator_eq_and_highNumerator_eq_of_le_neg_two_pow {b H : ℕ} (hb : 1 ≤ b) (hH : H < 2 ^ 63) {x : WithBotTop ℚ} (hx : x ≤ WithBotTop.coe (-2 ^ 63)) : lowNumerator b H x = -↑H ∧ highNumerator b H x = -↑H - 1

theorem Ratpoints.Sieve.value_run_exactEnd_of_lt_eq_false {x : Double} (lower : Bool) (ha : x.fabs.lt Double.twoPow63 = false) : (exactEnd x lower).run.value = if x.lt Double.zero = true then -2 ^ 63 else 2 ^ 63

theorem Ratpoints.Sieve.lowNumerator_eq_and_highNumerator_eq_run_exactEnd_of_lt_eq_false {x : Double} (hx : x.isNaN = false) (lower : Bool) (ha : x.fabs.lt Double.twoPow63 = false) {b H : ℕ} (hb : 1 ≤ b) (hH : H < 2 ^ 63) : lowNumerator b H (doubleValue x.bits) = lowNumerator b H (WithBotTop.coe (exactEnd x lower).run.value) ∧ highNumerator b H (doubleValue x.bits) = highNumerator b H (WithBotTop.coe (exactEnd x lower).run.value)

The numerators of the end x of a search interval with |x| ≥ 2 ^ 63 (an infinity included) are those of exact_end's ±2 ^ 63: beyond the height bound on the side of its sign.

theorem Ratpoints.Sieve.lowNumerator_eq_and_highNumerator_eq_of_abs_lt {b H : ℕ} (hb : 1 ≤ b) (hb63 : b < 2 ^ 63) {q : ℚ} {neg : Bool} {m : ℕ} (hq : q ≠ 0) (hq75 : |q| < 2 ^ (-75)) (hneg : neg = true ↔ q < 0) (hm0 : 0 < m) (hm : m < 2 ^ 53) : lowNumerator b H (WithBotTop.coe q) = lowNumerator b H (WithBotTop.coe ((if neg = true then -1 else 1) * (↑m / 2 ^ 127))) ∧ highNumerator b H (WithBotTop.coe q) = highNumerator b H (WithBotTop.coe ((if neg = true then -1 else 1) * (↑m / 2 ^ 127)))

A tiny end 0 < |q| < 2 ^ (-75) has the numerators of exact_end's ±m 2 ^ (-127) with 0 < m < 2 ^ 53 and the same sign, for every denominator 1 ≤ b < 2 ^ 63: b |q| and b m 2 ^ (-127) lie strictly between 0 and 1.

theorem Ratpoints.Sieve.lowNumerator_eq_and_highNumerator_eq_run_exactEnd_of_lt_eq_true {x : Double} (lower : Bool) (ha : x.fabs.lt Double.twoPow63 = true) {b H : ℕ} (hb : 1 ≤ b) (hb63 : b < 2 ^ 63) : lowNumerator b H (doubleValue x.bits) = lowNumerator b H (WithBotTop.coe (exactEnd x lower).run.value) ∧ highNumerator b H (doubleValue x.bits) = highNumerator b H (WithBotTop.coe (exactEnd x lower).run.value)

The numerators of the end x of a search interval with |x| < 2 ^ 63 are those of the value of exact_end, exact unless capped for a tiny x, for every denominator 1 ≤ b < 2 ^ 63.

theorem Ratpoints.Sieve.lowNumerator_eq_and_highNumerator_eq_run_exactEnd {x : Double} (hx : x.isNaN = false) (lower : Bool) {b H : ℕ} (hb : 1 ≤ b) (hb63 : b < 2 ^ 63) (hH : H < 2 ^ 63) : lowNumerator b H (doubleValue x.bits) = lowNumerator b H (WithBotTop.coe (exactEnd x lower).run.value) ∧ highNumerator b H (doubleValue x.bits) = highNumerator b H (WithBotTop.coe (exactEnd x lower).run.value)

The numerators of the end x of a search interval, not a NaN, are those of the value of exact_end, for every denominator 1 ≤ b < 2 ^ 63 and height bound H < 2 ^ 63.

def Ratpoints.Sieve.IsEnd (e : ExactEnd) (lower : Bool) : Prop

The end e of a search interval, at its lower end if lower, is one that exact_end makes: s ≤ 127, m ≤ 2 ^ 63, and the rounding 2 ^ s - 1 when the end wants b |x| rounded up.

Equations

• Ratpoints.Sieve.IsEnd e lower = (e.s ≤ 127 ∧ e.m.toNat ≤ 2 ^ 63 ∧ e.rh.toNat * 2 ^ 64 + e.rl.toNat = if (lower != e.neg) = true then 2 ^ e.s - 1 else 0)

theorem Ratpoints.Sieve.isEnd_run_exactEnd (x : Double) (lower : Bool) : IsEnd (exactEnd x lower).run lower

theorem Ratpoints.Sieve.ceil_mul_div_two_pow (B m s : ℕ) : ⌈↑B * (↑m / 2 ^ s)⌉ = ↑((B * m + (2 ^ s - 1)) / 2 ^ s)

theorem Ratpoints.Sieve.floor_mul_div_two_pow (B m s : ℕ) : ⌊↑B * (↑m / 2 ^ s)⌋ = ↑(B * m / 2 ^ s)

theorem Ratpoints.Sieve.toNat_exactScale_of_isEnd {e : ExactEnd} {lower : Bool} (he : IsEnd e lower) {B : ℕ} (hB : B < 2 ^ 63) : (exactScale B.toInt64 e).toNat = min (2 ^ 64 - 1) (if (lower != e.neg) = true then (B * e.m.toNat + (2 ^ e.s - 1)) / 2 ^ e.s else B * e.m.toNat / 2 ^ e.s)

theorem Ratpoints.Sieve.lowNumerator_value_of_not_neg {e : ExactEnd} (hn : e.neg = false) (B H : ℕ) : lowNumerator B H (WithBotTop.coe e.value) = max (-↑H) (min (↑((B * e.m.toNat + (2 ^ e.s - 1)) / 2 ^ e.s)) (↑H + 1))

theorem Ratpoints.Sieve.lowNumerator_value_of_neg {e : ExactEnd} (hn : e.neg = true) (B H : ℕ) : lowNumerator B H (WithBotTop.coe e.value) = max (-↑H) (min (-↑(B * e.m.toNat / 2 ^ e.s)) (↑H + 1))

theorem Ratpoints.Sieve.highNumerator_value_of_not_neg {e : ExactEnd} (hn : e.neg = false) (B H : ℕ) : highNumerator B H (WithBotTop.coe e.value) = max (-↑H - 1) (min ↑(B * e.m.toNat / 2 ^ e.s) ↑H)

theorem Ratpoints.Sieve.highNumerator_value_of_neg {e : ExactEnd} (hn : e.neg = true) (B H : ℕ) : highNumerator B H (WithBotTop.coe e.value) = max (-↑H - 1) (min (-↑((B * e.m.toNat + (2 ^ e.s - 1)) / 2 ^ e.s)) ↑H)

theorem Ratpoints.Sieve.lowNumerator_exact_of_not_neg {e : ExactEnd} (he : IsEnd e true) (hn : e.neg = false) {B H : ℕ} (hB : B < 2 ^ 63) (hH : H < 2 ^ 63) : (H.toInt64.toUInt64 < exactScale B.toInt64 e ↔ ↑H < lowNumerator B H (WithBotTop.coe e.value)) ∧ (exactScale B.toInt64 e ≤ H.toInt64.toUInt64 → (exactScale B.toInt64 e).toInt64.toInt = lowNumerator B H (WithBotTop.coe e.value))

interval_bits_exact at a lower end x ≥ 0: the code 2 exactly when ⌈b x⌉ > h, and otherwise ⌈b x⌉.

theorem Ratpoints.Sieve.lowNumerator_exact_of_neg {e : ExactEnd} (he : IsEnd e true) (hn : e.neg = true) {B H : ℕ} (hB : B < 2 ^ 63) (hH : H < 2 ^ 63) : (if H.toInt64.toUInt64 ≤ exactScale B.toInt64 e then -H.toInt64 else -(exactScale B.toInt64 e).toInt64).toInt = lowNumerator B H (WithBotTop.coe e.value)

interval_bits_exact at a lower end x < 0: ⌈b x⌉ = -⌊b |x|⌋, clipped to -h.

theorem Ratpoints.Sieve.highNumerator_exact_of_not_neg {e : ExactEnd} (he : IsEnd e false) (hn : e.neg = false) {B H : ℕ} (hB : B < 2 ^ 63) (hH : H < 2 ^ 63) : (if H.toInt64.toUInt64 ≤ exactScale B.toInt64 e then H.toInt64 else (exactScale B.toInt64 e).toInt64).toInt = highNumerator B H (WithBotTop.coe e.value)

interval_bits_exact at an upper end x ≥ 0: ⌊b x⌋, clipped to h.

theorem Ratpoints.Sieve.highNumerator_exact_of_neg {e : ExactEnd} (he : IsEnd e false) (hn : e.neg = true) {B H : ℕ} (hB : B < 2 ^ 63) (hH : H < 2 ^ 63) : (H.toInt64.toUInt64 < exactScale B.toInt64 e ↔ highNumerator B H (WithBotTop.coe e.value) < -↑H) ∧ (exactScale B.toInt64 e ≤ H.toInt64.toUInt64 → (-(exactScale B.toInt64 e).toInt64).toInt = highNumerator B H (WithBotTop.coe e.value))

interval_bits_exact at an upper end x < 0: the code 1 exactly when ⌊b x⌋ < -h, and otherwise ⌊b x⌋ = -⌈b |x|⌉.

theorem Ratpoints.Sieve.toInt_numeratorsToBits_of_range {l h : Int64} {cl : NumClass} (hcl : cl.WF) {H : ℕ} (hH : H < 2 ^ 63) {L U : ℤ} (hl : l.toInt = L) (hh : h.toInt = U) (hL : -↑H ≤ L) (hU : -↑H - 1 ≤ U) (hUH : U ≤ ↑H) : (numeratorsToBits l h cl (decide (9223372036854775807 - 64 < H.toInt64))).1.toInt = -((↑cl.a0 - max L (-↑H)) / 2 ^ cl.k) ∧ (numeratorsToBits l h cl (decide (9223372036854775807 - 64 < H.toInt64))).2.toInt = (min U ↑H - ↑cl.a0) / 2 ^ cl.k

The bits of the range L, …, U of numerators within -H - 1, …, H + 1 in the packing of a class, in the form of numerators_to_bits that the sieve takes for the height bound H, the plain one for H ≤ 2 ^ 63 - 65.

theorem Ratpoints.Sieve.toInt_intervalBitsExact {bd : IntervalBounds} (hl : IsEnd bd.low true) (hu : IsEnd bd.up false) {B H : ℕ} (hBH : B ≤ H) (hH : H < 2 ^ 63) {cl : NumClass} (hcl : cl.WF) : ((intervalBitsExact B.toInt64 bd H.toInt64 cl).1 = 2 → ↑H < lowNumerator B H (WithBotTop.coe bd.low.value)) ∧ ((intervalBitsExact B.toInt64 bd H.toInt64 cl).1 = 1 → highNumerator B H (WithBotTop.coe bd.up.value) < -↑H) ∧ ((intervalBitsExact B.toInt64 bd H.toInt64 cl).1 ≠ 1 → (intervalBitsExact B.toInt64 bd H.toInt64 cl).1 ≠ 2 → (intervalBitsExact B.toInt64 bd H.toInt64 cl).2.1.toInt = -((↑cl.a0 - max (lowNumerator B H (WithBotTop.coe bd.low.value)) (-↑H)) / 2 ^ cl.k) ∧ (intervalBitsExact B.toInt64 bd H.toInt64 cl).2.2.toInt = (min (highNumerator B H (WithBotTop.coe bd.up.value)) ↑H - ↑cl.a0) / 2 ^ cl.k)

interval_bits_exact gives the range of the numerators of the ends: the code 2 only above H, the code 1 only below -H, and otherwise the bits of the range within -H, …, H.

theorem Ratpoints.Sieve.toInt_mul_add_shiftRight {B : ℕ} (hB : B < 2 ^ 63) {M C : Int64} {s : ℕ} (hs : s < 64) (h1 : -2 ^ 63 ≤ ↑B * M.toInt) (h2 : ↑B * M.toInt < 2 ^ 63) (h3 : -2 ^ 63 ≤ ↑B * M.toInt + C.toInt) (h4 : ↑B * M.toInt + C.toInt < 2 ^ 63) : ((B.toInt64 * M + C) >>> s.toInt64).toInt = (↑B * M.toInt + C.toInt) / 2 ^ s

The form (b M + C) >> sh of an end on the longs, without overflow: the floor of (b M + C) / 2 ^ sh.

theorem Ratpoints.Sieve.toInt_ite_neg_toInt64 {e : ExactEnd} (hm : e.m.toNat < 2 ^ 63) : (if e.neg = true then -e.m.toInt64 else e.m.toInt64).toInt = (if e.neg = true then -1 else 1) * ↑e.m.toNat

theorem Ratpoints.Sieve.natCast_mul_value {e : ExactEnd} (B : ℕ) : ↑B * e.value = ↑(↑B * ((if e.neg = true then -1 else 1) * ↑e.m.toNat)) / 2 ^ e.s

theorem Ratpoints.Sieve.toInt_form {e : ExactEnd} {B bHigh : ℕ} {C : Int64} (hs : e.s < 64) (hB1 : 1 ≤ B) (hB : B ≤ bHigh) (hB63 : B < 2 ^ 63) (hC : 0 ≤ C.toInt) (hg : ↑e.m.toNat * ↑bHigh + C.toInt ≤ 2 ^ 63 - 1) : (((B.toInt64 * if e.neg = true then -e.m.toInt64 else e.m.toInt64) + C) >>> e.s.toInt64).toInt = (↑B * ((if e.neg = true then -1 else 1) * ↑e.m.toNat) + C.toInt) / 2 ^ e.s

The form (b M + C) >> s of an end with C ≥ 0, without overflow for b up to the largest denominator by the guard of end_form, on the longs: the floor of (b (±m) + C) / 2 ^ s.

theorem Ratpoints.Sieve.mul_add_le_of_le_toUInt64_div {m : UInt64} {c : Int64} {bHigh : ℕ} (hc0 : 0 ≤ c.toInt) (hb : 0 < bHigh) (hb63 : bHigh < 2 ^ 63) (h : m ≤ ((9223372036854775807 - c) / bHigh.toInt64).toUInt64) : ↑m.toNat * ↑bHigh + c.toInt ≤ 2 ^ 63 - 1

The guard m ≤ (LONG_MAX - c) / b_high of end_form on the longs: m b_high + c is a long.

theorem Ratpoints.Sieve.lowNumerator_of_form {e : ExactEnd} {H bHigh B : ℕ} (hH : H < 2 ^ 63) (hbH : bHigh ≤ H) (hB1 : 1 ≤ B) (hB : B ≤ bHigh) (hs : e.s < 64) (hg : e.m ≤ ((9223372036854775807 - (1 <<< e.s.toUInt64 - 1).toInt64) / bHigh.toInt64).toUInt64) : max (-↑H) (min (((B.toInt64 * if e.neg = true then -e.m.toInt64 else e.m.toInt64) + (1 <<< e.s.toUInt64 - 1).toInt64) >>> e.s.toInt64).toInt (↑H + 1)) = lowNumerator B H (WithBotTop.coe e.value)

The form (b (±m) + 2 ^ s - 1) >> s of a lower end with s < 64 and the guard of end_form, clamped to -H, …, H + 1, is the least numerator of the end.

theorem Ratpoints.Sieve.toInt_const_shiftRight_zero {B : ℕ} (hB : B < 2 ^ 63) {C : Int64} : ((B.toInt64 * 0 + C) >>> Nat.toInt64 0).toInt = C.toInt

theorem Ratpoints.Sieve.le_mul_div_of_le_exactScale_one {e : ExactEnd} {lower : Bool} (he : IsEnd e lower) (hr : (lower != e.neg) = false) {H B : ℕ} (hH : H < 2 ^ 63) (hB1 : 1 ≤ B) (ht : H.toInt64.toUInt64 ≤ exactScale 1 e) : H ≤ B * e.m.toNat / 2 ^ e.s

An end whose magnitude, rounded down, exact_scale at b = 1 finds at least H, has ⌊b |x|⌋ ≥ H for every denominator b ≥ 1.

theorem Ratpoints.Sieve.lowNumerator_of_le_exactScale_one {e : ExactEnd} (he : IsEnd e true) {H B : ℕ} (hH : H < 2 ^ 63) (hB1 : 1 ≤ B) (hB63 : B < 2 ^ 63) (hn : e.neg = true) (ht : H.toInt64.toUInt64 ≤ exactScale 1 e) : max (-↑H) (min ((B.toInt64 * 0 + -H.toInt64) >>> Nat.toInt64 0).toInt (↑H + 1)) = lowNumerator B H (WithBotTop.coe e.value)

The form (0, -H, 0) of a lower end x ≤ -H, clamped, is the least numerator -H.

theorem Ratpoints.Sieve.lowNumerator_of_endForm {e : ExactEnd} (he : IsEnd e true) {H bHigh B : ℕ} (hH : H < 2 ^ 63) (hbH : bHigh ≤ H) (hB1 : 1 ≤ B) (hB : B ≤ bHigh) {f : Int64 × Int64 × ℕ} (hf : endForm e true H.toInt64 bHigh.toInt64 = some f) : max (-↑H) (min ((B.toInt64 * f.1 + f.2.1) >>> f.2.2.toInt64).toInt (↑H + 1)) = lowNumerator B H (WithBotTop.coe e.value)

The form of a lower end, clamped to -H, …, H + 1, is the least numerator of the end: the constant -H for an end x ≤ -H, which exact_scale at b = 1 finds, and ⌈b x⌉ for an end with a short mantissa.

theorem Ratpoints.Sieve.highNumerator_of_form {e : ExactEnd} {H bHigh B : ℕ} (hH : H < 2 ^ 63) (hbH : bHigh ≤ H) (hB1 : 1 ≤ B) (hB : B ≤ bHigh) (hs : e.s < 64) (hg : e.m ≤ ((9223372036854775807 - 0) / bHigh.toInt64).toUInt64) : max (-↑H - 1) (min (((B.toInt64 * if e.neg = true then -e.m.toInt64 else e.m.toInt64) + 0) >>> e.s.toInt64).toInt ↑H) = highNumerator B H (WithBotTop.coe e.value)

The form (b (±m)) >> s of an upper end with s < 64 and the guard of end_form, clamped to -H - 1, …, H, is the largest numerator of the end.

theorem Ratpoints.Sieve.highNumerator_of_le_exactScale_one {e : ExactEnd} (he : IsEnd e false) {H B : ℕ} (hH : H < 2 ^ 63) (hB1 : 1 ≤ B) (hB63 : B < 2 ^ 63) (hn : e.neg = false) (ht : H.toInt64.toUInt64 ≤ exactScale 1 e) : max (-↑H - 1) (min ((B.toInt64 * 0 + H.toInt64) >>> Nat.toInt64 0).toInt ↑H) = highNumerator B H (WithBotTop.coe e.value)

The form (0, H, 0) of an upper end x ≥ H, clamped, is the largest numerator H.

theorem Ratpoints.Sieve.highNumerator_of_endForm {e : ExactEnd} (he : IsEnd e false) {H bHigh B : ℕ} (hH : H < 2 ^ 63) (hbH : bHigh ≤ H) (hB1 : 1 ≤ B) (hB : B ≤ bHigh) {f : Int64 × Int64 × ℕ} (hf : endForm e false H.toInt64 bHigh.toInt64 = some f) : max (-↑H - 1) (min ((B.toInt64 * f.1 + f.2.1) >>> f.2.2.toInt64).toInt ↑H) = highNumerator B H (WithBotTop.coe e.value)

The form of an upper end, clamped to -H - 1, …, H, is the largest numerator of the end: the constant H for an end x ≥ H, which exact_scale at b = 1 finds, and ⌊b x⌋ for an end with a short mantissa.

theorem Ratpoints.Sieve.toInt_numeratorsToBits_clip {lo hi : Int64} {H : ℕ} (hH : H ≤ 2 ^ 63 - 65) {L U : ℤ} (hL : max (-↑H) (min lo.toInt (↑H + 1)) = L) (hU : max (-↑H - 1) (min hi.toInt ↑H) = U) (h1 : lo.toInt ≤ ↑H) (h2 : -↑H ≤ hi.toInt) {cl : NumClass} (hcl : cl.WF) : (numeratorsToBits (if lo < -H.toInt64 then -H.toInt64 else lo) (if H.toInt64 < hi then H.toInt64 else hi) cl false).1.toInt = -((↑cl.a0 - max L (-↑H)) / 2 ^ cl.k) ∧ (numeratorsToBits (if lo < -H.toInt64 then -H.toInt64 else lo) (if H.toInt64 < hi then H.toInt64 else hi) cl false).2.toInt = (min U ↑H - ↑cl.a0) / 2 ^ cl.k

The bits of interval_bits on an interval taken inline, from the values lo ≤ H and hi ≥ -H of the forms of its ends clipped to -H, …, H: those of the least numerator L and the largest numerator U.

theorem Ratpoints.Sieve.IntervalBounds.Represents.of_forall {bd : IntervalBounds} {b H : ℕ} {lo hi : ℤ} (h : ∀ (cl : NumClass), cl.WF → ((intervalBits b.toInt64 bd H.toInt64 cl).1 = 2 → ↑H < lo) ∧ ((intervalBits b.toInt64 bd H.toInt64 cl).1 = 1 → hi < -↑H) ∧ ((intervalBits b.toInt64 bd H.toInt64 cl).1 ≠ 1 → (intervalBits b.toInt64 bd H.toInt64 cl).1 ≠ 2 → (intervalBits b.toInt64 bd H.toInt64 cl).2.1.toInt = -((↑cl.a0 - max lo (-↑H)) / 2 ^ cl.k) ∧ (intervalBits b.toInt64 bd H.toInt64 cl).2.2.toInt = (min hi ↑H - ↑cl.a0) / 2 ^ cl.k)) : bd.Represents b H lo hi

theorem Ratpoints.Sieve.IntervalBounds.represents_of_fast {bd : IntervalBounds} (hfast : bd.fast = true) {B H : ℕ} (hH : H ≤ 2 ^ 63 - 65) {L U : ℤ} (hL : max (-↑H) (min ((B.toInt64 * bd.lM + bd.lC) >>> bd.lsh.toInt64).toInt (↑H + 1)) = L) (hU : max (-↑H - 1) (min ((B.toInt64 * bd.uM + bd.uC) >>> bd.ush.toInt64).toInt ↑H) = U) : bd.Represents B H L U

The bounds bd of an interval taken inline give the range L, …, U of the numerators, from the forms of its ends clamped to the least numerator L and the largest numerator U: in interval_bits, the code 2 only above H, the code 1 only below -H, and otherwise the bits of L, …, U.

def Ratpoints.Sieve.intervalBoundsOf (height bHigh : Int64) (i : Double × Double) : IntervalBounds

The bounds of the search interval i that Ratpoints.Sieve.exactBounds makes for the height bound height and the largest denominator bHigh: the body of its loop.

Equations

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

theorem Ratpoints.Sieve.toList_run_exactBounds (dom : List (Double × Double)) (height bHigh : Int64) : (exactBounds dom height bHigh).run.toList = List.map (intervalBoundsOf height bHigh) dom

theorem Ratpoints.Sieve.intervalBits_eq_intervalBitsExact (low up : ExactEnd) {B H : ℕ} (hB : B < 2 ^ 63) (hH : H < 2 ^ 63) (cl : NumClass) : intervalBits B.toInt64 { lM := 0, lC := 0, uM := 0, uC := -9223372036854775808, lsh := 0, ush := 0, fast := false, low := low, up := up } H.toInt64 cl = intervalBitsExact B.toInt64 { lM := 0, lC := 0, uM := 0, uC := -9223372036854775808, lsh := 0, ush := 0, fast := false, low := low, up := up } H.toInt64 cl

An interval that is not taken inline has the forms of an empty one, and interval_bits goes to interval_bits_exact for it.

theorem Ratpoints.Sieve.represents_intervalBoundsOf (l u : Double) {H bHigh B : ℕ} (hH : H < 2 ^ 63) (hbH : bHigh ≤ H) (hB1 : 1 ≤ B) (hB : B ≤ bHigh) : (intervalBoundsOf H.toInt64 bHigh.toInt64 (l, u)).Represents B H (lowNumerator B H (WithBotTop.coe (exactEnd l true).run.value)) (highNumerator B H (WithBotTop.coe (exactEnd u false).run.value))

The bounds of a search interval [l, u] give, for the denominator 1 ≤ B ≤ bHigh ≤ H < 2 ^ 63, the range of the numerators ⌈B l⌉, …, ⌊B u⌋ of the values of exact_end, clamped, in both paths of interval_bits.

theorem Ratpoints.Sieve.areSearchIntervals_domainValues {dom : List (Double × Double)} (hdom : IntervalsWF (domainBits dom)) : AreSearchIntervals (domainValues dom)

theorem Ratpoints.Sieve.rangesFor_run_exactBounds {dom : List (Double × Double)} (hdom : IntervalsWF (domainBits dom)) {H bHigh : ℕ} (hH : H < 2 ^ 63) (hbHigh : bHigh ≤ H) {b : ℕ} (hb : 0 < b) (hbb : b ≤ bHigh) : RangesFor (exactBounds dom H.toInt64 bHigh.toInt64).run b H (numeratorRanges b H (domainValues dom))

The bounds of well-formed search intervals for H < 2 ^ 63 and the largest denominator bHigh ≤ H give, for every denominator 1 ≤ b ≤ bHigh, the ranges of the numerators of the intervals (Ratpoints.Sieve.numeratorRanges).