The search region after the Sturm step

The Sturm step of the search (Ratpoints.sturmRegion) refuses exactly when the remainder chain does, leaves the search intervals as they are when it is off, and otherwise, at a depth of at most 55, leaves well-formed intervals inside the given ones (Ratpoints.run_sturmRegion_subset, from Ratpoints.Sturm.computeSturm_wf); assuming Sturm's theorem (Ratpoints.SturmTheorem), for a polynomial of degree d < 2 ^ 57 every a / b with |a| ≤ 2 ^ 63 of the given intervals with F(a, b) ≥ 0, in particular the x / z of every point, lies in one of the intervals that it leaves (Ratpoints.run_sturmRegion_covers, from Ratpoints.Sturm.covers_computeSturm). The search region of the search that Ratpoints.findPointsWith runs (Ratpoints.searchRegion), over the values of the ends of its intervals, lies inside the caller's search intervals, and assuming Sturm's theorem when the step is on, it holds the x / z of every point in them.

Main definitions

• Ratpoints.searchRegion: the search intervals of the search after the Sturm step, over the values of their ends, or none when the step returns before the search.

Main statements

• Ratpoints.run_sturmRegion_eq_error_iff, Ratpoints.run_sturmRegion_of_neg, Ratpoints.run_sturmRegion_eq_ok_none: the refusal of the Sturm step, the step off, and the return before the search, only for even degree and a leading coefficient that is not a square.
• Ratpoints.run_sturmRegion_subset: the intervals that the step leaves at a depth of at most 55, where the search clamps it, are well formed and lie inside the given ones.
• Ratpoints.run_sturmRegion_covers: assuming Sturm's theorem, they hold every a / b of the given intervals with F(a, b) ≥ 0 and |a| ≤ 2 ^ 63.
• Ratpoints.searchRegion_subset, Ratpoints.searchRegion_covers, Ratpoints.searchRegion_eq_none: the search region inside the caller's intervals, holding the x / z of every point in them, and none only for even degree and a leading coefficient that is not a square.

The Sturm step

theorem Ratpoints.run_sturmRegion_of_neg (c : List ℤ) (d : ℕ) {s : ℤ} (hs : s < 0) (dom : List (Double × Double)) : (sturmRegion c d s dom).run = Except.ok (some (dom, false))

theorem Ratpoints.run_sturmRegion_of_nonneg (c : List ℤ) (d : ℕ) {s : ℤ} (hs : 0 ≤ s) (dom : List (Double × Double)) : (sturmRegion c d s dom).run = match (Sturm.computeSturm c d s.toNat dom.toArray).run with | none => Except.error Refusal.notSquarefree | some iv => if iv = #[] then if d % 2 = 1 ∨ Setup.isSquare (c.getD d 0) = true then Except.ok (some ([], true)) else Except.ok none else Except.ok (some (iv.toList, false))

The Sturm step on, by the result of Ratpoints.Sturm.computeSturm.

theorem Ratpoints.run_sturmRegion_eq_error_iff (c : List ℤ) (d : ℕ) (s : ℤ) (dom : List (Double × Double)) (e : Refusal) : (sturmRegion c d s dom).run = Except.error e ↔ 0 ≤ s ∧ (Sturm.chain c d).run = none ∧ e = Refusal.notSquarefree

The Sturm step refuses exactly when it is on and the remainder chain fails (Ratpoints.Sturm.run_computeSturm_eq_none_iff).

theorem Ratpoints.run_sturmRegion_eq_ok_none {c : List ℤ} {d : ℕ} {s : ℤ} {dom : List (Double × Double)} (h : (sturmRegion c d s dom).run = Except.ok none) : d % 2 = 0 ∧ Setup.isSquare (c.getD d 0) = false

The Sturm step returns before the search only for even degree and a leading coefficient that is not a square, when there is no point at infinity.

theorem Ratpoints.run_sturmRegion_subset {c : List ℤ} {d : ℕ} {s : ℤ} {dom dom' : List (Double × Double)} {empty : Bool} (hs : s ≤ 55) (hdom : IntervalsWF (domainBits dom)) (h : (sturmRegion c d s dom).run = Except.ok (some (dom', empty))) : IntervalsWF (domainBits dom') ∧ (empty = true → dom' = []) ∧ ∀ (x : ℚ), InIntervals (domainValues dom') x → InIntervals (domainValues dom) x

The intervals that the Sturm step at a depth of at most 55 leaves for well-formed intervals are well formed (Ratpoints.Sturm.computeSturm_wf), none when it sets sturm_empty, and lie inside the given ones.

theorem Ratpoints.run_sturmRegion_covers {c : List ℤ} {d : ℕ} {s : ℤ} {dom : List (Double × Double)} {r : Option (List (Double × Double) × Bool)} (hS : 0 ≤ s → SturmTheorem) (hs : s ≤ 55) (hdom : IntervalsWF (domainBits dom)) (hd : d = degree c) (hd0 : 0 < d) (hd57 : d < 2 ^ 57) (h : (sturmRegion c d s dom).run = Except.ok r) {a : ℤ} {b : ℕ} (hb : 0 < b) (ha : a.natAbs ≤ 2 ^ 63) (hF : 0 ≤ binaryForm c a ↑b) (hx : InIntervals (domainValues dom) (↑a / ↑b)) : ∃ (dom' : List (Double × Double)), r = some (dom', false) ∧ InIntervals (domainValues dom') (↑a / ↑b)

Assuming Sturm's theorem when the step is on, the intervals that the Sturm step at a depth of at most 55 leaves for well-formed intervals and the polynomial c of degree 0 < d < 2 ^ 57 hold every a / b, b ≥ 1, |a| ≤ 2 ^ 63, of the given intervals with F(a, b) ≥ 0 (Ratpoints.Sturm.covers_computeSturm): the step does not return before the search then, and does not set sturm_empty.

The search region of the search

def Ratpoints.searchRegion (c : List ℤ) (d H : ℕ) (o : Options) : Option (List (WithBotTop ℚ × WithBotTop ℚ))

The search intervals, over the values of their ends, of the search that Ratpoints.findPointsWith runs for the options o and the height bound H on the polynomial c of degree d that the reversal check hands on, after the Sturm step: none when the step returns before the search (find_points.c:4889), no intervals when it leaves none (sturm_empty, the search delivering the points at infinity only), and otherwise the values of the intervals that it leaves, inside those of the caller or the default interval (Ratpoints.searchIntervals). Junk (none) for the search intervals and the polynomials that Ratpoints.findPointsWith refuses.

Equations

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

theorem Ratpoints.searchRegion_subset {c : List ℤ} {d H : ℕ} {o : Options} {D : List (WithBotTop ℚ × WithBotTop ℚ)} (hdom : IntervalsWF (domainBits o.domain)) (h : searchRegion c d H o = some D) (x : ℚ) (hx : InIntervals D x) : o.domain = [] ∨ InIntervals (domainValues o.domain) x

The search region of the search lies inside the caller's search intervals, when there are some.

theorem Ratpoints.searchRegion_covers {c : List ℤ} {d H : ℕ} {o : Options} (hS : 0 ≤ o.sturm → SturmTheorem) (hdom : IntervalsWF (domainBits o.domain)) (hd : d = degree c) (hd0 : 0 < d) (hd57 : d < 2 ^ 57) (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) (hc : 0 ≤ o.sturm → (Sturm.chain c d).run ≠ none) {a : ℤ} {b : ℕ} (hb : 0 < b) (ha : a.natAbs ≤ H) (hF : 0 ≤ binaryForm c a ↑b) (hx : o.domain = [] ∨ InIntervals (domainValues o.domain) (↑a / ↑b)) : ∃ (D : List (WithBotTop ℚ × WithBotTop ℚ)), searchRegion c d H o = some D ∧ InIntervals D (↑a / ↑b)

Assuming Sturm's theorem when the step is on, the search region of the search for the polynomial c of degree 0 < d < 2 ^ 57, 1 ≤ H < 2 ^ 63 and well-formed search intervals of the caller holds every a / b with b ≥ 1, |a| ≤ H and F(a, b) ≥ 0 in the caller's intervals (anywhere when there are none), when the Sturm step does not refuse.

theorem Ratpoints.searchRegion_eq_none {c : List ℤ} {d H : ℕ} {o : Options} (hdom : IntervalsWF (domainBits o.domain)) (hc : 0 ≤ o.sturm → (Sturm.chain c d).run ≠ none) (h : searchRegion c d H o = none) : d % 2 = 0 ∧ Setup.isSquare (c.getD d 0) = false

The search region of the search is none only for even degree and a leading coefficient that is not a square, when the search intervals are well formed and the Sturm step does not refuse.

theorem Ratpoints.searchRegion_eq_of_run_sturmRegion_eq {c : List ℤ} {d H : ℕ} {o : Options} {dom : List (Double × Double)} (hsi : (searchIntervals H o.domain).run = some dom) {r : Option (List (Double × Double) × Bool)} (hst : (sturmRegion c d (o.normalize H).sturm dom).run = Except.ok r) : searchRegion c d H o = Option.map (fun (x : List (Double × Double) × Bool) => if x.2 = true then [] else domainValues x.1) r

The search region of the search, from the result of the Sturm step on the search intervals of Ratpoints.searchIntervals.

theorem Ratpoints.chain_ne_none_of_run_sturmRegion_eq_ok {c : List ℤ} {d H : ℕ} {o : Options} {dom : List (Double × Double)} {r : Option (List (Double × Double) × Bool)} (h : (sturmRegion c d (o.normalize H).sturm dom).run = Except.ok r) (hs : 0 ≤ o.sturm) : (Sturm.chain c d).run ≠ none

When the Sturm step of the normalized options is on and does not refuse, the remainder chain succeeds (Ratpoints.run_sturmRegion_eq_error_iff).