theorem Hex.PolyQuot.Roots.componentRoots?_sound {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (multiplicity : ℕ) (hMultiplicity : 0 < multiplicity) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) {roots : Array RootCount} (hrun : componentRoots? f multiplicity hMultiplicity rep h = some roots) (entry : RootCount) : entry ∈ roots.toList → Polynomial.eval entry.root.toComplex (toPolynomialAt f rep h) = 0 ∧ entry.multiplicity = multiplicity

Every entry returned by a successful component run is a root at the selected embedding and carries the requested multiplicity.

theorem Hex.PolyQuot.Roots.componentRoots?_complete {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (multiplicity : ℕ) (hMultiplicity : 0 < multiplicity) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (hf : (!f.isZero) = true) {roots : Array RootCount} (hrun : componentRoots? f multiplicity hMultiplicity rep h = some roots) (z : ℂ) (hz : Polynomial.eval z (toPolynomialAt f rep h) = 0) : ∃ entry ∈ roots.toList, entry.root.toComplex = z ∧ entry.multiplicity = multiplicity

Every semantic root of a nonzero component occurs in a successful component run with the requested multiplicity.

theorem Hex.PolyQuot.contains_roots_iff {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (z : ℂ) : (roots f rep h).Contains z ↔ Polynomial.eval z (toPolynomialAt f rep h) = 0

Semantic membership in the fixed-field output is exactly polynomial vanishing.

theorem Hex.PolyQuot.multiplicity_roots {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (z : ℂ) : (roots f rep h).multiplicityOf z = Polynomial.rootMultiplicity z (toPolynomialAt f rep h)

Fixed-field root multiplicities agree with Mathlib multiplicities.

theorem Hex.PolyQuot.roots_positive {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (roots f rep h).Positive

The fixed-field driver produces positive multiplicities.

theorem Hex.PolyQuot.roots_noDuplicates {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (roots f rep h).NoDuplicates

The fixed-field driver merges all semantic duplicates.

theorem Hex.PolyQuot.roots_ordered {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (roots f rep h).Ordered

The fixed-field driver uses its deterministic canonical root order.

theorem Hex.PolyQuot.totalMultiplicity_roots {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (hf : toPolynomialAt f rep h ≠ 0) : (roots f rep h).totalMultiplicity = (toPolynomialAt f rep h).natDegree

For a nonzero fixed-field polynomial, the output multiplicities sum to its degree.