structure HexRealRootsMathlib.LiteralIsolation (count : Hex.DyadicInterval → ℤ) : Type

One interval certified by an externally supplied integer root count.

• interval : Hex.DyadicInterval

  The half-open interval (lower, upper].

• count_one : count self.interval = 1

  The supplied count says that the interval contains one root.

structure HexRealRootsMathlib.LiteralIsolations (count : Hex.DyadicInterval → ℤ) (total : ℤ) : Type

An ordered, complete array of intervals certified by externally supplied interval and total root counts.

• isolations : Array (LiteralIsolation count)

  The count-one intervals.

• ordered (i j : Fin self.isolations.size) : i < j → self.isolations[i].interval.upper ≤ self.isolations[j].interval.lower

  Earlier half-open intervals end no later than later intervals begin.

• complete : total = ↑self.isolations.size

  The supplied total count agrees with the number of intervals.

theorem HexRealRootsMathlib.LiteralIsolation.exists_unique_root {p : Hex.ZPoly} {count : Hex.DyadicInterval → ℤ} (hp : p ≠ 0) (iso : LiteralIsolation count) (hcount : count iso.interval = ↑(Literal.rootsIn (toPolyℝ p) iso.interval).card) : ∃! r : ℝ, (toPolyℝ p).IsRoot r ∧ Literal.InInterval iso.interval r

A literal count of one denotes exactly one real root in the interval.

No squarefreeness hypothesis is needed locally: the exact multiset count of the interval is already one. Nonzeroness is needed to pass between IsRoot and membership in Polynomial.roots.

theorem HexRealRootsMathlib.LiteralIsolations.isolates {p : Hex.ZPoly} {count : Hex.DyadicInterval → ℤ} {total : ℤ} (hp : p ≠ 0) (hsf : Squarefree (toPolyℝ p)) (out : LiteralIsolations count total) (hcount : ∀ (i : Fin out.isolations.size), count out.isolations[i].interval = ↑(Literal.rootsIn (toPolyℝ p) out.isolations[i].interval).card) (htotal : total = ↑(toPolyℝ p).roots.card) (r : ℝ) : (toPolyℝ p).IsRoot r → ∃! i : Fin out.isolations.size, Literal.InInterval out.isolations[i].interval r

An ordered complete array of literal count-one intervals captures every real root at exactly one array index.

Squarefreeness is used only to show that the root multiset has no duplicate elements, so equality of the supplied total count with roots.card measures the number of distinct roots.