The search region in the proofs

The search intervals of the model, pairs of doubles (Ratpoints.Double), over the values of their ends (Ratpoints.domainValues) and their bits (Ratpoints.domainBits); the ranges of the numerators of a denominator b that a list of intervals over values (Ratpoints.InIntervals) gives within -H, …, H (Ratpoints.Sieve.numeratorRanges), with the ends ⌈b l⌉ and ⌊b u⌋ clamped, which the bounds of the search intervals of a run give to the sieve of one denominator (Ratpoints.Sieve.RangesFor); and the normalized options of a search (Ratpoints.Options.normalize) in the terms of the specification of the search region (Ratpoints.IsFullBox, Ratpoints.denominatorBound).

Main definitions

• Ratpoints.domainValues, Ratpoints.domainBits: the values and the bits of the ends of the search intervals of the model.
• Ratpoints.Sieve.lowNumerator, Ratpoints.Sieve.highNumerator, Ratpoints.Sieve.numeratorRanges: the ranges of the numerators of a denominator in a list of intervals.

Main statements

• Ratpoints.Sieve.inRanges_numeratorRanges: a numerator |a| ≤ H lies in one of the ranges exactly when a / b lies in one of the intervals.
• Ratpoints.Sieve.pairwise_numeratorRanges, Ratpoints.Sieve.le_add_one_of_mem_numeratorRanges: the ranges of search intervals are increasing and strictly apart, each empty at most by one.
• Ratpoints.Options.reverse_normalize, Ratpoints.Options.toNat_bHigh_normalize, Ratpoints.Options.bLow_normalize_le_iff: the normalized options in the terms of the specification.

@[reducible, inline]

abbrev Ratpoints.domainValues (dom : List (Double × Double)) : List (WithBotTop ℚ × WithBotTop ℚ)

The values of the ends of the search intervals dom of the model (Ratpoints.doubleValue).

Equations

• Ratpoints.domainValues dom = List.map (fun (i : Ratpoints.Double × Ratpoints.Double) => (Ratpoints.doubleValue i.1.bits, Ratpoints.doubleValue i.2.bits)) dom

@[reducible, inline]

abbrev Ratpoints.domainBits (dom : List (Double × Double)) : List (UInt64 × UInt64)

The bits of the ends of the search intervals dom of the model.

Equations

• Ratpoints.domainBits dom = List.map (fun (i : Ratpoints.Double × Ratpoints.Double) => (i.1.bits, i.2.bits)) dom

theorem Ratpoints.inRegion_of_isFullBox {D : List (WithBotTop ℚ × WithBotTop ℚ)} {bLow bHigh : ℤ} {H : ℕ} (hb : IsFullBox D bLow bHigh H) {p : ℤ × ℤ × ℤ} (hz : 0 ≤ p.2.2) (hzH : p.2.2 ≤ ↑H) : InRegion D bLow bHigh p

A pair (x, z) of height at most H lies in the search region of the whole box.

theorem Ratpoints.IsNormalizedPair.inRegion_of_isFullBox {H : ℕ} {p : ℤ × ℤ × ℤ} (hn : IsNormalizedPair H p.1 p.2.2) {D : List (WithBotTop ℚ × WithBotTop ℚ)} {bLow bHigh : ℤ} (hb : IsFullBox D bLow bHigh H) : InRegion D bLow bHigh p

A normalized pair (x, z) of height at most H lies, with any y, in the search region of the whole box.

theorem Ratpoints.IsFullBox.map {α : Type u_1} {β : Type u_2} {dom : List α} {bLow bHigh : ℤ} {H : ℕ} (h : IsFullBox dom bLow bHigh H) (f : α → β) : IsFullBox (List.map f dom) bLow bHigh H

def Ratpoints.Sieve.lowNumerator (b H : ℕ) (x : WithBotTop ℚ) : ℤ

The least numerator of the denominator b in an interval with the lower end x, within -H, …, H + 1: ⌈b x⌉ clamped, -H for x = ⊥ and H + 1 for x = ⊤.

Equations

• Ratpoints.Sieve.lowNumerator b H x = WithBotTop.rec (-↑H) (fun (q : ℚ) => max (-↑H) (min ⌈↑b * q⌉ (↑H + 1))) (↑H + 1) x

def Ratpoints.Sieve.highNumerator (b H : ℕ) (x : WithBotTop ℚ) : ℤ

The largest numerator of the denominator b in an interval with the upper end x, within -H - 1, …, H: ⌊b x⌋ clamped, -H - 1 for x = ⊥ and H for x = ⊤.

Equations

• Ratpoints.Sieve.highNumerator b H x = WithBotTop.rec (-↑H - 1) (fun (q : ℚ) => max (-↑H - 1) (min ⌊↑b * q⌋ ↑H)) (↑H) x

def Ratpoints.Sieve.numeratorRanges (b H : ℕ) (D : List (WithBotTop ℚ × WithBotTop ℚ)) : List (ℤ × ℤ)

The ranges of the numerators of the denominator b in the intervals D, within -H, …, H but for the clamps: an integer |a| ≤ H lies in the range of an interval exactly when a / b lies in the interval (Ratpoints.Sieve.inRanges_numeratorRanges).

Equations

• Ratpoints.Sieve.numeratorRanges b H D = List.map (fun (i : WithBotTop ℚ × WithBotTop ℚ) => (Ratpoints.Sieve.lowNumerator b H i.1, Ratpoints.Sieve.highNumerator b H i.2)) D

theorem Ratpoints.Sieve.lowNumerator_le_iff {b H : ℕ} (hb : 0 < b) {a : ℤ} (ha : a.natAbs ≤ H) (x : WithBotTop ℚ) : lowNumerator b H x ≤ a ↔ x ≤ WithBotTop.coe (↑a / ↑b)

theorem Ratpoints.Sieve.le_highNumerator_iff {b H : ℕ} (hb : 0 < b) {a : ℤ} (ha : a.natAbs ≤ H) (x : WithBotTop ℚ) : a ≤ highNumerator b H x ↔ WithBotTop.coe (↑a / ↑b) ≤ x

theorem Ratpoints.Sieve.inRanges_numeratorRanges {b H : ℕ} (hb : 0 < b) {a : ℤ} (ha : a.natAbs ≤ H) (D : List (WithBotTop ℚ × WithBotTop ℚ)) : inRanges (numeratorRanges b H D) a = decide (InIntervals D (↑a / ↑b))

theorem Ratpoints.Sieve.neg_le_lowNumerator (b H : ℕ) (x : WithBotTop ℚ) : -↑H ≤ lowNumerator b H x

theorem Ratpoints.Sieve.lowNumerator_le (b H : ℕ) (x : WithBotTop ℚ) : lowNumerator b H x ≤ ↑H + 1

theorem Ratpoints.Sieve.neg_sub_one_le_highNumerator (b H : ℕ) (x : WithBotTop ℚ) : -↑H - 1 ≤ highNumerator b H x

theorem Ratpoints.Sieve.highNumerator_le (b H : ℕ) (x : WithBotTop ℚ) : highNumerator b H x ≤ ↑H

theorem Ratpoints.Sieve.lowNumerator_le_highNumerator_add_one {l u : WithBotTop ℚ} (h : l ≤ u) (b H : ℕ) : lowNumerator b H l ≤ highNumerator b H u + 1

The range of an interval [l, u] with l ≤ u is empty at most by one: ⌈b l⌉ ≤ ⌊b u⌋ + 1, and the clamps keep it.

theorem Ratpoints.Sieve.highNumerator_lt_lowNumerator {u l : WithBotTop ℚ} (h : u < l) {b : ℕ} (hb : 0 < b) (H : ℕ) : highNumerator b H u < lowNumerator b H l

The range of an interval ending below the start of another ends below the start of its range: ⌊b u⌋ < ⌈b l⌉ for u < l, and the clamps keep it.

theorem Ratpoints.Sieve.le_add_one_of_mem_numeratorRanges {D : List (WithBotTop ℚ × WithBotTop ℚ)} (hD : ∀ i ∈ D, i.1 ≤ i.2) (b H : ℕ) (r : ℤ × ℤ) : r ∈ numeratorRanges b H D → r.1 ≤ r.2 + 1

theorem Ratpoints.Sieve.pairwise_numeratorRanges {D : List (WithBotTop ℚ × WithBotTop ℚ)} (hD : AreSearchIntervals D) {b : ℕ} (hb : 0 < b) (H : ℕ) : List.Pairwise (fun (r s : ℤ × ℤ) => r.2 < s.1) (numeratorRanges b H D)

The normalized options

theorem Ratpoints.Options.reverse_normalize (o : Options) (H : ℕ) : (o.normalize H).reverse = (o.reverse && decide (IsFullBox o.domain o.bLow o.bHigh H))

theorem Ratpoints.Options.toNat_bHigh_normalize (o : Options) (H : ℕ) : (o.normalize H).bHigh.toNat = denominatorBound o.bHigh H

theorem Ratpoints.Options.one_le_toNat_bLow_normalize (o : Options) (H : ℕ) : 1 ≤ (o.normalize H).bLow.toNat

theorem Ratpoints.Options.one_le_toNat_bHigh_normalize (o : Options) {H : ℕ} (hH : 1 ≤ H) : 1 ≤ (o.normalize H).bHigh.toNat

theorem Ratpoints.Options.toNat_bHigh_normalize_le (o : Options) (H : ℕ) : (o.normalize H).bHigh.toNat ≤ H

theorem Ratpoints.Options.le_toNat_bHigh_normalize_iff (o : Options) {H : ℕ} {z : ℤ} (hzH : z ≤ ↑H) : z ≤ ↑(o.normalize H).bHigh.toNat ↔ o.bHigh < 1 ∨ z ≤ o.bHigh

A denominator z ≤ H lies below the normalized largest denominator exactly when it satisfies the bound of the search region of the specification (Ratpoints.InRegion).

theorem Ratpoints.Options.bLow_normalize_le_iff (o : Options) (H : ℕ) {z : ℤ} (hz : 1 ≤ z) : ↑(o.normalize H).bLow.toNat ≤ z ↔ o.bLow ≤ z

The normalized least denominator lies below a denominator z ≥ 1 exactly when the given one does.

theorem Ratpoints.Options.sturm_normalize_nonneg_iff (o : Options) (H : ℕ) : 0 ≤ (o.normalize H).sturm ↔ 0 ≤ o.sturm

theorem Ratpoints.Options.sturm_normalize_le (o : Options) (H : ℕ) : (o.normalize H).sturm ≤ 55

The depth of the Sturm step of the normalized options is at most 55 (Ratpoints.Double.mantDig + 2).

theorem Ratpoints.Options.sturm_normalize_neg_iff (o : Options) (H : ℕ) : (o.normalize H).sturm < 0 ↔ o.sturm < 0