@[reducible, inline]

abbrev Hex.MvPoly.Kernel.Term (κ : Type u) : Type u

A list-form term: an exponent list and a coefficient.

Equations

• Hex.MvPoly.Kernel.Term κ = (List Nat × κ)

@[reducible, inline]

abbrev Hex.MvPoly.Kernel.PolyList (κ : Type u) : Type u

A sparse polynomial represented by a canonical list of terms.

Equations

• Hex.MvPoly.Kernel.PolyList κ = List (Hex.MvPoly.Kernel.Term κ)

def Hex.MvPoly.Kernel.expBeqImpl : List Nat → List Nat → Bool

Equality of exponent lists, using only Nat.beq and structural recursion.

Equations

• Hex.MvPoly.Kernel.expBeqImpl [] [] = true
• Hex.MvPoly.Kernel.expBeqImpl (a :: as) (b :: bs) = (a.beq b && Hex.MvPoly.Kernel.expBeqImpl as bs)
• Hex.MvPoly.Kernel.expBeqImpl x✝¹ x✝ = false

noncomputable def Hex.MvPoly.Kernel.expBeq (a b : List Nat) : Bool

Kernel equality through a simple recursor; compiled calls use expBeqImpl.

Equations

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

def Hex.MvPoly.Kernel.expCmpImpl : List Nat → List Nat → Ordering

Lexicographic comparison of exponent lists, using only Nat.blt.

Equations

• Hex.MvPoly.Kernel.expCmpImpl [] [] = Ordering.eq
• Hex.MvPoly.Kernel.expCmpImpl [] (head :: tail) = Ordering.lt
• Hex.MvPoly.Kernel.expCmpImpl (head :: tail) [] = Ordering.gt
• Hex.MvPoly.Kernel.expCmpImpl (a :: as) (b :: bs) = if a.blt b = true then Ordering.lt else if b.blt a = true then Ordering.gt else Hex.MvPoly.Kernel.expCmpImpl as bs

noncomputable def Hex.MvPoly.Kernel.expCmp (a b : List Nat) : Ordering

Kernel comparison through a simple recursor; compiled calls use expCmpImpl.

Equations

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

def Hex.MvPoly.Kernel.addExpImpl : List Nat → List Nat → List Nat

Pointwise addition of exponent lists. Canonical inputs have equal length; the trailing clauses make the operation total on untrusted data.

Equations

• Hex.MvPoly.Kernel.addExpImpl [] x✝ = x✝
• Hex.MvPoly.Kernel.addExpImpl x✝ [] = x✝
• Hex.MvPoly.Kernel.addExpImpl (a :: as) (b :: bs) = a.add b :: Hex.MvPoly.Kernel.addExpImpl as bs

noncomputable def Hex.MvPoly.Kernel.addExp (a b : List Nat) : List Nat

Kernel exponent addition through a simple recursor; compiled calls use addExpImpl.

Equations

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

@[simp]

theorem Hex.MvPoly.Kernel.expBeq_nil (b : List Nat) : expBeq [] b = match b with | [] => true | head :: tail => false

@[simp]

theorem Hex.MvPoly.Kernel.expBeq_cons_nil (x : Nat) (xs : List Nat) : expBeq (x :: xs) [] = false

@[simp]

theorem Hex.MvPoly.Kernel.expBeq_cons_cons (x y : Nat) (xs ys : List Nat) : expBeq (x :: xs) (y :: ys) = (x.beq y && expBeq xs ys)

@[simp]

theorem Hex.MvPoly.Kernel.expCmp_nil (b : List Nat) : expCmp [] b = match b with | [] => Ordering.eq | head :: tail => Ordering.lt

@[simp]

theorem Hex.MvPoly.Kernel.expCmp_cons_nil (x : Nat) (xs : List Nat) : expCmp (x :: xs) [] = Ordering.gt

@[simp]

theorem Hex.MvPoly.Kernel.expCmp_cons_cons (x y : Nat) (xs ys : List Nat) : expCmp (x :: xs) (y :: ys) = if x.blt y = true then Ordering.lt else if y.blt x = true then Ordering.gt else expCmp xs ys

@[simp]

theorem Hex.MvPoly.Kernel.addExp_nil (b : List Nat) : addExp [] b = b

@[simp]

theorem Hex.MvPoly.Kernel.addExp_cons_nil (x : Nat) (xs : List Nat) : addExp (x :: xs) [] = x :: xs

@[simp]

theorem Hex.MvPoly.Kernel.addExp_cons_cons (x y : Nat) (xs ys : List Nat) : addExp (x :: xs) (y :: ys) = x.add y :: addExp xs ys

@[csimp]

theorem Hex.MvPoly.Kernel.expBeq_eq_impl : expBeq = expBeqImpl

@[csimp]

theorem Hex.MvPoly.Kernel.expCmp_eq_impl : expCmp = expCmpImpl

@[csimp]

theorem Hex.MvPoly.Kernel.addExp_eq_impl : addExp = addExpImpl

def Hex.MvPoly.Kernel.insert {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] (t : Term κ) : PolyList κ → PolyList κ

Insert one term into descending lexicographic order, adding coefficients on a collision and dropping a zero coefficient.

Equations

• One or more equations did not get rendered due to their size.
• Hex.MvPoly.Kernel.insert t [] = if t.snd = 0 then [] else [t]

def Hex.MvPoly.Kernel.normalize {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] : PolyList κ → PolyList κ

Canonicalize an arbitrary term stream by insertion.

Equations

• Hex.MvPoly.Kernel.normalize [] = []
• Hex.MvPoly.Kernel.normalize (u :: us) = Hex.MvPoly.Kernel.insert u (Hex.MvPoly.Kernel.normalize us)

def Hex.MvPoly.Kernel.insertSum {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] : PolyList κ → PolyList κ → PolyList κ

Insertion sum, also the total fallback for an undersupplied merge budget.

Equations

• Hex.MvPoly.Kernel.insertSum [] x✝ = x✝
• Hex.MvPoly.Kernel.insertSum (t :: ts) x✝ = Hex.MvPoly.Kernel.insert t (Hex.MvPoly.Kernel.insertSum ts x✝)

def Hex.MvPoly.Kernel.merge {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] : Nat → PolyList κ → PolyList κ → PolyList κ

Linear merge of descending term lists. Recursion is structural on fuel. The public caller supplies the sum of the lengths, so its fallback is never needed; the fallback keeps the denotation law unconditional.

Equations

• One or more equations did not get rendered due to their size.
• Hex.MvPoly.Kernel.merge x✝¹ [] x✝ = x✝
• Hex.MvPoly.Kernel.merge x✝¹ x✝ [] = x✝
• Hex.MvPoly.Kernel.merge 0 x✝¹ x✝ = Hex.MvPoly.Kernel.insertSum x✝¹ x✝

def Hex.MvPoly.Kernel.add {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] (p q : PolyList κ) : PolyList κ

Add canonical term lists in one merge pass.

Equations

• Hex.MvPoly.Kernel.add p q = Hex.MvPoly.Kernel.merge ((List.length p).add (List.length q)) p q

def Hex.MvPoly.Kernel.mapCoeffs {κ : Type u_1} [Zero κ] [DecidableEq κ] (f : κ → κ) : PolyList κ → PolyList κ

Map coefficients, filtering zero results without changing exponents.

Equations

• Hex.MvPoly.Kernel.mapCoeffs f [] = []
• Hex.MvPoly.Kernel.mapCoeffs f (u :: us) = if f u.snd = 0 then Hex.MvPoly.Kernel.mapCoeffs f us else (u.fst, f u.snd) :: Hex.MvPoly.Kernel.mapCoeffs f us

def Hex.MvPoly.Kernel.neg {κ : Type u_1} [Zero κ] [Neg κ] [DecidableEq κ] (p : PolyList κ) : PolyList κ

Negate a canonical term list, defensively filtering zero results.

Equations

• Hex.MvPoly.Kernel.neg p = Hex.MvPoly.Kernel.mapCoeffs Neg.neg p

def Hex.MvPoly.Kernel.sub {κ : Type u_1} [Zero κ] [Add κ] [Neg κ] [DecidableEq κ] (p q : PolyList κ) : PolyList κ

Subtraction through canonical addition and negation.

Equations

• Hex.MvPoly.Kernel.sub p q = Hex.MvPoly.Kernel.add p (Hex.MvPoly.Kernel.neg q)

def Hex.MvPoly.Kernel.smul {κ : Type u_1} [Zero κ] [Mul κ] [DecidableEq κ] (a : κ) (p : PolyList κ) : PolyList κ

Multiply every coefficient by a scalar, filtering zero products.

Equations

• Hex.MvPoly.Kernel.smul a p = Hex.MvPoly.Kernel.mapCoeffs (fun (c : κ) => a * c) p

def Hex.MvPoly.Kernel.mulTermImpl {κ : Type u_1} [Zero κ] [Add κ] [Mul κ] [DecidableEq κ] (t : Term κ) : PolyList κ → PolyList κ

Multiply one term by every term of a polynomial, canonicalizing the row.

Equations

• Hex.MvPoly.Kernel.mulTermImpl t [] = []
• Hex.MvPoly.Kernel.mulTermImpl t (u :: us) = Hex.MvPoly.Kernel.insert (Hex.MvPoly.Kernel.addExp t.fst u.fst, t.snd * u.snd) (Hex.MvPoly.Kernel.mulTermImpl t us)

noncomputable def Hex.MvPoly.Kernel.mulTerm {κ : Type u_1} [Zero κ] [Add κ] [Mul κ] [DecidableEq κ] (t : Term κ) (p : PolyList κ) : PolyList κ

Kernel row multiplication; compilation uses the equation implementation.

Equations

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

@[simp]

theorem Hex.MvPoly.Kernel.mulTerm_nil {κ : Type u_1} [Zero κ] [Add κ] [Mul κ] [DecidableEq κ] (t : Term κ) : mulTerm t [] = []

@[simp]

theorem Hex.MvPoly.Kernel.mulTerm_cons {κ : Type u_1} [Zero κ] [Add κ] [Mul κ] [DecidableEq κ] (t u : Term κ) (us : PolyList κ) : mulTerm t (u :: us) = insert (addExp t.fst u.fst, t.snd * u.snd) (mulTerm t us)

@[csimp]

theorem Hex.MvPoly.Kernel.mulTerm_eq_impl : @mulTerm = @mulTermImpl

def Hex.MvPoly.Kernel.sumRows {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] : List (PolyList κ) → PolyList κ

Sum rows, used for the total fallback of balanced merging.

Equations

• Hex.MvPoly.Kernel.sumRows [] = []
• Hex.MvPoly.Kernel.sumRows (p :: ps) = Hex.MvPoly.Kernel.add p (Hex.MvPoly.Kernel.sumRows ps)

def Hex.MvPoly.Kernel.mergeRound {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] : List (PolyList κ) → List (PolyList κ)

Merge each adjacent pair of rows.

Equations

• Hex.MvPoly.Kernel.mergeRound [] = []
• Hex.MvPoly.Kernel.mergeRound [p] = [p]
• Hex.MvPoly.Kernel.mergeRound (p :: q :: ps) = Hex.MvPoly.Kernel.add p q :: Hex.MvPoly.Kernel.mergeRound ps

def Hex.MvPoly.Kernel.mergeRows {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] : Nat → List (PolyList κ) → PolyList κ

Balanced merge rounds, structurally recursive on a row-count budget.

Equations

• Hex.MvPoly.Kernel.mergeRows x✝ [] = []
• Hex.MvPoly.Kernel.mergeRows x✝ [p] = p
• Hex.MvPoly.Kernel.mergeRows 0 x✝ = Hex.MvPoly.Kernel.sumRows x✝
• Hex.MvPoly.Kernel.mergeRows fuel.succ x✝ = Hex.MvPoly.Kernel.mergeRows fuel (Hex.MvPoly.Kernel.mergeRound x✝)

def Hex.MvPoly.Kernel.mul {κ : Type u_1} [Zero κ] [Add κ] [Mul κ] [DecidableEq κ] (p q : PolyList κ) : PolyList κ

Multiply via translated rows and balanced linear merges.

Equations

• Hex.MvPoly.Kernel.mul p q = Hex.MvPoly.Kernel.mergeRows (List.length p) (List.map (fun (t : Hex.MvPoly.Kernel.Term κ) => Hex.MvPoly.Kernel.mulTerm t q) p)

def Hex.MvPoly.Kernel.isZero {κ : Type u_1} : PolyList κ → Bool

The zero test for a canonical list.

Equations

• Hex.MvPoly.Kernel.isZero [] = true
• Hex.MvPoly.Kernel.isZero (u :: us) = false

def Hex.MvPoly.Kernel.beqImpl {κ : Type u_1} [DecidableEq κ] : PolyList κ → PolyList κ → Bool

Structural equality of term lists, with explicit exponent comparison.

Equations

• Hex.MvPoly.Kernel.beqImpl [] [] = true
• Hex.MvPoly.Kernel.beqImpl (t :: ts) (u :: us) = (Hex.MvPoly.Kernel.expBeq t.fst u.fst && decide (t.snd = u.snd) && Hex.MvPoly.Kernel.beqImpl ts us)
• Hex.MvPoly.Kernel.beqImpl x✝¹ x✝ = false

noncomputable def Hex.MvPoly.Kernel.beq {κ : Type u_1} [DecidableEq κ] (p q : PolyList κ) : Bool

Kernel list equality; compilation uses the equation implementation.

Equations

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

@[simp]

theorem Hex.MvPoly.Kernel.beq_nil {κ : Type u_1} [DecidableEq κ] (q : PolyList κ) : beq [] q = match q with | [] => true | head :: tail => false

@[simp]

theorem Hex.MvPoly.Kernel.beq_cons_nil {κ : Type u_1} [DecidableEq κ] (t : Term κ) (ts : PolyList κ) : beq (t :: ts) [] = false

@[simp]

theorem Hex.MvPoly.Kernel.beq_cons_cons {κ : Type u_1} [DecidableEq κ] (t u : Term κ) (ts us : PolyList κ) : beq (t :: ts) (u :: us) = (expBeq t.fst u.fst && decide (t.snd = u.snd) && beq ts us)

@[csimp]

theorem Hex.MvPoly.Kernel.beq_eq_impl : @beq = @beqImpl

def Hex.MvPoly.Kernel.pow {κ : Type u_1} [One κ] [Mul κ] (a : κ) : Nat → κ

Linear-time exponentiation used by evalAt; unlike the reference repeated-squaring helper this is visibly structural recursion on Nat.

Equations

• Hex.MvPoly.Kernel.pow a 0 = 1
• Hex.MvPoly.Kernel.pow a n.succ = Hex.MvPoly.Kernel.pow a n * a

def Hex.MvPoly.Kernel.evalMono {κ : Type u_1} [One κ] [Mul κ] : List κ → List Nat → κ

Evaluate a monomial at a list point, stopping at the shorter list.

Equations

• Hex.MvPoly.Kernel.evalMono (x_2 :: xs) (e :: es) = Hex.MvPoly.Kernel.pow x_2 e * Hex.MvPoly.Kernel.evalMono xs es
• Hex.MvPoly.Kernel.evalMono x✝¹ x✝ = 1

def Hex.MvPoly.Kernel.evalAt {κ : Type u_1} [Zero κ] [One κ] [Add κ] [Mul κ] (x : List κ) : PolyList κ → κ

Evaluate a term list at a point.

Equations

• Hex.MvPoly.Kernel.evalAt x [] = 0
• Hex.MvPoly.Kernel.evalAt x (u :: us) = u.snd * Hex.MvPoly.Kernel.evalMono x u.fst + Hex.MvPoly.Kernel.evalAt x us

def Hex.MvPoly.Kernel.zeroExp : Nat → List Nat

The zero exponent list of length n.

Equations

• Hex.MvPoly.Kernel.zeroExp 0 = []
• Hex.MvPoly.Kernel.zeroExp n.succ = 0 :: Hex.MvPoly.Kernel.zeroExp n

def Hex.MvPoly.Kernel.one {κ : Type u_1} [Zero κ] [One κ] [DecidableEq κ] (n : Nat) : PolyList κ

The list-form multiplicative identity in n variables.

Equations

• Hex.MvPoly.Kernel.one n = if 1 = 0 then [] else [(Hex.MvPoly.Kernel.zeroExp n, 1)]

def Hex.MvPoly.Kernel.Canonical {κ : Type u_1} [Zero κ] (n : Nat) (p : PolyList κ) : Prop

Canonical lists have the declared arity, strictly descending lexicographic exponents, and no zero coefficient. The arity conjunct is essential: without it distinct exponent lists can denote the same fixed-arity monomial.

Equations

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

theorem Hex.MvPoly.Kernel.length_zeroExp (n : Nat) : (zeroExp n).length = n

The structurally generated zero exponent has its declared length.

theorem Hex.MvPoly.Kernel.one_canonical {κ : Type u_1} [Zero κ] [One κ] [DecidableEq κ] (n : Nat) : Canonical n (one n)

The list-form multiplicative identity is canonical.

theorem Hex.MvPoly.Kernel.expBeq_iff {a b : List Nat} : expBeq a b = true ↔ a = b

The explicit equality test agrees with equality of exponent lists.

theorem Hex.MvPoly.Kernel.expCmp_eq_compare (a b : List Nat) : expCmp a b = compare a b

The explicit kernel comparator is the standard lexicographic list comparison.

theorem Hex.MvPoly.Kernel.expCmp_eq_lt_iff {a b : List Nat} : expCmp a b = Ordering.lt ↔ a < b

The result .lt of the explicit comparator is lexicographic <.

theorem Hex.MvPoly.Kernel.length_addExp {a b : List Nat} {n : Nat} (ha : a.length = n) (hb : b.length = n) : (addExp a b).length = n

Pointwise exponent addition preserves a common arity.

theorem Hex.MvPoly.Kernel.exp_mem_insert {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] {t u : Term κ} {us : PolyList κ} (h : u ∈ insert t us) : u.fst = t.fst ∨ ∃ (v : Term κ), v ∈ us ∧ u.fst = v.fst

Every exponent emitted by insertion is either the inserted exponent or an exponent already present.

theorem Hex.MvPoly.Kernel.insert_canonical {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] {n : Nat} {t : Term κ} {p : PolyList κ} (ht : t.fst.length = n) (hp : Canonical n p) : Canonical n (insert t p)

Insertion preserves canonical form. The inserted coefficient may be zero; in that case no term is added.

theorem Hex.MvPoly.Kernel.normalize_canonical {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] {n : Nat} {p : PolyList κ} (h : ∀ (t : Term κ), t ∈ p → t.fst.length = n) : Canonical n (normalize p)

Normalization emits a canonical list when every input exponent has the declared arity.

theorem Hex.MvPoly.Kernel.insertSum_canonical {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] {n : Nat} {p q : PolyList κ} (hp : Canonical n p) (hq : Canonical n q) : Canonical n (insertSum p q)

Addition preserves canonical form.

theorem Hex.MvPoly.Kernel.merge_canonical {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] {n : Nat} (fuel : Nat) {p q : PolyList κ} (hp : Canonical n p) (hq : Canonical n q) : Canonical n (merge fuel p q)

Merging preserves canonical form, including for an undersupplied budget.

theorem Hex.MvPoly.Kernel.add_canonical {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] {n : Nat} {p q : PolyList κ} (hp : Canonical n p) (hq : Canonical n q) : Canonical n (add p q)

Addition preserves canonical form.

theorem Hex.MvPoly.Kernel.merge_stable {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] (fuel extra : Nat) (p q : PolyList κ) (h : List.length p + List.length q ≤ fuel) : merge (fuel + extra) p q = merge fuel p q

Once the combined input length is covered, extra fuel cannot change a merge. In particular the insertion fallback is irrelevant to public addition.

theorem Hex.MvPoly.Kernel.add_eq_merge {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] (p q : PolyList κ) (fuel : Nat) (h : List.length p + List.length q ≤ fuel) : add p q = merge fuel p q

The public addition budget agrees with any larger merge budget.

theorem Hex.MvPoly.Kernel.exp_mem_mapCoeffs {κ : Type u_1} [Zero κ] [DecidableEq κ] (f : κ → κ) {u : Term κ} {p : PolyList κ} (hu : u ∈ mapCoeffs f p) : ∃ (v : Term κ), v ∈ p ∧ u.fst = v.fst

A coefficient map preserves the exponent of every surviving term.

theorem Hex.MvPoly.Kernel.mapCoeffs_canonical {κ : Type u_1} [Zero κ] [DecidableEq κ] (f : κ → κ) {n : Nat} {p : PolyList κ} (hp : Canonical n p) : Canonical n (mapCoeffs f p)

Mapping and filtering coefficients preserves canonical form.

theorem Hex.MvPoly.Kernel.neg_canonical {κ : Type u_1} [Zero κ] [Neg κ] [DecidableEq κ] {n : Nat} {p : PolyList κ} (hp : Canonical n p) : Canonical n (neg p)

Negation preserves canonical form.

theorem Hex.MvPoly.Kernel.sub_canonical {κ : Type u_1} [Zero κ] [Add κ] [Neg κ] [DecidableEq κ] {n : Nat} {p q : PolyList κ} (hp : Canonical n p) (hq : Canonical n q) : Canonical n (sub p q)

Subtraction preserves canonical form.

theorem Hex.MvPoly.Kernel.smul_canonical {κ : Type u_1} [Zero κ] [Mul κ] [DecidableEq κ] (a : κ) {n : Nat} {p : PolyList κ} (hp : Canonical n p) : Canonical n (smul a p)

Scalar multiplication preserves canonical form.

theorem Hex.MvPoly.Kernel.mulTerm_canonical {κ : Type u_1} [Zero κ] [Add κ] [Mul κ] [DecidableEq κ] {n : Nat} {t : Term κ} {p : PolyList κ} (ht : t.fst.length = n) (hp : Canonical n p) : Canonical n (mulTerm t p)

A translated product row is canonical.

theorem Hex.MvPoly.Kernel.mergeRows_canonical {κ : Type u_1} [Zero κ] [Add κ] [DecidableEq κ] {n : Nat} (fuel : Nat) (ps : List (PolyList κ)) (h : ∀ (p : PolyList κ), p ∈ ps → Canonical n p) : Canonical n (mergeRows fuel ps)

Balanced merging preserves canonical form.

theorem Hex.MvPoly.Kernel.mul_canonical {κ : Type u_1} [Zero κ] [Add κ] [Mul κ] [DecidableEq κ] {n : Nat} {p q : PolyList κ} (hp : Canonical n p) (hq : Canonical n q) : Canonical n (mul p q)

Multiplication preserves canonical form.

def Hex.MvPoly.Kernel.isCanonical {κ : Type u_1} [Zero κ] [DecidableEq κ] (n : Nat) : PolyList κ → Bool

Boolean check for the canonical invariant.

Equations

• Hex.MvPoly.Kernel.isCanonical n [] = true
• Hex.MvPoly.Kernel.isCanonical n [t] = (t.fst.length.beq n && decide (t.snd ≠ 0))
• Hex.MvPoly.Kernel.isCanonical n (t :: u :: ts) = (t.fst.length.beq n && decide (t.snd ≠ 0) && Hex.MvPoly.Kernel.expCmp t.fst u.fst == Ordering.gt && Hex.MvPoly.Kernel.isCanonical n (u :: ts))

theorem Hex.MvPoly.Kernel.isCanonical_iff {κ : Type u_1} [Zero κ] [DecidableEq κ] {n : Nat} {p : PolyList κ} : isCanonical n p = true ↔ Canonical n p

The Boolean canonicality check decides the proposition.

def Hex.MvPoly.Kernel.mono (n : Nat) (e : List Nat) : Mono n

Read an exponent list as an n-variable monomial. Canonical inputs have exactly length n; getD merely makes denotation total on malformed input.

Equations

• Hex.MvPoly.Kernel.mono n e = Hex.Vector.ofFn' fun (i : Fin n) => e.getD (↑i) 0

def Hex.MvPoly.Kernel.monoFast (n : Nat) (e : List Nat) : Mono n

Materialize the input once instead of repeatedly indexing a linked list.

Equations

• Hex.MvPoly.Kernel.monoFast n e = Hex.Vector.ofFn' fun (i : Fin n) => e.toArray[↑i]?.getD 0

@[csimp]

theorem Hex.MvPoly.Kernel.mono_eq_fast : mono = monoFast

def Hex.MvPoly.Kernel.denote {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : PolyList κ → MvPoly n κ cmp

Denote a term list in the reference polynomial type.

Equations

• Hex.MvPoly.Kernel.denote [] = 0
• Hex.MvPoly.Kernel.denote (u :: us) = Hex.MvPoly.monomial (Hex.MvPoly.Kernel.mono n u.fst) u.snd + Hex.MvPoly.Kernel.denote us

def Hex.MvPoly.Kernel.toList {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p : MvPoly n κ cmp) : PolyList κ

Convert a reference polynomial to the fixed canonical list order. This is a producer-side conversion; certificate replay sees only its quoted result.

Equations

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

theorem Hex.MvPoly.Kernel.denote_insert {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (t : Term κ) (p : PolyList κ) : denote (insert t p) = monomial (mono n t.fst) t.snd + denote p

Inserting a term has the denotation of adding its monomial.

theorem Hex.MvPoly.Kernel.denote_normalize {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p : PolyList κ) : denote (normalize p) = denote p

Normalization does not change denotation.

theorem Hex.MvPoly.Kernel.denote_insertSum {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p q : PolyList κ) : denote (insertSum p q) = denote p + denote q

List addition denotes reference addition.

theorem Hex.MvPoly.Kernel.denote_merge {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (fuel : Nat) (p q : PolyList κ) : denote (merge fuel p q) = denote p + denote q

A merge has the denotation of the sum, for any fuel and any input.

theorem Hex.MvPoly.Kernel.denote_add {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p q : PolyList κ) : denote (add p q) = denote p + denote q

List addition denotes reference addition.

theorem Hex.MvPoly.Kernel.denote_neg {n : Nat} {κ : Type u} [Lean.Grind.CommRing κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p : PolyList κ) : denote (neg p) = -denote p

List negation denotes reference negation.

theorem Hex.MvPoly.Kernel.denote_sub {n : Nat} {κ : Type u} [Lean.Grind.CommRing κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p q : PolyList κ) : denote (sub p q) = denote p - denote q

List subtraction denotes reference subtraction.

theorem Hex.MvPoly.Kernel.denote_smul {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (a : κ) (p : PolyList κ) : denote (smul a p) = C a * denote p

List scalar multiplication denotes multiplication by a constant.

theorem Hex.MvPoly.Kernel.get_mono (n : Nat) (e : List Nat) (i : Fin n) : (mono n e)[i] = e.getD (↑i) 0

Reading a list exponent through its denotation uses getD.

theorem Hex.MvPoly.Kernel.mono_zeroExp (n : Nat) : mono n (zeroExp n) = Mono.zero

The zero exponent denotes the reference constant monomial.

theorem Hex.MvPoly.Kernel.denote_one {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : denote (one n) = 1

The list multiplicative identity denotes the reference identity.

theorem Hex.MvPoly.Kernel.getD_addExp {a b : List Nat} {n i : Nat} (ha : a.length = n) (hb : b.length = n) (hi : i < n) : (addExp a b).getD i 0 = a.getD i 0 + b.getD i 0

A pointwise sum has the pointwise sum of getD values when both lists have the declared arity.

theorem Hex.MvPoly.Kernel.mono_addExp {a b : List Nat} {n : Nat} (ha : a.length = n) (hb : b.length = n) : mono n (addExp a b) = (mono n a).mul (mono n b)

List exponent addition denotes monomial multiplication.

theorem Hex.MvPoly.Kernel.denote_mulTerm {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (t : Term κ) (p : PolyList κ) (ht : t.fst.length = n) (hp : ∀ (u : Term κ), u ∈ p → u.fst.length = n) : denote (mulTerm t p) = monomial (mono n t.fst) t.snd * denote p

Multiplying one term through a list denotes multiplication by its reference monomial.

theorem Hex.MvPoly.Kernel.denote_mergeRows {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (fuel : Nat) (ps : List (PolyList κ)) : denote (mergeRows fuel ps) = denote (sumRows ps)

Balanced merging denotes the sum of its rows, independently of fuel.

theorem Hex.MvPoly.Kernel.denote_mul {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p q : PolyList κ) (hp : ∀ (t : Term κ), t ∈ p → t.fst.length = n) (hq : ∀ (t : Term κ), t ∈ q → t.fst.length = n) : denote (mul p q) = denote p * denote q

List multiplication denotes reference multiplication.

theorem Hex.MvPoly.Kernel.denote_eq_ofTerms {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p : PolyList κ) : denote p = ofTerms (List.map (fun (t : Term κ) => (mono n t.fst, t.snd)) p)

The recursive sum denotation agrees with the reference bulk constructor.

theorem Hex.MvPoly.Kernel.mono_toList {n : Nat} (m : Mono n) : mono n (Vector.toList m) = m

Converting a vector monomial to a list and reading it back is exact.

theorem Hex.MvPoly.Kernel.toList_canonical {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p : MvPoly n κ cmp) : Canonical n (toList p)

Producer conversion always emits a canonical list.

theorem Hex.MvPoly.Kernel.denote_toList {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p : MvPoly n κ cmp) : denote (toList p) = p

Producer conversion round-trips through denotation.

def Hex.MvPoly.Kernel.toRows {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (rows : List (List (MvPoly n κ cmp))) : List (List (PolyList κ))

Producer conversion for nested polynomial lists. A matrix consumer passes rowLists P; no matrix dependency is needed in this library.

Equations

• Hex.MvPoly.Kernel.toRows rows = List.map (List.map Hex.MvPoly.Kernel.toList) rows

theorem Hex.MvPoly.Kernel.denote_toRows {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (rows : List (List (MvPoly n κ cmp))) : List.map (List.map denote) (toRows rows) = rows

Entrywise denotation identifies quoted rows with the original rows. In particular, instantiate rows with rowLists P for a reference matrix.

theorem Hex.MvPoly.Kernel.pow_eq_pow {κ : Type u_1} [Lean.Grind.Semiring κ] (a : κ) (k : Nat) : pow a k = a ^ k

The linear structural power used by certificate replay has the standard semiring value.

theorem Hex.MvPoly.Kernel.evalMono_eq_prod {κ : Type u_1} [Lean.Grind.Semiring κ] {n : Nat} {x : List κ} {e : List Nat} (hx : x.length = n) (he : e.length = n) : evalMono x e = Mono.prod (fun (i : Fin n) => x.getD (↑i) 0) (mono n e)

List monomial evaluation agrees with reference monomial evaluation when the point and exponent list have the declared arity.

theorem Hex.MvPoly.Kernel.evalAt_denote {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (x : List κ) (p : PolyList κ) (hx : x.length = n) (hp : ∀ (t : Term κ), t ∈ p → t.fst.length = n) : evalAt x p = eval (fun (i : Fin n) => x.getD (↑i) 0) (denote p)

List evaluation commutes with evaluation of the reference denotation.

theorem Hex.MvPoly.Kernel.toList_mono {e : List Nat} {n : Nat} (h : e.length = n) : Vector.toList (mono n e) = e

An exact-length exponent list is recovered from its monomial.

theorem Hex.MvPoly.Kernel.mono_inj {a b : List Nat} {n : Nat} (ha : a.length = n) (hb : b.length = n) : mono n a = mono n b ↔ a = b

Denotation of exponent lists is injective at a fixed arity.

def Hex.MvPoly.Kernel.coeffAt {κ : Type u_1} [Zero κ] (e : List Nat) : PolyList κ → κ

Coefficient lookup on a canonical list.

Equations

• Hex.MvPoly.Kernel.coeffAt e [] = 0
• Hex.MvPoly.Kernel.coeffAt e (u :: us) = if e = u.fst then u.snd else Hex.MvPoly.Kernel.coeffAt e us

theorem Hex.MvPoly.Kernel.coeff_denote_eq_zero {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (e : List Nat) (p : PolyList κ) (he : e.length = n) (hp : ∀ (t : Term κ), t ∈ p → t.fst.length = n) (hnot : ∀ (t : Term κ), t ∈ p → e ≠ t.fst) : coeff (mono n e) (denote p) = 0

A monomial absent from a well-formed list has zero coefficient in its denotation.

theorem Hex.MvPoly.Kernel.coeff_denote {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (e : List Nat) (p : PolyList κ) (he : e.length = n) (hp : Canonical n p) : coeff (mono n e) (denote p) = coeffAt e p

Reference coefficients read back the stored coefficient of a canonical list.

theorem Hex.MvPoly.Kernel.coeffAt_eq_zero_of_gt_head {κ : Type u_1} [Zero κ] {e : List Nat} {t : Term κ} {ts : PolyList κ} (hp : List.Pairwise (fun (a b : Term κ) => b.fst < a.fst) (t :: ts)) (he : t.fst < e) : coeffAt e (t :: ts) = 0

Lookup is zero above the head of a descending canonical list.

theorem Hex.MvPoly.Kernel.coeffAt_tail_eq_zero {κ : Type u_1} [Zero κ] {t : Term κ} {ts : PolyList κ} (hp : List.Pairwise (fun (a b : Term κ) => b.fst < a.fst) (t :: ts)) : coeffAt t.fst ts = 0

The tail has zero coefficient at the head exponent.

theorem Hex.MvPoly.Kernel.coeffAt_ext {κ : Type u_1} [Zero κ] {p q : PolyList κ} (hp : List.Pairwise (fun (a b : Term κ) => b.fst < a.fst) p) (hq : List.Pairwise (fun (a b : Term κ) => b.fst < a.fst) q) (hp0 : ∀ (t : Term κ), t ∈ p → t.snd ≠ 0) (hq0 : ∀ (t : Term κ), t ∈ q → t.snd ≠ 0) (h : ∀ (e : List Nat), coeffAt e p = coeffAt e q) : p = q

Canonical lists with the same coefficient function are equal.

theorem Hex.MvPoly.Kernel.coeffAt_eq_zero_of_length_ne {κ : Type u_1} [Zero κ] {e : List Nat} {n : Nat} {p : PolyList κ} (hp : ∀ (t : Term κ), t ∈ p → t.fst.length = n) (he : e.length ≠ n) : coeffAt e p = 0

A lookup with the wrong arity is zero in a well-formed list.

theorem Hex.MvPoly.Kernel.denote_injective {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {p q : PolyList κ} (hp : Canonical n p) (hq : Canonical n q) (h : denote p = denote q) : p = q

Canonical list denotation is injective.

theorem Hex.MvPoly.Kernel.toList_denote {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {p : PolyList κ} (hp : Canonical n p) : toList (denote p) = p

A canonical list is recovered by converting its denotation back to list form.

theorem Hex.MvPoly.Kernel.beq_eq_true_iff {κ : Type u_1} [DecidableEq κ] {p q : PolyList κ} : beq p q = true ↔ p = q

Structural equality returns true exactly for equal term lists.

theorem Hex.MvPoly.Kernel.isZero_iff {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {p : PolyList κ} (hp : Canonical n p) : isZero p = true ↔ denote p = 0

The empty-list test agrees with zero denotation on canonical inputs.

theorem Hex.MvPoly.Kernel.beq_iff {n : Nat} {κ : Type u} [Lean.Grind.Semiring κ] [BEq κ] [LawfulBEq κ] [DecidableEq κ] {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {p q : PolyList κ} (hp : Canonical n p) (hq : Canonical n q) : beq p q = true ↔ denote p = denote q

Structural equality agrees with denotational equality on canonical inputs.

theorem Hex.MvPoly.Kernel.beq_refl {κ : Type u_1} [DecidableEq κ] (p : PolyList κ) : beq p p = true

Reflexivity of list equality, stated at the kernel Boolean interface.

theorem Hex.MvPoly.Kernel.beq_symm {κ : Type u_1} [DecidableEq κ] {p q : PolyList κ} (h : beq p q = true) : beq q p = true

Symmetry of list equality, stated at the kernel Boolean interface.

theorem Hex.MvPoly.Kernel.beq_trans {κ : Type u_1} [DecidableEq κ] {p q r : PolyList κ} (hpq : beq p q = true) (hqr : beq q r = true) : beq p r = true

Transitivity of list equality, stated at the kernel Boolean interface.