theorem Hex.AlgebraicPoly.Common.rational?_isSome (q : ℚ) : (rational? q).isSome = true

Checked canonical construction of a rational algebraic number is total.

theorem Hex.AlgebraicPoly.Common.rational?_sound (q : ℚ) {a : AlgebraicNumber} (h : rational? q = some a) : a.toComplex = ↑q

Checked canonical construction of a rational preserves its value.

theorem Hex.AlgebraicPoly.Common.add?_isSome (a b : AlgebraicNumber) : (add? a b).isSome = true

Checked canonical addition is total.

theorem Hex.AlgebraicPoly.Common.add?_sound (a b : AlgebraicNumber) {c : AlgebraicNumber} (h : add? a b = some c) : c.toComplex = a.toComplex + b.toComplex

Checked canonical addition preserves the represented complex value.

theorem Hex.AlgebraicPoly.Common.mul?_isSome (a b : AlgebraicNumber) : (mul? a b).isSome = true

Checked canonical multiplication is total.

theorem Hex.AlgebraicPoly.Common.mul?_sound (a b : AlgebraicNumber) {c : AlgebraicNumber} (h : mul? a b = some c) : c.toComplex = a.toComplex * b.toComplex

Checked canonical multiplication preserves the represented complex value.

theorem Hex.AlgebraicPoly.Common.scale?_isSome (c : ℤ) (a : AlgebraicNumber) : (scale? c a).isSome = true

Checked integer scaling is total.

theorem Hex.AlgebraicPoly.Common.scale?_sound (c : ℤ) (a : AlgebraicNumber) {b : AlgebraicNumber} (h : scale? c a = some b) : b.toComplex = ↑c * a.toComplex

A successful checked integer scaling has the expected value.

theorem Hex.AlgebraicPoly.Common.shift?_isSome (theta alpha : AlgebraicNumber) (c : ℤ) : (shift? theta alpha c).isSome = true

A checked primitive-element shift is total.

theorem Hex.AlgebraicPoly.Common.shift?_sound (theta alpha : AlgebraicNumber) (c : ℤ) {candidate : AlgebraicNumber} (h : shift? theta alpha c = some candidate) : candidate.toComplex = theta.toComplex + ↑c * alpha.toComplex

A successful checked primitive-element shift has the expected value.

theorem Hex.AlgebraicPoly.Common.degree_eq_minpoly (a : AlgebraicNumber) : degree a = (minpoly ℚ a.toComplex).natDegree

The executable degree is the degree of the rational minimal polynomial.

theorem Hex.AlgebraicPoly.Common.isIntegral_toComplex (a : AlgebraicNumber) : IsIntegral ℚ a.toComplex

The complex value represented by a canonical algebraic number is algebraic over the rationals.

theorem Hex.AlgebraicPoly.Common.degree_pos (a : AlgebraicNumber) : 0 < degree a

Every canonical algebraic number has positive degree.

theorem Hex.AlgebraicPoly.Common.signedShift_injective : Function.Injective signedShift

The deterministic signed-shift enumeration never repeats a scalar.

theorem Hex.AlgebraicPoly.Common.extendShift?_isSome (theta alpha : AlgebraicNumber) : (extendShift? theta alpha).isSome = true

The shift-retaining primitive search is total.

theorem Hex.AlgebraicPoly.Common.extendShift?_value (theta alpha : AlgebraicNumber) : Option.map ShiftCandidate.value (extendShift? theta alpha) = extend? theta alpha

Retaining the producing shift does not change the selected primitive element.

theorem Hex.AlgebraicPoly.Common.extend?_isSome (theta alpha : AlgebraicNumber) : (extend? theta alpha).isSome = true

The bounded maximum-degree primitive-element search is operationally total. Its field-generation invariant is established separately.

theorem Hex.AlgebraicPoly.Common.extendShift?_source (theta alpha : AlgebraicNumber) (shifted : ShiftCandidate) (h : extendShift? theta alpha = some shifted) : shift? theta alpha shifted.shift = some shifted.value

The retained shift exactly produces the selected primitive candidate.

theorem Hex.AlgebraicPoly.Common.primitive?_isSome (coefficients : Array AlgebraicNumber) (hnonzero : ∃ a ∈ coefficients.toList, a.isZero = false) : (primitive? coefficients).isSome = true

The primitive-element fold is total for any coefficient array containing a semantically nonzero entry.

theorem Hex.AlgebraicPoly.Common.powers?_isSome (gamma : AlgebraicNumber) (last : ℕ) : (powers? gamma last).isSome = true

The checked power table construction is total.

theorem Hex.AlgebraicPoly.Common.powers?_sound (gamma : AlgebraicNumber) (last : ℕ) {powers : Array AlgebraicNumber} (h : powers? gamma last = some powers) : powers.size = last + 1 ∧ ∀ (i : ℕ) (hi : i < powers.size), powers[i].toComplex = gamma.toComplex ^ i

A successful checked power table contains exactly the requested initial powers of its generator.