def Hex.DensePolyNormalized {R : Type u} [Zero R] [DecidableEq R] (coeffs : Array R) : Prop

DensePolyNormalized coeffs means either coeffs is empty or its last coefficient is nonzero, so the array has no trailing zeros.

Equations

• Hex.DensePolyNormalized coeffs = (coeffs.size = 0 ∨ coeffs.back? ≠ some Zero.zero)

structure Hex.DensePoly (R : Type u) [Zero R] [DecidableEq R] : Type u

Dense polynomials store coefficients in ascending degree order, with index i holding the coefficient of x^i.

The packed native polynomial kernels rely on proof erasure leaving coeffs as the sole runtime constructor field. Any new data-bearing field requires a matching FFI update and native cross-check.

• coeffs : Array R

  The stored coefficients in ascending degree order.

• normalized : DensePolyNormalized self.coeffs

  Proof that coeffs carries no trailing zeros.

@[instance_reducible]

instance Hex.DensePoly.instDecidableEq {R : Type u} [Zero R] [DecidableEq R] : DecidableEq (DensePoly R)

Equations

• a.instDecidableEq b = match decEq a.coeffs.toList b.coeffs.toList with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

def Hex.DensePoly.trimTrailingZerosList {R : Type u} [Zero R] [DecidableEq R] : List R → List R

Remove trailing zeros from a coefficient list without disturbing the remaining order.

Equations

• Hex.DensePoly.trimTrailingZerosList [] = []
• Hex.DensePoly.trimTrailingZerosList (a :: as) = if Hex.DensePoly.trimTrailingZerosList as = [] ∧ a = Zero.zero then [] else a :: Hex.DensePoly.trimTrailingZerosList as

theorem Hex.DensePoly.trimTrailingZerosList_getD {R : Type u} [Zero R] [DecidableEq R] (coeffs : List R) (n : Nat) : (trimTrailingZerosList coeffs).getD n Zero.zero = coeffs.getD n Zero.zero

Trimming preserves the value at every index, including indices beyond the trimmed length where both sides default to 0.

theorem Hex.DensePoly.trimTrailingZerosList_length_le {R : Type u} [Zero R] [DecidableEq R] (coeffs : List R) : (trimTrailingZerosList coeffs).length ≤ coeffs.length

Trimming trailing zeros never increases the coefficient-list length.

theorem Hex.DensePoly.trimTrailingZerosList_normalized {R : Type u} [Zero R] [DecidableEq R] (coeffs : List R) : trimTrailingZerosList coeffs = [] ∨ (trimTrailingZerosList coeffs).getLast? ≠ some Zero.zero

Trimming leaves the list either empty or with a nonzero last entry; this is the list-level form of the DensePolyNormalized invariant.

noncomputable def Hex.DensePoly.trimTrailingZeros {R : Type u} [Zero R] [DecidableEq R] (coeffs : Array R) : Array R

Normalize a coefficient array by discarding all trailing zeros. The compiled runtime uses the value-equal in-place implementation below, registered through @[csimp], which pops trailing zeros off the array instead of round-tripping through coeffs.toList.

Equations

• Hex.DensePoly.trimTrailingZeros coeffs = (Hex.DensePoly.trimTrailingZerosList coeffs.toList).toArray

def Hex.DensePoly.trimTrailingZerosGo {R : Type u} [Zero R] [DecidableEq R] (coeffs : Array R) : Nat → Array R

Runtime loop for trimTrailingZeros: pop trailing zeros off the array, up to n of them. With n = coeffs.size it pops the whole trailing-zero run, reusing the input storage in place when it is uniquely referenced rather than allocating a list.

Equations

• Hex.DensePoly.trimTrailingZerosGo coeffs 0 = coeffs
• Hex.DensePoly.trimTrailingZerosGo coeffs n.succ = if coeffs.back? = some Zero.zero then Hex.DensePoly.trimTrailingZerosGo coeffs.pop n else coeffs

def Hex.DensePoly.trimTrailingZerosImpl {R : Type u} [Zero R] [DecidableEq R] (coeffs : Array R) : Array R

Runtime implementation of trimTrailingZeros.

Equations

• Hex.DensePoly.trimTrailingZerosImpl coeffs = Hex.DensePoly.trimTrailingZerosGo coeffs coeffs.size

@[csimp]

theorem Hex.DensePoly.trimTrailingZeros_eq_impl : @trimTrailingZeros = @trimTrailingZerosImpl

Register the value-equal trimTrailingZerosImpl as the compiled implementation of trimTrailingZeros. Unlike @[implemented_by], the @[csimp] swap is backed by the proof trimTrailingZerosGo_eq, so the runtime loop is verified equal to the specification.

def Hex.DensePoly.ofCoeffs {R : Type u} [Zero R] [DecidableEq R] (coeffs : Array R) : DensePoly R

Build a dense polynomial from a raw coefficient array by normalizing away trailing zeros.

Equations

• Hex.DensePoly.ofCoeffs coeffs = { coeffs := Hex.DensePoly.trimTrailingZeros coeffs, normalized := ⋯ }

def Hex.DensePoly.densePolyLiteral : Lean.ParserDescr

#p[a₀, a₁, ...] constructs a dense polynomial whose coefficient of xⁱ is aᵢ. Trailing zero coefficients are removed by ofCoeffs.

Equations

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

def Hex.DensePoly.zero {R : Type u} [Zero R] [DecidableEq R] : DensePoly R

The zero polynomial.

Equations

• Hex.DensePoly.zero = Hex.DensePoly.ofCoeffs #[]

@[instance_reducible]

instance Hex.DensePoly.instZero {R : Type u} [Zero R] [DecidableEq R] : Zero (DensePoly R)

Equations

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

def Hex.DensePoly.ofList {R : Type u} [Zero R] [DecidableEq R] (coeffs : List R) : DensePoly R

Build a dense polynomial from a coefficient list by normalizing away trailing zeros.

Equations

• Hex.DensePoly.ofList coeffs = Hex.DensePoly.ofCoeffs coeffs.toArray

def Hex.DensePoly.C {R : Type u} [Zero R] [DecidableEq R] (c : R) : DensePoly R

Build the constant polynomial with value c. The zero constant collapses to the zero polynomial.

Equations

• Hex.DensePoly.C c = Hex.DensePoly.ofCoeffs #[c]

def Hex.DensePoly.monomial {R : Type u} [Zero R] [DecidableEq R] (n : Nat) (c : R) : DensePoly R

Build the monomial c * x^n. The zero coefficient collapses to the zero polynomial.

Equations

• Hex.DensePoly.monomial n c = if hc : c = Zero.zero then 0 else { coeffs := (Array.replicate n Zero.zero).push c, normalized := ⋯ }

def Hex.DensePoly.size {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : Nat

The number of stored coefficients. For a normalized polynomial this is one more than the degree, except for the zero polynomial where it is 0.

Equations

• p.size = p.coeffs.size

theorem Hex.DensePoly.size_ofCoeffs_le {R : Type u} [Zero R] [DecidableEq R] (coeffs : Array R) : (ofCoeffs coeffs).size ≤ coeffs.size

The normalized polynomial built from a raw coefficient array stores no more coefficients than the input array.

def Hex.DensePoly.isZero {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : Bool

true exactly when the polynomial is zero.

Equations

• p.isZero = p.coeffs.isEmpty

def Hex.DensePoly.coeff {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (n : Nat) : R

The coefficient of x^n, defaulting to 0 when n is out of range.

Equations

• p.coeff n = p.coeffs.getD n Zero.zero

@[simp]

theorem Hex.DensePoly.coeff_ofCoeffs {R : Type u} [Zero R] [DecidableEq R] (coeffs : Array R) (n : Nat) : (ofCoeffs coeffs).coeff n = coeffs.getD n Zero.zero

Coefficient of ofCoeffs arr agrees with arr.getD _ 0: trimming trailing zeros does not change the value at any index.

@[simp]

theorem Hex.DensePoly.coeff_C {R : Type u} [Zero R] [DecidableEq R] (c : R) (n : Nat) : (C c).coeff n = if n = 0 then c else Zero.zero

Characterising lemma for the constant polynomial: its coefficient is c at degree 0, zero elsewhere.

@[simp]

theorem Hex.DensePoly.coeff_monomial {R : Type u} [Zero R] [DecidableEq R] (n : Nat) (c : R) (i : Nat) : (monomial n c).coeff i = if i = n then c else Zero.zero

Characterising lemma for monomials: monomial n c has coefficient c at degree n and zero elsewhere, even when c = 0 (in which case the polynomial is zero and every coefficient is 0).

@[simp]

theorem Hex.DensePoly.coeff_ofList {R : Type u} [Zero R] [DecidableEq R] (coeffs : List R) (n : Nat) : (ofList coeffs).coeff n = coeffs.getD n Zero.zero

Coefficient of ofList coeffs agrees with coeffs.getD _ 0: normalization does not change the value at any index.

theorem Hex.DensePoly.size_ofList_le {R : Type u} [Zero R] [DecidableEq R] (coeffs : List R) : (ofList coeffs).size ≤ coeffs.length

The normalized polynomial built from a raw coefficient list stores no more coefficients than the input list.

theorem Hex.DensePoly.ext_of_size_eq {R : Type u} [Zero R] [DecidableEq R] {p q : DensePoly R} (hsize : p.size = q.size) (hcoeff : ∀ (i : Nat), i < p.size → p.coeff i = q.coeff i) : p = q

Extensionality for normalized dense polynomials when the stored sizes agree.

theorem Hex.DensePoly.coeff_eq_zero_of_size_le {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) {i : Nat} (h : p.size ≤ i) : p.coeff i = Zero.zero

Coefficients outside the stored support are zero.

theorem Hex.DensePoly.coeff_last_ne_zero_of_pos_size {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (hpos : 0 < p.size) : p.coeff (p.size - 1) ≠ Zero.zero

The last stored coefficient of a nonzero normalized dense polynomial is nonzero.

theorem Hex.DensePoly.size_eq_of_coeff_eq {R : Type u} [Zero R] [DecidableEq R] {p q : DensePoly R} (hcoeff : ∀ (i : Nat), p.coeff i = q.coeff i) : p.size = q.size

Coefficientwise equality of normalized dense polynomials forces equal stored sizes.

theorem Hex.DensePoly.ext_coeff {R : Type u} [Zero R] [DecidableEq R] {p q : DensePoly R} (hcoeff : ∀ (i : Nat), p.coeff i = q.coeff i) : p = q

Extensionality for normalized dense polynomials by their coefficient functions. This is the preferred form of extensionality: it asks only for coefficient agreement, since size agreement is forced by Hex.DensePoly.size_eq_of_coeff_eq.

theorem Hex.DensePoly.ext_coeff_iff {R : Type u} [Zero R] [DecidableEq R] {p q : DensePoly R} : p = q ↔ ∀ (i : Nat), p.coeff i = q.coeff i

def Hex.DensePoly.beqCoeffs {R : Type u} [Zero R] [DecidableEq R] (a b : DensePoly R) : Bool

Coefficient-level Boolean equality of two dense polynomials: equal stored sizes and equal coefficients at every stored index. Because DensePoly has no trailing zero coefficients, this decides polynomial equality. Its explicit Bool fold also reduces on literal data after an ordinary public import.

Equations

• a.beqCoeffs b = (a.size == b.size && (List.range a.size).all fun (i : Nat) => decide (a.coeff i = b.coeff i))

theorem Hex.DensePoly.eq_of_beqCoeffs {R : Type u} [Zero R] [DecidableEq R] {a b : DensePoly R} (h : a.beqCoeffs b = true) : a = b

beqCoeffs is sound: a true result forces genuine polynomial equality.

theorem Hex.DensePoly.beqCoeffs_iff_eq {R : Type u} [Zero R] [DecidableEq R] {a b : DensePoly R} : a.beqCoeffs b = true ↔ a = b

beqCoeffs decides equality: the checker returns true exactly on equal polynomials.

def Hex.DensePoly.degree? {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : Option Nat

The largest exponent with a stored coefficient, or none for the zero polynomial.

Equations

• p.degree? = if _h : p.size = 0 then none else some (p.size - 1)

@[simp]

theorem Hex.DensePoly.size_zero {R : Type u} [Zero R] [DecidableEq R] : size 0 = 0

The zero polynomial has no stored coefficients.

@[simp]

theorem Hex.DensePoly.size_eq_zero_iff {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : p.size = 0 ↔ p = 0

A normalized dense polynomial has no stored coefficients exactly when it is the zero polynomial.

@[simp]

theorem Hex.DensePoly.degree?_zero {R : Type u} [Zero R] [DecidableEq R] : degree? 0 = none

The zero polynomial has no degree.

@[simp]

theorem Hex.DensePoly.degree?_zero_getD {R : Type u} [Zero R] [DecidableEq R] (d : Nat) : (degree? 0).getD d = d

Defaulting the degree of the zero polynomial returns the supplied default.

theorem Hex.DensePoly.isZero_eq_true_iff {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : p.isZero = true ↔ p.size = 0

isZero is the Boolean test for having no stored coefficients.

theorem Hex.DensePoly.isZero_eq_false_iff {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : p.isZero = false ↔ 0 < p.size

A polynomial is nonzero exactly when it stores at least one coefficient.

@[simp]

theorem Hex.DensePoly.coeffs_C_zero {R : Type u} [Zero R] [DecidableEq R] : (C 0).coeffs = #[]

The constant polynomial C 0 collapses to the zero polynomial, so its coefficient array is empty.

theorem Hex.DensePoly.coeffs_C_of_ne_zero {R : Type u} [Zero R] [DecidableEq R] {c : R} (hc : c ≠ 0) : (C c).coeffs = #[c]

A constant polynomial with a nonzero scalar stores a single-element coefficient array; this is the companion to coeffs_C_zero for the nonzero case.

theorem Hex.DensePoly.size_C_le_one {R : Type u} [Zero R] [DecidableEq R] (c : R) : (C c).size ≤ 1

A constant polynomial has size at most one, with size 0 when the scalar is zero and 1 otherwise.

@[simp]

theorem Hex.DensePoly.size_C_zero {R : Type u} [Zero R] [DecidableEq R] : (C 0).size = 0

The zero constant polynomial stores no coefficients.

theorem Hex.DensePoly.size_C_of_ne_zero {R : Type u} [Zero R] [DecidableEq R] {c : R} (hc : c ≠ 0) : (C c).size = 1

A nonzero constant polynomial stores exactly its scalar coefficient.

theorem Hex.DensePoly.isZero_C_eq_true_iff {R : Type u} [Zero R] [DecidableEq R] (c : R) : (C c).isZero = true ↔ c = 0

A constant polynomial is zero exactly when its scalar is zero.

@[simp]

theorem Hex.DensePoly.monomial_zero {R : Type u} [Zero R] [DecidableEq R] (n : Nat) : monomial n 0 = 0

The monomial with zero coefficient is the zero polynomial.

theorem Hex.DensePoly.size_monomial_of_ne_zero {R : Type u} [Zero R] [DecidableEq R] {n : Nat} {c : R} (hc : c ≠ 0) : (monomial n c).size = n + 1

A monomial with nonzero coefficient stores exactly the n + 1 coefficients up to degree n.

theorem Hex.DensePoly.isZero_monomial_eq_true_iff {R : Type u} [Zero R] [DecidableEq R] (n : Nat) (c : R) : (monomial n c).isZero = true ↔ c = 0

A monomial is zero exactly when its coefficient is zero.

theorem Hex.DensePoly.isZero_monomial_eq_false_of_ne_zero {R : Type u} [Zero R] [DecidableEq R] {n : Nat} {c : R} (hc : c ≠ 0) : (monomial n c).isZero = false

A monomial with nonzero coefficient is not the zero polynomial.

@[simp]

theorem Hex.DensePoly.degree?_C_getD {R : Type u} [Zero R] [DecidableEq R] (c : R) : (C c).degree?.getD 0 = 0

The degree? of a constant polynomial, defaulted to 0, is 0 regardless of the scalar: either degree? = none (when c = 0) and getD 0 = 0, or degree? = some 0 (otherwise).

theorem Hex.DensePoly.degree?_eq_none_iff {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : p.degree? = none ↔ p.size = 0

The zero polynomial is the only dense polynomial with no degree.

theorem Hex.DensePoly.degree?_eq_some_of_pos_size {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (hpos : 0 < p.size) : p.degree? = some (p.size - 1)

A nonzero dense polynomial has degree one less than its stored coefficient count.

theorem Hex.DensePoly.degree?_monomial_of_ne_zero {R : Type u} [Zero R] [DecidableEq R] {n : Nat} {c : R} (hc : c ≠ 0) : (monomial n c).degree? = some n

A monomial with nonzero coefficient has degree exactly its exponent.

theorem Hex.DensePoly.degree?_monomial_getD_of_ne_zero {R : Type u} [Zero R] [DecidableEq R] {n : Nat} {c : R} (hc : c ≠ 0) : (monomial n c).degree?.getD 0 = n

The default-0 degree of a monomial with nonzero coefficient is its exponent.

theorem Hex.DensePoly.monomial_ne_zero_of_ne_zero {R : Type u} [Zero R] [DecidableEq R] {n : Nat} {c : R} (hc : c ≠ 0) : monomial n c ≠ 0

A monomial with nonzero coefficient is not the zero polynomial.

def Hex.DensePoly.support {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : List Nat

The support of a dense polynomial, listed in ascending degree order.

Equations

• p.support = List.filter (fun (i : Nat) => decide (p.coeff i ≠ Zero.zero)) (List.range p.size)

@[simp]

theorem Hex.DensePoly.mem_support {R : Type u} [Zero R] [DecidableEq R] {p : DensePoly R} {i : Nat} : i ∈ p.support ↔ i < p.size ∧ p.coeff i ≠ Zero.zero

Membership in support is coefficient nonzeroness inside the stored range.

@[simp]

theorem Hex.DensePoly.support_zero {R : Type u} [Zero R] [DecidableEq R] : support 0 = []

The zero polynomial has empty support.

@[simp]

theorem Hex.DensePoly.support_C {R : Type u} [Zero R] [DecidableEq R] (c : R) : (C c).support = if c = 0 then [] else [0]

A constant polynomial has support {0} exactly when its scalar is nonzero.

theorem Hex.DensePoly.mem_support_C {R : Type u} [Zero R] [DecidableEq R] {c : R} {i : Nat} : i ∈ (C c).support ↔ i = 0 ∧ c ≠ 0

Membership in the support of a constant polynomial is exactly nonzero degree zero.

@[simp]

theorem Hex.DensePoly.support_monomial {R : Type u} [Zero R] [DecidableEq R] (n : Nat) (c : R) : (monomial n c).support = if c = 0 then [] else [n]

A monomial has support {n} exactly when its coefficient is nonzero.

theorem Hex.DensePoly.mem_support_monomial {R : Type u} [Zero R] [DecidableEq R] {n : Nat} {c : R} {i : Nat} : i ∈ (monomial n c).support ↔ i = n ∧ c ≠ 0

Membership in the support of a monomial is exactly its nonzero exponent.

def Hex.DensePoly.toArray {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : Array R

Return the underlying normalized coefficient array.

Equations

• p.toArray = p.coeffs

@[simp]

theorem Hex.DensePoly.toArray_size {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : p.toArray.size = p.size

The exposed normalized coefficient array has the same size as the polynomial.

@[simp]

theorem Hex.DensePoly.toArray_getD {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (n : Nat) : p.toArray.getD n Zero.zero = p.coeff n

Reading the exposed normalized coefficient array with default 0 is the polynomial coefficient function.

noncomputable def Hex.DensePoly.toList {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : List R

View of the stored coefficients as a list, lowest degree first. noncomputable by design: kernel-facing specifications, theorem statements, and proofs read coefficients through this list view, while runtime code stays on the Array API. A deliberate runtime list round-trip spells out toArray.toList explicitly.

Equations

• p.toList = p.toArray.toList

@[simp]

theorem Hex.DensePoly.length_toList {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : p.toList.length = p.size

The coefficient list has one entry per stored coefficient.

@[simp]

theorem Hex.DensePoly.ofCoeffs_toArray {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : ofCoeffs p.toArray = p

Normalizing the already-normalized coefficient array reconstructs the same polynomial.

@[simp]

theorem Hex.DensePoly.ofList_toList {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : ofList p.toList = p

Building from the reference coefficient list reconstructs the same polynomial.

@[simp]

theorem Hex.DensePoly.ofCoeffs_empty {R : Type u} [Zero R] [DecidableEq R] : ofCoeffs #[] = 0

Normalizing an empty coefficient array gives the zero polynomial.

@[simp]

theorem Hex.DensePoly.ofList_nil {R : Type u} [Zero R] [DecidableEq R] : ofList [] = 0

Normalizing an empty coefficient list gives the zero polynomial.

@[simp]

theorem Hex.DensePoly.ofCoeffs_replicate_zero {R : Type u} [Zero R] [DecidableEq R] (n : Nat) : ofCoeffs (Array.replicate n Zero.zero) = 0

An array consisting only of zeros normalizes to the zero polynomial.