noncomputable def HexRealRootsMathlib.theRoot {p : Hex.ZPoly} (hp : p.SquareFreeRat) (iso : Hex.RefinedRealIsolation p) : ℝ

The unique real root isolated by a refined isolation, delivered by RealRootIsolation.exists_unique_root for the underlying RealRootIsolation.

Equations

• HexRealRootsMathlib.theRoot hp iso = Exists.choose ⋯

theorem HexRealRootsMathlib.theRoot_isRoot {p : Hex.ZPoly} (hp : p.SquareFreeRat) (iso : Hex.RefinedRealIsolation p) : (toPolyℝ p).IsRoot (theRoot hp iso)

theRoot is a root of toPolyℝ p.

theorem HexRealRootsMathlib.theRoot_lt {p : Hex.ZPoly} (hp : p.SquareFreeRat) (iso : Hex.RefinedRealIsolation p) : Dyadic.toReal (↑iso).interval.lower < theRoot hp iso

theRoot lies strictly above the isolation's lower endpoint.

theorem HexRealRootsMathlib.theRoot_le {p : Hex.ZPoly} (hp : p.SquareFreeRat) (iso : Hex.RefinedRealIsolation p) : theRoot hp iso ≤ Dyadic.toReal (↑iso).interval.upper

theRoot lies at or below the isolation's upper endpoint.

theorem HexRealRootsMathlib.overlaps_iff_same_root {p : Hex.ZPoly} (hp : p.SquareFreeRat) (i₁ i₂ : Hex.RefinedRealIsolation p) : Hex.Overlaps i₁ i₂ ↔ theRoot hp i₁ = theRoot hp i₂

Overlaps classes are the real roots. Two refined isolations of p overlap iff they name the same real root of toPolyℝ p.

Forward: both widths are ≤ 2^{−sepPrec p}, below sep(p)/4; an overlap point sits within one width of each root, so the two roots are less than 4 · 2^{−sepPrec p} apart, and sepPrec_separates' forces them equal. Backward: a common root lies in both half-open intervals, so max lower (below the root) is under min upper (at or above it).

noncomputable def Hex.SimpleRealRoot.toReal {p : ZPoly} (hp : p.SquareFreeRat) : SimpleRealRoot p → ℝ

The real value of a root identity: theRoot lifted through the overlap quotient. Well-defined by the forward direction of overlaps_iff_same_root.

Equations

• Hex.SimpleRealRoot.toReal hp = Quot.lift (HexRealRootsMathlib.theRoot hp) ⋯

theorem Hex.SimpleRealRoot.toReal_isRoot {p : ZPoly} (hp : p.SquareFreeRat) (s : SimpleRealRoot p) : (HexRealRootsMathlib.toPolyℝ p).IsRoot (toReal hp s)

The lifted value is a genuine root of toPolyℝ p.

theorem Hex.SimpleRealRoot.toReal_injective {p : ZPoly} (hp : p.SquareFreeRat) : Function.Injective (toReal hp)

Distinct root identities name distinct reals: toReal is injective. The backward direction of overlaps_iff_same_root produces the Overlaps witness that Quot.sound needs.

theorem HexRealRootsMathlib.sameRoot_iff {p : Hex.ZPoly} (hp : p.SquareFreeRat) (i₁ i₂ : Hex.RefinedRealIsolation p) : i₁.sameRoot i₂ = true ↔ Hex.SimpleRealRoot.mk i₁ = Hex.SimpleRealRoot.mk i₂

sameRoot decides equality in SimpleRealRoot p. The executable boolean overlap test on refined isolations is true exactly when they are the same element of the quotient.