class Hex.ZPoly.CheckedIrreducible (p : ZPoly) : Prop

Runtime evidence that the factorization-backed irreducibility checker accepted an integer polynomial.

• is_true : p.isIrreducible = true

  The factorization-backed Boolean irreducibility checker accepted p.

• pos_degree : 0 < DensePoly.natDegree p

  p has positive degree, excluding the prime constants the integer checker also accepts.

structure Hex.PolyQuot (p : ZPoly) (x : SimpleRoot p) : Type

Canonical reduced rational coordinates in the fixed field ℚ(x).

• coeffs : DensePoly Rat

  Reduced rational coordinates in the power basis of the selected root.

• degree_lt : self.coeffs.natDegree < DensePoly.natDegree p

  The coordinates are already reduced modulo the defining polynomial.

structure Hex.AlgebraicRoot : Type

A factorization-lazy algebraic root with an eagerly certified isolating representative.

• p : ZPoly

  The enclosing integer polynomial; it need not be irreducible.

• prim : self.p.Primitive

  p has unit content.

• pos_lc : 0 < DensePoly.leadingCoeff self.p

  p has positive leading coefficient.

• pos_degree : 0 < DensePoly.natDegree self.p

  p has positive degree.

• squarefree : HasOnlySimpleRoots self.p

  p has only simple roots.

• x : SimpleRoot self.p

  The selected root of p.

• rep : RefinedIsolation self.p

  The certified refined isolation of the selected root.

• rep_mk : SimpleRoot.mk self.rep = self.x

  The stored representative selects exactly the root x.

def Hex.AlgebraicNumber.zeroRep : RefinedIsolation ZPoly.X

The fixed explicit representative of the root of X.

Equations

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

def Hex.AlgebraicNumber.IsCanonical (p : ZPoly) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) : Prop

Evidence that a representative is the deterministic representative stored by the canonical algebraic-number constructor.

Equations

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

def Hex.AlgebraicNumber.rawRep? (p : ZPoly) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (hzero : p ≠ ZPoly.X) : Option { r : RefinedIsolation p // IsCanonical p squarefree r ∧ r.sameRoot rep = true }

Run the deterministic representative-selection pipeline and retain its provenance together with the match against the supplied root.

Equations

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

def Hex.AlgebraicNumber.rawRepIn? (p : ZPoly) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (hzero : p ≠ ZPoly.X) (isolations : Array (DyadicRootIsolation p)) (refined : Array (RefinedIsolation p)) (hisolate : p.isolateComplexRoots? squarefree ↑(separationDepth p) = some isolations) (hrefine : Array.mapM DyadicRootIsolation.toRefined? isolations = some refined) : Option { r : RefinedIsolation p // IsCanonical p squarefree r ∧ r.sameRoot rep = true }

Select from an already computed deterministic isolation run. Its equations certify the provenance used by the canonical constructor; both proofs erase from compiled code.

Equations

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

theorem Hex.AlgebraicNumber.rawRepIn?_eq (p : ZPoly) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (hzero : p ≠ ZPoly.X) (isolations : Array (DyadicRootIsolation p)) (refined : Array (RefinedIsolation p)) (hisolate : p.isolateComplexRoots? squarefree ↑(separationDepth p) = some isolations) (hrefine : Array.mapM DyadicRootIsolation.toRefined? isolations = some refined) : rawRepIn? p squarefree rep hzero isolations refined hisolate hrefine = rawRep? p squarefree rep hzero

Reusing a certified isolation run preserves the complete selector result.

inductive Hex.AlgebraicNumber.RootSide : Type

The real axis or one of the two open half planes.

• real : RootSide
• upper : RootSide
• lower : RootSide

@[instance_reducible]

instance Hex.AlgebraicNumber.instDecidableEqRootSide : DecidableEq RootSide

Equations

• Hex.AlgebraicNumber.instDecidableEqRootSide x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.AlgebraicNumber.instBEqRootSide : BEq RootSide

Equations

• Hex.AlgebraicNumber.instBEqRootSide = { beq := Hex.AlgebraicNumber.instBEqRootSide.beq }

def Hex.AlgebraicNumber.instBEqRootSide.beq : RootSide → RootSide → Bool

Equations

• Hex.AlgebraicNumber.instBEqRootSide.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Hex.AlgebraicNumber.OrientedIsolation (p : ZPoly) : Type

An isolation with a canonical upper or real base and an orientation.

• base : RefinedIsolation p
• side : RootSide
• valid : match self.side with | RootSide.real => self.base.val.square.meetsRealAxis = true | RootSide.upper => self.base.val.square.radiusHi < self.base.val.square.im | RootSide.lower => self.base.val.square.radiusHi < self.base.val.square.im

def Hex.AlgebraicNumber.OrientedIsolation.rep {p : ZPoly} (r : OrientedIsolation p) : RefinedIsolation p

The effective isolation of an oriented root.

Equations

• r.rep = match r.side with | Hex.AlgebraicNumber.RootSide.lower => r.base.conj | x => r.base

def Hex.AlgebraicNumber.OrientedIsolation.conj {p : ZPoly} (r : OrientedIsolation p) : OrientedIsolation p

Reflect an oriented root without changing its base isolation.

Equations

• { base := base, side := Hex.AlgebraicNumber.RootSide.real, valid := h }.conj = { base := base, side := Hex.AlgebraicNumber.RootSide.real, valid := h }
• { base := base, side := Hex.AlgebraicNumber.RootSide.upper, valid := h }.conj = { base := base, side := Hex.AlgebraicNumber.RootSide.lower, valid := h }
• { base := base, side := Hex.AlgebraicNumber.RootSide.lower, valid := h }.conj = { base := base, side := Hex.AlgebraicNumber.RootSide.upper, valid := h }

@[simp]

theorem Hex.AlgebraicNumber.OrientedIsolation.conj_base {p : ZPoly} (r : OrientedIsolation p) : r.conj.base = r.base

def Hex.AlgebraicNumber.sideOf {p : ZPoly} (r : RefinedIsolation p) : RootSide

Determine the half plane of a refined isolation.

Equations

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

def Hex.AlgebraicNumber.orient? {p : ZPoly} (base : RefinedIsolation p) (side : RootSide) : Option (OrientedIsolation p)

Check that the base lies in the required half plane.

Equations

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

theorem Hex.AlgebraicNumber.orient?_base {p : ZPoly} {base : RefinedIsolation p} {side : RootSide} {r : OrientedIsolation p} (h : orient? base side = some r) : r.base = base

Successful orientation preserves the base.

def Hex.AlgebraicNumber.canonicalRep? (p : ZPoly) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (hzero : p ≠ ZPoly.X) : Option { r : OrientedIsolation p // IsCanonical p squarefree r.base ∧ r.rep.sameRoot rep = true }

Select the canonical upper representative and restore the requested orientation.

Equations

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

def Hex.AlgebraicNumber.canonicalRepIn? (p : ZPoly) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (hzero : p ≠ ZPoly.X) (isolations : Array (DyadicRootIsolation p)) (refined : Array (RefinedIsolation p)) (hisolate : p.isolateComplexRoots? squarefree ↑(separationDepth p) = some isolations) (hrefine : Array.mapM DyadicRootIsolation.toRefined? isolations = some refined) : Option { r : OrientedIsolation p // IsCanonical p squarefree r.base ∧ r.rep.sameRoot rep = true }

Canonical orientation using a certified deterministic isolation run.

Equations

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

theorem Hex.AlgebraicNumber.canonicalRepIn?_eq (p : ZPoly) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (hzero : p ≠ ZPoly.X) (isolations : Array (DyadicRootIsolation p)) (refined : Array (RefinedIsolation p)) (hisolate : p.isolateComplexRoots? squarefree ↑(separationDepth p) = some isolations) (hrefine : Array.mapM DyadicRootIsolation.toRefined? isolations = some refined) : canonicalRepIn? p squarefree rep hzero isolations refined hisolate hrefine = canonicalRep? p squarefree rep hzero

Certified reuse preserves the orientation and canonical stored isolation.

structure Hex.AlgebraicNumber : Type

A canonical algebraic number. Construction is sealed so each normalized polynomial/root pair receives one fixed representative.

• p : ZPoly

  The normalized minimal integer polynomial of the represented value.

• prim : self.p.Primitive

  p has unit content.

• pos_lc : 0 < DensePoly.leadingCoeff self.p

  p has positive leading coefficient.

• pos_degree : 0 < DensePoly.natDegree self.p

  p has positive degree.

• checked : self.p.CheckedIrreducible

  The Boolean irreducibility checker accepted p.

• squarefree : HasOnlySimpleRoots self.p

  p has only simple roots.

• isolation : OrientedIsolation self.p

  The canonical base isolation and the selected orientation.

• canonical : IsCanonical self.p ⋯ self.isolation.base

  The base comes from the deterministic isolation pipeline or explicit zero.

def Hex.AlgebraicNumber.rep (a : AlgebraicNumber) : RefinedIsolation a.p

The certified isolation of the selected complex root.

Equations

• a.rep = a.isolation.rep

def Hex.AlgebraicNumber.side (a : AlgebraicNumber) : RootSide

The half plane of the represented number.

Equations

• a.side = a.isolation.side

def Hex.AlgebraicNumber.conj (a : AlgebraicNumber) : AlgebraicNumber

Complex conjugation shares the canonical base and only changes orientation.

Equations

• a.conj = { p := a.p, prim := ⋯, pos_lc := ⋯, pos_degree := ⋯, checked := ⋯, squarefree := ⋯, isolation := a.isolation.conj, canonical := ⋯ }

@[simp]

theorem Hex.AlgebraicNumber.conj_conj (a : AlgebraicNumber) : a.conj.conj = a

Conjugation is an involution on the stored data.

@[simp]

theorem Hex.AlgebraicNumber.conj_p (a : AlgebraicNumber) : a.conj.p = a.p

theorem Hex.AlgebraicNumber.conj_rep (a : AlgebraicNumber) : a.conj.rep ≍ a.isolation.conj.rep

Conjugation exposes the reflected isolation without exposing the sealed constructor.

@[simp]

theorem Hex.AlgebraicNumber.conj_base_square (a : AlgebraicNumber) : a.conj.isolation.base.val.square = a.isolation.base.val.square

Conjugation preserves the canonical base square.

@[simp]

theorem Hex.AlgebraicNumber.conj_side (a : AlgebraicNumber) : a.conj.side = match a.side with | RootSide.real => RootSide.real | RootSide.upper => RootSide.lower | RootSide.lower => RootSide.upper

Conjugation flips precisely the two nonreal sides.

theorem Hex.AlgebraicNumber.conj_of_side_real (a : AlgebraicNumber) (h : a.side = RootSide.real) : a.conj = a

Real values are fixed by conjugation.

def Hex.AlgebraicNumber.x (a : AlgebraicNumber) : SimpleRoot a.p

The selected simple root is determined by the canonical representative.

Equations

• a.x = Hex.SimpleRoot.mk a.rep

@[simp]

theorem Hex.AlgebraicNumber.rep_mk (a : AlgebraicNumber) : SimpleRoot.mk a.rep = a.x

The stored canonical representative selects exactly the root a.x.

def Hex.AlgebraicNumber.zero : AlgebraicNumber

The canonical algebraic number zero, represented by the fixed explicit isolation of the normalized polynomial X.

Equations

• Hex.AlgebraicNumber.zero = Hex.AlgebraicNumber.zeroRaw✝

@[instance_reducible]

instance Hex.AlgebraicNumber.instZero : Zero AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instZero = { zero := Hex.AlgebraicNumber.zero }

theorem Hex.AlgebraicNumber.zero_eq_zero : zero = 0

The named canonical zero agrees with the Zero instance.

@[simp]

theorem Hex.AlgebraicNumber.zero_p : p 0 = ZPoly.X

The canonical zero retains X as its normalized polynomial.

@[simp]

theorem Hex.AlgebraicNumber.zero_square : (rep 0).val.square = { re := 0, im := 0, prec := ↑(separationDepth ZPoly.X) }

The canonical zero carries its explicit square centred on the real axis.

@[simp]

theorem Hex.AlgebraicNumber.zero_side : side 0 = RootSide.real

Zero lies on the real axis.

def Hex.AlgebraicNumber.ofNormalized? (p : ZPoly) (prim : p.Primitive) (pos_lc : 0 < DensePoly.leadingCoeff p) (pos_degree : 0 < DensePoly.natDegree p) (checked : p.CheckedIrreducible) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) : Option AlgebraicNumber

Re-isolate an already normalized irreducible polynomial with the fixed default strategy and retain the unique canonical disc matching rep.

The normalized polynomial X takes the explicit canonical-zero fast path, so the total Zero instance does not depend on success of a bounded driver. For all other inputs this is the implementation boundary used by later smart constructors. It is checked because failure of the bounded isolation driver is retired only by the theory companion's completeness proof.

Equations

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

def Hex.AlgebraicNumber.ofNormalizedIn? (p : ZPoly) (prim : p.Primitive) (pos_lc : 0 < DensePoly.leadingCoeff p) (pos_degree : 0 < DensePoly.natDegree p) (checked : p.CheckedIrreducible) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (isolations : Array (DyadicRootIsolation p)) (refined : Array (RefinedIsolation p)) (hisolate : p.isolateComplexRoots? squarefree ↑(separationDepth p) = some isolations) (hrefine : Array.mapM DyadicRootIsolation.toRefined? isolations = some refined) : Option AlgebraicNumber

Construct the identical canonical value using an isolation run already performed by the caller. The zero fast path remains explicit.

Equations

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

theorem Hex.AlgebraicNumber.ofNormalizedIn?_eq (p : ZPoly) (prim : p.Primitive) (pos_lc : 0 < DensePoly.leadingCoeff p) (pos_degree : 0 < DensePoly.natDegree p) (checked : p.CheckedIrreducible) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (isolations : Array (DyadicRootIsolation p)) (refined : Array (RefinedIsolation p)) (hisolate : p.isolateComplexRoots? squarefree ↑(separationDepth p) = some isolations) (hrefine : Array.mapM DyadicRootIsolation.toRefined? isolations = some refined) : ofNormalizedIn? p prim pos_lc pos_degree checked squarefree rep isolations refined hisolate hrefine = ofNormalized? p prim pos_lc pos_degree checked squarefree rep

Reuse preserves the complete checked constructor result, including its canonical stored representative and every failure branch.

theorem Hex.AlgebraicNumber.ofNormalized?_isSome_eq (p : ZPoly) (prim : p.Primitive) (pos_lc : 0 < DensePoly.leadingCoeff p) (pos_degree : 0 < DensePoly.natDegree p) (checked : p.CheckedIrreducible) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) : (ofNormalized? p prim pos_lc pos_degree checked squarefree rep).isSome = if _hzero : p = ZPoly.X then true else (canonicalRep? p squarefree rep _hzero).isSome

The success bit of canonicalization is exactly the success bit of its isolation, refinement, and representative-selection pipeline. This exposes the checked boundary needed by the Mathlib totality proof without exposing the sealed AlgebraicNumber constructor.

theorem Hex.AlgebraicNumber.ofNormalized?_p (p : ZPoly) (prim : p.Primitive) (pos_lc : 0 < DensePoly.leadingCoeff p) (pos_degree : 0 < DensePoly.natDegree p) (checked : p.CheckedIrreducible) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) {a : AlgebraicNumber} (h : ofNormalized? p prim pos_lc pos_degree checked squarefree rep = some a) : a.p = p

Successful canonicalization retains the supplied normalized polynomial.

theorem Hex.AlgebraicNumber.canonical_transport (a : AlgebraicNumber) (p : ZPoly) (h : a.p = p) : IsCanonical p ⋯ (h ▸ a.isolation).base

Canonicality is preserved when the defining polynomial is identified.

def Hex.AlgebraicNumber.ofNormalized (p : ZPoly) (prim : p.Primitive) (pos_lc : 0 < DensePoly.leadingCoeff p) (pos_degree : 0 < DensePoly.natDegree p) (checked : p.CheckedIrreducible) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (h : (ofNormalized? p prim pos_lc pos_degree checked squarefree rep).isSome = true) : AlgebraicNumber

The checked total constructor retains the defining polynomial as literal data. Its root is the same canonical root returned by ofNormalized?; reading the polynomial does not replay the isolation pipeline.

Equations

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

@[simp]

theorem Hex.AlgebraicNumber.ofNormalized_p (p : ZPoly) (prim : p.Primitive) (pos_lc : 0 < DensePoly.leadingCoeff p) (pos_degree : 0 < DensePoly.natDegree p) (checked : p.CheckedIrreducible) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (h : (ofNormalized? p prim pos_lc pos_degree checked squarefree rep).isSome = true) : (ofNormalized p prim pos_lc pos_degree checked squarefree rep h).p = p

theorem Hex.AlgebraicNumber.ofNormalized?_spec (p : ZPoly) (prim : p.Primitive) (pos_lc : 0 < DensePoly.leadingCoeff p) (pos_degree : 0 < DensePoly.natDegree p) (checked : p.CheckedIrreducible) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) {a : AlgebraicNumber} (h : ofNormalized? p prim pos_lc pos_degree checked squarefree rep = some a) : p = ZPoly.X ∧ a = 0 ∨ ∃ (hp : a.p = p), Intersects (hp ▸ a.rep) rep

A successful canonicalization either takes the explicit zero path or stores a representative intersecting the supplied isolation. This is the Mathlib-free behavioral boundary used by semantic soundness proofs.

@[instance_reducible]

instance Hex.AlgebraicNumber.instInhabited : Inhabited AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instInhabited = { default := Hex.AlgebraicNumber.zero }

theorem Hex.AlgebraicNumber.ext (a b : AlgebraicNumber) (hp : a.p = b.p) (hisolation : a.isolation ≍ b.isolation) : a = b

Two canonical values are equal once their dependent polynomials and stored representatives agree. The remaining fields are propositions, and the selected SimpleRoot is forced by rep_mk.

def Hex.RefinedIsolation.containsZero {p : ZPoly} (r : RefinedIsolation p) : Bool

Closed-disc membership test for zero, including boundary contact.

Equations

• r.containsZero = r.val.square.discContains (0, 0)

def Hex.AlgebraicNumber.beq (a b : AlgebraicNumber) : Bool

Canonical equality: compare minimal polynomials, then the selected roots.

Equations

• a.beq b = (a.p == b.p && a.rep.val.square.discsMeet b.rep.val.square)

@[instance_reducible]

instance Hex.instBEqAlgebraicNumber : BEq AlgebraicNumber

Equations

• Hex.instBEqAlgebraicNumber = { beq := Hex.AlgebraicNumber.beq }

def Hex.AlgebraicNumber.isZero (a : AlgebraicNumber) : Bool

A canonical algebraic number is zero exactly when its minimal polynomial is X.

Equations

• a.isZero = (a.p == Hex.ZPoly.X)

def Hex.AlgebraicRoot.isZero (a : AlgebraicRoot) : Bool

The selected lazy root is zero exactly when its polynomial has zero constant coefficient and its closed isolating disc contains zero. The refined separation bound makes this test decisive between distinct simple roots.

Equations

• a.isZero = (Hex.DensePoly.coeff a.p 0 == 0 && a.rep.containsZero)

def Hex.panicWith {α : Sort u_1} (fallback : α) (message : String) : α

Print a diagnostic in compiled code and return the supplied fallback.

Equations

• Hex.panicWith fallback message = Batteries.panicWith fallback message

structure Hex.RootCount : Type

A root paired with its positive multiplicity.

• root : AlgebraicRoot

  The recorded root.

• multiplicity : Nat

  The multiplicity of the root in the polynomial being solved.

• multiplicity_pos : 0 < self.multiplicity

  Roots are recorded only with positive multiplicity.

inductive Hex.RootSet : Type

A polynomial root set; .all is reserved for the zero polynomial.

• all : RootSet
• finite (roots : Array RootCount) : RootSet

def Hex.RootSet.finite? : RootSet → Option (Array RootCount)

The recorded roots of a nonzero polynomial, or none for the zero polynomial, every number being a root of that.

Equations

• (Hex.RootSet.finite roots).finite? = some roots
• Hex.RootSet.all.finite? = none

def Hex.RootSet.toArray (roots : RootSet) : Array RootCount

The recorded roots, with the zero polynomial giving the empty array.

Equations

• roots.toArray = roots.finite?.getD #[]

@[simp]

theorem Hex.RootSet.finite?_finite (roots : Array RootCount) : (finite roots).finite? = some roots

@[simp]

theorem Hex.RootSet.finite?_all : all.finite? = none

@[simp]

theorem Hex.RootSet.toArray_finite (roots : Array RootCount) : (finite roots).toArray = roots

@[simp]

theorem Hex.RootSet.toArray_all : all.toArray = #[]