@[reducible, inline]

abbrev Hex.ZPoly : Type

Integer polynomials represented by the dense normalized coefficient type from HexPoly.

Equations

• Hex.ZPoly = Hex.DensePoly Int

instance Hex.instAssociativeZPolyHMul : Std.Associative fun (x1 x2 : ZPoly) => x1 * x2

ZPoly is a multiplicative monoid for Std, so the shared List.foldl_mul_* algebra and the standard List.foldl_assoc apply to fold-products of integer polynomials.

instance Hex.instLawfulIdentityZPolyHMulOfNat : Std.LawfulIdentity (fun (x1 x2 : ZPoly) => x1 * x2) 1

instance Hex.instAddZeroLawInt_hexPolyZ : DensePoly.AddZeroLaw Int

instance Hex.instSubZeroLawInt_hexPolyZ : DensePoly.SubZeroLaw Int

instance Hex.instZeroSubNegLawInt_hexPolyZ : DensePoly.ZeroSubNegLaw Int

instance Hex.instAddZeroLawRat_hexPolyZ : DensePoly.AddZeroLaw Rat

instance Hex.instSubZeroLawRat_hexPolyZ : DensePoly.SubZeroLaw Rat

instance Hex.instZeroSubNegLawRat_hexPolyZ : DensePoly.ZeroSubNegLaw Rat

def Hex.ZPoly.congr (f g : ZPoly) (m : Nat) : Prop

Coefficientwise congruence modulo m.

Equations

• f.congr g m = ∀ (i : Nat), (Hex.DensePoly.coeff f i - Hex.DensePoly.coeff g i) % ↑m = 0

def Hex.ZPoly.coprimeModP (f g : ZPoly) (p : Nat) : Prop

Two integer polynomials are coprime mod p when they admit a Bezout combination congruent to 1 modulo p.

Equations

• f.coprimeModP g p = ∃ (s : Hex.ZPoly), ∃ (t : Hex.ZPoly), (s * f + t * g).congr 1 p

def Hex.ZPoly.content (f : ZPoly) : Int

The nonnegative gcd of the coefficients of f.

Equations

• f.content = Hex.DensePoly.content f

def Hex.ZPoly.primitivePart (f : ZPoly) : ZPoly

Divide every coefficient by the content to obtain a primitive polynomial.

Equations

• f.primitivePart = Hex.DensePoly.primitivePart f

def Hex.ZPoly.dilate (c : Int) (p : ZPoly) : ZPoly

Substitute the variable X ↦ c * X: the i-th coefficient is multiplied by c ^ i.

On a monic transform c^(d-1) · core(X / c), this is the inverse of the integer-scaling substitution: it maps a monic factor g of the transform to g(c · X), an integer multiple of the corresponding factor of core. Composing with Hex.ZPoly.primitivePart recovers the primitive integer factor of core. This is not the same as Hex.DensePoly.scale, which multiplies the whole polynomial by a constant.

Equations

• Hex.ZPoly.dilate c p = Hex.DensePoly.ofList (List.map (fun (i : Nat) => c ^ i * Hex.DensePoly.coeff p i) (List.range (Hex.DensePoly.size p)))

theorem Hex.ZPoly.coeff_dilate (c : Int) (p : ZPoly) (n : Nat) : DensePoly.coeff (dilate c p) n = c ^ n * DensePoly.coeff p n

The n-th coefficient of dilate c p is c ^ n times the n-th coefficient of p.

theorem Hex.ZPoly.size_dilate_neg_one (p : ZPoly) : DensePoly.size (dilate (-1) p) = DensePoly.size p

Reflection in the origin preserves the stored coefficient count.

@[simp]

theorem Hex.ZPoly.dilate_neg_one_dilate_neg_one (p : ZPoly) : dilate (-1) (dilate (-1) p) = p

Reflection in the origin is an involution on integer polynomials.

theorem Hex.ZPoly.dilate_neg_one_ne_zero {p : ZPoly} (hp : p ≠ 0) : dilate (-1) p ≠ 0

Reflection in the origin preserves nonzeroness.

@[simp]

theorem Hex.ZPoly.content_dilate_neg_one (p : ZPoly) : (dilate (-1) p).content = p.content

Reflection in the origin preserves integer content.

@[simp]

theorem Hex.ZPoly.degree?_dilate_neg_one (p : ZPoly) : DensePoly.degree? (dilate (-1) p) = DensePoly.degree? p

Reflection in the origin preserves the optional degree.

theorem Hex.ZPoly.leadingCoeff_dilate_neg_one (p : ZPoly) : DensePoly.leadingCoeff (dilate (-1) p) = (-1) ^ (DensePoly.size p - 1) * DensePoly.leadingCoeff p

The reflected leading coefficient differs only by the degree-parity sign.

@[simp]

theorem Hex.ZPoly.dilate_one (p : ZPoly) : dilate 1 p = p

Dilation by 1 is the identity: dilate 1 p = p. The simp normal form for the trivial dilation.

def Hex.ZPoly.Primitive (f : ZPoly) : Prop

A Hex.ZPoly is primitive when its content is 1.

Equations

• f.Primitive = (f.content = 1)

theorem Hex.ZPoly.primitive_dilate_neg_one {p : ZPoly} (hp : p.Primitive) : (dilate (-1) p).Primitive

Reflection in the origin preserves primitivity.

def Hex.ZPoly.IsUnit (f : ZPoly) : Prop

A Hex.ZPoly is a unit iff it is the constant polynomial 1 or -1.

Equations

• f.IsUnit = (f = Hex.DensePoly.C 1 ∨ f = Hex.DensePoly.C (-1))

@[instance_reducible]

instance Hex.ZPoly.instDecidableIsUnit (f : ZPoly) : Decidable f.IsUnit

Hex.ZPoly.IsUnit is decidable: it reduces to equality with the constant polynomials C 1 or C (-1), both of which are decidable.

Equations

• f.instDecidableIsUnit = id inferInstance

theorem Hex.ZPoly.isUnit_iff (f : ZPoly) : f.IsUnit ↔ f = DensePoly.C 1 ∨ f = DensePoly.C (-1)

The Hex.ZPoly.IsUnit predicate is exactly equality with the constant polynomial 1 or the constant polynomial -1.

@[simp]

theorem Hex.ZPoly.isUnit_one : IsUnit 1

The polynomial 1 is a unit, since (1 : ZPoly) is the constant polynomial C 1.

@[simp]

theorem Hex.ZPoly.isUnit_C_one : IsUnit (DensePoly.C 1)

The constant polynomial C 1 is a unit.

@[simp]

theorem Hex.ZPoly.isUnit_C_neg_one : IsUnit (DensePoly.C (-1))

The constant polynomial C (-1) is a unit.

theorem Hex.ZPoly.isUnit_of_eq_one {f : ZPoly} (h : f = 1) : f.IsUnit

Equality to 1 is the common constructor form for IsUnit.

theorem Hex.ZPoly.isUnit_of_eq_neg_one {f : ZPoly} (h : f = -1) : f.IsUnit

Equality to -1 is the common constructor form for IsUnit.

@[simp]

theorem Hex.ZPoly.isUnit_neg_one : (-1).IsUnit

The polynomial -1 is a unit.

def Hex.ZPoly.toRatPoly (f : ZPoly) : DensePoly Rat

View an integer polynomial as a rational polynomial.

Equations

• f.toRatPoly = Hex.DensePoly.ofCoeffs (Array.map (fun (coeff : Int) => ↑coeff) (Hex.DensePoly.toArray f))

@[simp]

theorem Hex.ZPoly.coeff_toRatPoly (f : ZPoly) (n : Nat) : f.toRatPoly.coeff n = ↑(DensePoly.coeff f n)

Coefficients of toRatPoly f are the rational casts of the coefficients of f.

@[simp]

theorem Hex.ZPoly.toRatPoly_zero : toRatPoly 0 = 0

Rational conversion sends the zero integer polynomial to the zero rational polynomial. The simp normal form for the zero case.

@[simp]

theorem Hex.ZPoly.toRatPoly_C (c : Int) : toRatPoly (DensePoly.C c) = DensePoly.C ↑c

Rational conversion sends the constant integer polynomial C c to the constant rational polynomial C (c : Rat). The simp normal form for the constant case.

@[simp]

theorem Hex.ZPoly.toRatPoly_one : toRatPoly 1 = 1

Rational conversion sends the unit integer polynomial 1 to the rational polynomial 1, since (1 : ZPoly) is the constant polynomial C 1. The simp normal form for the one case.

theorem Hex.ZPoly.toRatPoly_scale_int (c : Int) (f : ZPoly) : toRatPoly (DensePoly.scale c f) = DensePoly.scale (↑c) f.toRatPoly

Rational conversion commutes with scaling an integer polynomial by an integer.

theorem Hex.ZPoly.size_toRatPoly (f : ZPoly) : f.toRatPoly.size = DensePoly.size f

Rational conversion preserves the dense size of an integer polynomial.

theorem Hex.ZPoly.toRatPoly_ne_zero_of_ne_zero (f : ZPoly) (hf : f ≠ 0) : f.toRatPoly ≠ 0

A nonzero integer polynomial remains nonzero after coefficientwise rational casting.

theorem Hex.ZPoly.toRatPoly_mul (f g : ZPoly) : (f * g).toRatPoly = f.toRatPoly * g.toRatPoly

Rational conversion preserves multiplication of integer polynomials.

def Hex.ZPoly.normalizePrimitiveSign (f : ZPoly) : ZPoly

Negate f when its leading coefficient is negative, normalizing a primitive part to have nonnegative leading sign.

Equations

• f.normalizePrimitiveSign = if Hex.DensePoly.leadingCoeff f < 0 then Hex.DensePoly.scale (-1) f else f

def Hex.ZPoly.ratPolyPrimitivePart (f : DensePoly Rat) : ZPoly

Clear denominators in a rational polynomial and return the primitive integer representative of the resulting rational associate.

Equations

• Hex.ZPoly.ratPolyPrimitivePart f = (Hex.ZPoly.ratPolyPrimitivePartCleared✝ f).primitivePart.normalizePrimitiveSign

theorem Hex.ZPoly.ratPolyPrimitivePart_rational_associate (f : DensePoly Rat) : ∃ (unit : Rat), f = DensePoly.scale unit (ratPolyPrimitivePart f).toRatPoly

A rational polynomial is a rational scalar multiple of the rationalization of its integer primitive part.

structure Hex.ZPoly.PrimitiveSquareFreeDecomposition : Type

Executable primitive square-free decomposition data for integer-polynomial normalization.

primitive is the content-free input. squareFreeCore is computed over Rat[x] as primitive / gcd(primitive, primitive'), then converted back to a primitive integer representative. repeatedPart records the same rational gcd, also converted to a primitive integer representative. The proof layer relates these representatives back to the primitive input up to a rational unit.

• primitive : ZPoly

  The input divided by its content and normalized to positive leading coefficient.

• squareFreeCore : ZPoly

  A primitive representative of the product of the distinct irreducible factors.

• repeatedPart : ZPoly

  A primitive representative of the gcd of the primitive polynomial and its derivative.

def Hex.ZPoly.SquareFreeRat (f : ZPoly) : Prop

Square-free over Rat[x], up to the executable rational gcd's unit factor.

Equations

• f.SquareFreeRat = ((f.toRatPoly.gcd f.toRatPoly.derivative).size ≤ 1)

@[instance_reducible]

instance Hex.ZPoly.instDecidableSquareFreeRat (f : ZPoly) : Decidable f.SquareFreeRat

SquareFreeRat is by definition a Nat size inequality on the executable rational gcd, so Nat.decLe decides it. Drivers branch on this instance for their square-freeness precondition.

Equations

• f.instDecidableSquareFreeRat = Hex.ZPoly.instDecidableSquareFreeRat._aux_1 f

def Hex.ZPoly.primitiveSquareFreeDecomposition (f : ZPoly) : PrimitiveSquareFreeDecomposition

Compute the primitive square-free normalization data needed by the integer factorization computation.

Equations

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

def Hex.ZPoly.squareFreeCore (f : ZPoly) : ZPoly

The square-free part projection of primitiveSquareFreeDecomposition.

Equations

• f.squareFreeCore = f.primitiveSquareFreeDecomposition.squareFreeCore

theorem Hex.ZPoly.congr_refl (f : ZPoly) (m : Nat) : f.congr f m

Coefficientwise congruence modulo m is reflexive.

theorem Hex.ZPoly.congr_symm (f g : ZPoly) (m : Nat) (hfg : f.congr g m) : g.congr f m

Coefficientwise congruence modulo m is symmetric.

theorem Hex.ZPoly.congr_trans (f g h : ZPoly) (m : Nat) (hfg : f.congr g m) (hgh : g.congr h m) : f.congr h m

Coefficientwise congruence modulo m is transitive.

theorem Hex.ZPoly.congr_add (f g f' g' : ZPoly) (m : Nat) (hf : f.congr f' m) (hg : g.congr g' m) : (f + g).congr (f' + g') m

Addition preserves coefficientwise congruence modulo m in both inputs.

theorem Hex.ZPoly.congr_mul (f g f' g' : ZPoly) (m : Nat) (hf : f.congr f' m) (hg : g.congr g' m) : (f * g).congr (f' * g') m

Multiplication preserves coefficientwise congruence modulo m in both inputs.

theorem Hex.ZPoly.content_mul_primitivePart (f : ZPoly) : DensePoly.scale f.content f.primitivePart = f

Scaling the primitive part by the content reconstructs the original integer polynomial.

theorem Hex.ZPoly.content_dvd_coeff (f : ZPoly) (n : Nat) : f.content ∣ DensePoly.coeff f n

The content of an integer polynomial divides every coefficient.

theorem Hex.ZPoly.dvd_content_of_nat_dvd_coeff (f : ZPoly) (d : Nat) (h : ∀ (n : Nat), ↑d ∣ DensePoly.coeff f n) : ↑d ∣ f.content

If a natural number divides every coefficient, then its integer cast divides the content.

theorem Hex.ZPoly.natCast_dvd_content_of_dvd_coeff (f : ZPoly) (d : Nat) (h : ∀ (n : Nat), ↑d ∣ DensePoly.coeff f n) : ↑d ∣ f.content

Alias for dvd_content_of_nat_dvd_coeff with the divisibility conclusion written for the natural number cast to Int.

theorem Hex.ZPoly.primitivePart_primitive (f : ZPoly) (h : f.content ≠ 0) : f.primitivePart.Primitive

If the content of f is nonzero, then the primitive part of f is primitive.

theorem Hex.ZPoly.primitivePart_eq_self_of_primitive (f : ZPoly) (h : f.Primitive) : f.primitivePart = f

A primitive integer polynomial is equal to its primitive part.

theorem Hex.ZPoly.primitive_mul (p q : ZPoly) (hp : p.Primitive) (hq : q.Primitive) : (p * q).Primitive

The product of primitive integer polynomials is primitive.

theorem Hex.ZPoly.content_mul (p q : ZPoly) : (p * q).content = p.content * q.content

Hex.ZPoly-level wrapper for Hex.DensePoly.content_mul: the content of a product of integer polynomials is the product of their contents.

theorem Hex.ZPoly.primitivePart_mul (p q : ZPoly) : (p * q).primitivePart = p.primitivePart * q.primitivePart

Hex.ZPoly-level wrapper for Hex.DensePoly.primitivePart_mul (Gauss's lemma): the primitive part of a product of integer polynomials is the product of their primitive parts.

theorem Hex.ZPoly.coeff_mul_top (p q : ZPoly) (hp : 0 < DensePoly.size p) (hq : 0 < DensePoly.size q) : DensePoly.coeff (p * q) (DensePoly.size p - 1 + (DensePoly.size q - 1)) = DensePoly.coeff p (DensePoly.size p - 1) * DensePoly.coeff q (DensePoly.size q - 1)

The top coefficient of a product of nonzero integer polynomials is the product of their top coefficients.

theorem Hex.ZPoly.mul_size_eq_top_succ_of_nonzero (p q : ZPoly) (hp : 0 < DensePoly.size p) (hq : 0 < DensePoly.size q) : DensePoly.size (p * q) = DensePoly.size p + DensePoly.size q - 1

The size of a product of nonzero integer polynomials is one less than the sum of their sizes.

theorem Hex.ZPoly.size_pos_of_ne_zero (p : ZPoly) (hp : p ≠ 0) : 0 < DensePoly.size p

A nonzero integer polynomial has positive dense size.

theorem Hex.ZPoly.leadingCoeff_mul_of_nonzero (p q : ZPoly) (hp : p ≠ 0) (hq : q ≠ 0) : DensePoly.leadingCoeff (p * q) = DensePoly.leadingCoeff p * DensePoly.leadingCoeff q

The leading coefficient of a product of nonzero integer polynomials is the product of their leading coefficients.

theorem Hex.ZPoly.leadingCoeff_mul_pos_of_pos (p q : ZPoly) (hp_pos : 0 < DensePoly.leadingCoeff p) (hq_pos : 0 < DensePoly.leadingCoeff q) : 0 < DensePoly.leadingCoeff (p * q)

A product of integer polynomials with positive leading coefficients has positive leading coefficient.

theorem Hex.ZPoly.C_mul_eq_scale (c : Int) (p : ZPoly) : DensePoly.C c * p = DensePoly.scale c p

Multiplication by an integer constant agrees with coefficient scaling.

theorem Hex.ZPoly.scale_size_of_ne_zero (c : Int) (p : ZPoly) (hc : c ≠ 0) : (DensePoly.scale c p).size = DensePoly.size p

Nonzero integer scalar multiplication preserves the stored size.

theorem Hex.ZPoly.leadingCoeff_scale_of_nonzero (c : Int) (p : ZPoly) (hc : c ≠ 0) : (DensePoly.scale c p).leadingCoeff = c * DensePoly.leadingCoeff p

Leading coefficient after nonzero integer scalar multiplication.

theorem Hex.ZPoly.leadingCoeff_shift_of_nonzero (k : Nat) (p : ZPoly) (hp : p ≠ 0) : (DensePoly.shift k p).leadingCoeff = DensePoly.leadingCoeff p

Shifting a nonzero polynomial by x^k preserves its leading coefficient.

theorem Hex.ZPoly.mul_ne_zero_of_ne_zero (p q : ZPoly) (hp : p ≠ 0) (hq : q ≠ 0) : p * q ≠ 0

Integer dense polynomials have no zero divisors.

theorem Hex.ZPoly.mul_right_cancel_of_ne_zero {p q r : ZPoly} (hr : r ≠ 0) (h : p * r = q * r) : p = q

Right cancellation for multiplication by a nonzero integer polynomial.

theorem Hex.ZPoly.size_le_of_dvd_nonzero {d r : ZPoly} (hd : d ≠ 0) (hr : r ≠ 0) : d ∣ r → DensePoly.size d ≤ DensePoly.size r

A nonzero divisor of a nonzero integer polynomial has no larger dense size.

theorem Hex.ZPoly.divMod_reconstruction_of_monic (target candidate : ZPoly) (hmonic : DensePoly.Monic candidate) : (DensePoly.divMod target candidate).fst * candidate + (DensePoly.divMod target candidate).snd = target

Euclidean reconstruction for a monic integer divisor: the executable dense-polynomial division recomposes the dividend, quot * candidate + rem = target, for any dividend. This is the monic specialization over Int of DensePoly.divMod_reconstruction; the leading-coefficient cancellation invariant it requires holds because a monic divisor has leading coefficient 1. Unlike divMod_eq_of_monic_mul_eq, no exact-multiple hypothesis is needed, so the remainder may be nonzero.

theorem Hex.ZPoly.divMod_remainder_eq_zero_of_monic_mul_eq (target candidate quotient : ZPoly) (hmonic : DensePoly.Monic candidate) (hdegree : 0 < DensePoly.natDegree candidate) (hmul : quotient * candidate = target) : (DensePoly.divMod target candidate).snd = 0

If a monic positive-degree integer divisor has an exact product witness, the executable dense-polynomial division returns zero remainder.

theorem Hex.ZPoly.divMod_eq_of_monic_mul_eq (target candidate quotient : ZPoly) (hmonic : DensePoly.Monic candidate) (hdegree : 0 < DensePoly.natDegree candidate) (hmul : quotient * candidate = target) : DensePoly.divMod target candidate = (quotient, 0)

If a monic positive-degree integer divisor has an exact product witness, the executable dense-polynomial division returns the witnessed quotient and zero remainder.

theorem Hex.ZPoly.divMod_eq_mul (target candidate quotient : ZPoly) (hpos_lc : 0 < DensePoly.leadingCoeff candidate) (hmul : quotient * candidate = target) : DensePoly.divMod target candidate = (quotient, 0)

Non-monic exact-multiple divMod identity: if the divisor candidate has positive leading coefficient and the dividend factors as quotient * candidate, the executable dense-polynomial division returns the witnessed quotient and zero remainder. Sits one level above divMod_eq_of_monic_mul_eq, dropping the monic requirement at the cost of needing 0 < candidate.leadingCoeff to discharge the integer-division exactness side-conditions.