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.canonicalRep? (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.

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.

• rep : RefinedIsolation self.p

  The certified refined isolation of the represented root.

• canonical : IsCanonical self.p ⋯ self.rep

  The stored representative comes from the deterministic canonical isolation pipeline (or is the fixed representative of zero).

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.

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 Mathlib companion's completeness proof.

Equations

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

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.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) (hrep : a.rep ≍ b.rep) : 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 = #[]