theorem Hex.AlgebraicRoot.side_value (a : AlgebraicRoot) : a.side = if a.toComplex.im = 0 then AlgebraicNumber.RootSide.real else if 0 < a.toComplex.im then AlgebraicNumber.RootSide.upper else AlgebraicNumber.RootSide.lower

Lazy half-plane classification agrees with the selected complex value.

theorem Hex.AlgebraicRoot.side_nonneg (a : AlgebraicRoot) : a.side ≠ AlgebraicNumber.RootSide.lower ↔ 0 ≤ a.toComplex.im

The lower tag is exactly the negative imaginary half plane.

theorem Hex.RootSelection.same_sound (a b : AlgebraicRoot) (h : same a b = true) : a.toComplex = b.toComplex

A successful same-polynomial test identifies the selected complex value.

theorem Hex.RootSelection.dominates_sound (a b : Work) (h : dominates a b = true) : b.root.toComplex.re ≤ a.root.toComplex.re

Every accepted domination check is an inequality of actual real coordinates.

theorem Hex.RootSelection.probe_spec (roots : List Work) {a : Work} (h : probe roots = some a) : a ∈ roots ∧ ∀ b ∈ roots, b.root.toComplex.re ≤ a.root.toComplex.re

A validated proposal is an input and dominates every input.

theorem Hex.RootSelection.refine?_value (bits : ℕ) (a : Work) {b : Work} (h : refine? bits a = some b) : b.root.toComplex = a.root.toComplex

Refinement updates only the enclosure of a lazy value.

theorem Hex.RootSelection.refine_list (bits : ℕ) (roots : List Work) {out : List Work} (h : List.mapM (refine? bits) roots = some out) : List.map (fun (a : Work) => a.root.toComplex) out = List.map (fun (a : Work) => a.root.toComplex) roots

Refining an array preserves its entire ordered value list.

theorem Hex.RootSelection.search_spec (rounds : List ℕ) (roots : List Work) {a : AlgebraicRoot} (h : search rounds roots = some a) : a.toComplex ∈ List.map (fun (r : Work) => r.root.toComplex) roots ∧ ∀ z ∈ List.map (fun (r : Work) => r.root.toComplex) roots, z.re ≤ a.toComplex.re

Every successful bounded search certifies membership and maximal real coordinate.

theorem Hex.RootSelection.select?_spec (roots : List AlgebraicRoot) {a : AlgebraicRoot} (h : select? roots = some a) : a.toComplex ∈ List.map AlgebraicRoot.toComplex roots ∧ ∀ z ∈ List.map AlgebraicRoot.toComplex roots, z.re ≤ a.toComplex.re

Public lazy selection is sound independently of the refinement budget.

theorem Hex.AlgebraicNumber.Radical.rank_nonneg (a : AlgebraicNumber) : 0 ≤ rank a ↔ 0 ≤ a.toComplex.im

Imaginary-side ranking detects the nonnegative half plane.

def Hex.AlgebraicNumber.Radical.Dominates (a b : Candidate) : Prop

Lexicographic dominance by real coordinate and imaginary side.

Equations

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

theorem Hex.AlgebraicNumber.Radical.select_spec (roots : Array RootCount) (hne : roots.toList ≠ []) : ∃ (c : Candidate), select roots = some c ∧ (∃ r ∈ roots.toList, c = candidate r) ∧ ∀ r ∈ roots.toList, Dominates c (candidate r)

The exact reference selector returns an input dominating every input.

theorem Hex.RootSelection.maximum?_spec (roots : List AlgebraicRoot) (hne : roots ≠ []) : ∃ (a : AlgebraicNumber), maximum? roots = some a ∧ a.toComplex ∈ List.map AlgebraicRoot.toComplex roots ∧ ∀ z ∈ List.map AlgebraicRoot.toComplex roots, z.re ≤ a.toComplex.re

The shared maximum selector succeeds on nonempty inputs and preserves its contract whether the interval path or the exact reference supplies the result.