theorem Hex.AlgebraicNumber.OrientedIsolation.sign {p : ZPoly} (r : OrientedIsolation p) : match r.side with | RootSide.real => r.rep.root.im = 0 | RootSide.upper => 0 < r.rep.root.im | RootSide.lower => r.rep.root.im < 0

The orientation records the exact sign of the imaginary part.

theorem Hex.AlgebraicNumber.OrientedIsolation.real_iff {p : ZPoly} (r : OrientedIsolation p) : r.side = RootSide.real ↔ r.rep.root.im = 0

The real tag characterizes real values.

theorem Hex.AlgebraicNumber.OrientedIsolation.side_eq_of_im_eq {p q : ZPoly} (r : OrientedIsolation p) (s : OrientedIsolation q) (h : r.rep.root.im = s.rep.root.im) : r.side = s.side

Equal imaginary parts have the same orientation, even in different fields.

theorem Hex.AlgebraicNumber.OrientedIsolation.side_eq {p : ZPoly} (r s : OrientedIsolation p) (h : r.rep.root = s.rep.root) : r.side = s.side

Equal complex values have the same orientation.

theorem Hex.AlgebraicNumber.OrientedIsolation.base_root_eq {p : ZPoly} (r s : OrientedIsolation p) (h : r.rep.root = s.rep.root) : r.base.root = s.base.root

Equal oriented values have equal base values.

theorem Hex.AlgebraicNumber.OrientedIsolation.ext {p : ZPoly} (r s : OrientedIsolation p) (hb : r.base = s.base) (hs : r.side = s.side) : r = s

Orientation and the base determine all stored data.

theorem Hex.AlgebraicNumber.OrientedIsolation.conj_root {p : ZPoly} (r : OrientedIsolation p) : r.conj.rep.root = (starRingEnd ℂ) r.rep.root

Flipping orientation conjugates the represented value.

theorem Hex.AlgebraicNumber.sideOf_root {p : ZPoly} (r : RefinedIsolation p) : sideOf r = if r.root.im = 0 then RootSide.real else if 0 < r.root.im then RootSide.upper else RootSide.lower

Half-plane classification depends only on the represented complex value.

theorem Hex.AlgebraicNumber.orient?_exists {p : ZPoly} (r base : RefinedIsolation p) (hb : base.root = (if sideOf r = RootSide.lower then r.conj else r).root) : ∃ (s : OrientedIsolation p), orient? base (sideOf r) = some s ∧ s.rep.root = r.root

Reorienting a matching upper representative succeeds and preserves the root.