theorem Polynomial.sign_eq_of_noRoot {p : Polynomial ℝ} {s : Set ℝ} (hs : IsPreconnected s) (hnz : ∀ z ∈ s, ¬p.IsRoot z) {x y : ℝ} (hx : x ∈ s) (hy : y ∈ s) : SignType.sign (eval x p) = SignType.sign (eval y p)

The sign of a continuous polynomial evaluation is constant on a preconnected set containing no root of the polynomial.

theorem Hex.RCF.Cell.rank_injective {n : ℕ} : Function.Injective rank

rank is an injective encoding of the alternating cell order.

def Hex.RCF.Cell.Region {n : ℕ} (root : Fin n → ℝ) : Cell n → ℝ → Prop

Membership in a singleton or open interval cut out by a finite list of real points.

Equations

• One or more equations did not get rendered due to their size.
• Hex.RCF.Cell.Region root (Hex.RCF.Cell.root i) x✝ = (x✝ = root i)

theorem Hex.RCF.Cell.Region.exists_mem {n : ℕ} (root : Fin n → ℝ) (x : ℝ) : ∃ (c : Cell n), Region root c x

Every real point belongs to at least one semantic cell.

theorem Hex.RCF.Cell.Region.lt_of_rank_lt {n : ℕ} (root : Fin n → ℝ) (hmono : StrictMono root) {c d : Cell n} {x y : ℝ} (hcd : c.rank < d.rank) (hx : Region root c x) (hy : Region root d y) : x < y

Cells earlier in the alternating enumeration lie strictly to the left.

theorem Hex.RCF.Cell.Region.unique_mem {n : ℕ} (root : Fin n → ℝ) (hmono : StrictMono root) (x : ℝ) {c d : Cell n} (hc : Region root c x) (hd : Region root d x) : c = d

Semantic cell membership is unique.

theorem Hex.RCF.Cell.Region.existsUnique_mem {n : ℕ} (root : Fin n → ℝ) (hmono : StrictMono root) (x : ℝ) : ∃! c : Cell n, Region root c x

The semantic cells form a genuine partition of the real line.

theorem Hex.RCF.Cell.Region.open_ne {n : ℕ} (root : Fin n → ℝ) (hmono : StrictMono root) {cut : Fin (n + 1)} {x : ℝ} (hx : Region root («open» cut) x) (i : Fin n) : x ≠ root i

An open cell contains none of the points defining the partition.

theorem Hex.RCF.Cell.Region.exists_point {n : ℕ} (root : Fin n → ℝ) (hmono : StrictMono root) (c : Cell n) : ∃ (x : ℝ), Region root c x

Every semantic cell contains a real point.

theorem Hex.RCF.Cell.Region.isPreconnected_open {n : ℕ} (root : Fin n → ℝ) (cut : Fin (n + 1)) : IsPreconnected {x : ℝ | Region root («open» cut) x}

Every open semantic cell is an interval, hence preconnected.

theorem Hex.RCF.Cell.Region.sign_eq {n : ℕ} (root : Fin n → ℝ) (hmono : StrictMono root) (p : Polynomial ℝ) (hroots : p = 0 ∨ ∀ (z : ℝ), p.IsRoot z → ∃ (i : Fin n), root i = z) (c : Cell n) {x y : ℝ} (hx : Region root c x) (hy : Region root c y) : SignType.sign (Polynomial.eval x p) = SignType.sign (Polynomial.eval y p)

Polynomial signs are constant on each cell when the defining points contain every root. The zero polynomial is handled separately, since its root set cannot be contained in a finite list.