hex

6.2. The representation🔗

🔗structure
Hex.SparsePoly.{u} (R : Type u) [Zero R] [DecidableEq R] : Type u
Hex.SparsePoly.{u} (R : Type u) [Zero R]
  [DecidableEq R] : Type u

A univariate polynomial over R as a canonical sorted array of (exponent, coefficient) terms, ascending in exponent. Exponents are Nat, so degrees like 10^6 cost nothing to store; only toDense materialises a coefficient vector.

Per design principle 10, consumers read terms through the API (coeff, support, numTerms, degree?, leadingCoeff, and the ordered toTerms and foldTerms), not directly, so the representation can change.

Constructor

Hex.SparsePoly.mk.{u}

Fields

terms : Array (ℕ × R)

The stored (exponent, coefficient) terms in strictly increasing exponent order, with no zero coefficients.

canonical : Hex.SparsePolyCanonical self.terms

Proof that terms is canonical.

🔗def
Hex.SparsePolyCanonical.{u} {R : Type u} [Zero R]
  (terms : Array (ℕ × R)) : Prop
Hex.SparsePolyCanonical.{u} {R : Type u}
  [Zero R] (terms : Array (ℕ × R)) : Prop

A term array is canonical when its exponents are strictly increasing and no stored coefficient is zero.

Coefficient access is the semantic anchor: every equality of sparse polynomials reduces to coefficient extensionality, and the canonical invariant makes the stored exponents exactly the nonzero positions.

🔗def
Hex.SparsePoly.coeff.{u} {R : Type u} [Zero R] [DecidableEq R]
  (s : Hex.SparsePoly R) (e : ℕ) : R
Hex.SparsePoly.coeff.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (s : Hex.SparsePoly R) (e : ℕ) : R

The coefficient at e. Kernel-facing specification (an ordered List lookup); compiled code uses Hex.SparsePoly.coeffImpl, the value-equal binary search selected by Hex.SparsePoly.coeff_eq_impl.

🔗theorem
Hex.SparsePoly.mem_support_iff.{u} {R : Type u} [Zero R] [DecidableEq R]
  (s : Hex.SparsePoly R) (e : ℕ) : e ∈ s.support.toList ↔ s.coeff e ≠ 0
Hex.SparsePoly.mem_support_iff.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  (s : Hex.SparsePoly R) (e : ℕ) :
  e ∈ s.support.toList ↔ s.coeff e ≠ 0

The stored exponents are exactly the exponents with a nonzero coefficient. Uses both canonical-form invariants: strict increase makes the stored coefficient the coefficient, and zero-freedom makes it nonzero.

Construction goes through Hex.SparsePoly.ofTerms, which accepts arbitrary unsorted term arrays, combines duplicates in input order, and drops cancellations; its compiled implementation is a stable sort-and-combine selected by @[csimp].

🔗def
Hex.SparsePoly.ofTerms.{u} {R : Type u} [Zero R] [DecidableEq R] [Add R]
  (ts : Array (ℕ × R)) : Hex.SparsePoly R
Hex.SparsePoly.ofTerms.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R]
  (ts : Array (ℕ × R)) : Hex.SparsePoly R

The canonical polynomial with the given terms. Exponents may repeat and may appear in any order, and coefficients at equal exponents are summed and zero results are dropped.

Kernel-facing specification (a fold of addTerm); compiled code uses Hex.SparsePoly.ofTermsImpl, the value-equal stable sort and combining pass selected by Hex.SparsePoly.ofTerms_eq_impl.

🔗def
Hex.SparsePoly.addTerm.{u} {R : Type u} [Zero R] [DecidableEq R] [Add R]
  (s : Hex.SparsePoly R) (e : ℕ) (c : R) : Hex.SparsePoly R
Hex.SparsePoly.addTerm.{u} {R : Type u}
  [Zero R] [DecidableEq R] [Add R]
  (s : Hex.SparsePoly R) (e : ℕ) (c : R) :
  Hex.SparsePoly R

Add c · x^e to s, combining with an existing term at e and deleting the term when the sum is zero.

Kernel-facing specification (a single ordered List insert); compiled code uses Hex.SparsePoly.addTermImpl, the value-equal binary search and in-place array update selected by Hex.SparsePoly.addTerm_eq_impl.

🔗def
Hex.SparsePoly.monomial.{u} {R : Type u} [Zero R] [DecidableEq R]
  (e : ℕ) (c : R) : Hex.SparsePoly R
Hex.SparsePoly.monomial.{u} {R : Type u}
  [Zero R] [DecidableEq R] (e : ℕ)
  (c : R) : Hex.SparsePoly R

The monomial c · x^e. The zero coefficient collapses to the zero polynomial.