3.4. Arithmetic and correctness🔗

Addition merges supports and deletes coefficients that cancel. Multiplication accumulates every pairwise monomial product into one canonical output map. Negation maps the values in a single tree pass. The usual +, -, unary -, *, and power notation uses these executable operations.

def

Hex.MvPoly.add.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Add R] [Zero R] [BEq R] [LawfulBEq R]
  (p q : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp
Hex.MvPoly.add.{u} {n : ℕ} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Add R] [Zero R] [BEq R] [LawfulBEq R]
  (p q : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp

Polynomial addition, combining equal monomials and deleting cancellations.

def

Hex.MvPoly.neg.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Neg R] [Zero R] [BEq R] [LawfulBEq R]
  (p : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp
Hex.MvPoly.neg.{u} {n : ℕ} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Neg R] [Zero R] [BEq R] [LawfulBEq R]
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp

Coefficientwise negation, filtering any zero result in one tree pass.

def

Hex.MvPoly.mul.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Add R] [Mul R] [Zero R] [BEq R] [LawfulBEq R]
  (p q : Hex.MvPoly n R cmp) : Hex.MvPoly n R cmp
Hex.MvPoly.mul.{u} {n : ℕ} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Add R] [Mul R] [Zero R] [BEq R]
  [LawfulBEq R]
  (p q : Hex.MvPoly n R cmp) :
  Hex.MvPoly n R cmp

Polynomial multiplication. Every translated product term is accumulated directly into one output map, so collisions and cancellations are normalized as they arise.

Coefficient laws characterize the operations without exposing the backing map. In particular, a product coefficient is the convolution over every split of its target monomial.

theorem

Hex.MvPoly.coeff_add.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R]
  [DecidableEq R] (m : Hex.Mono n) (p q : Hex.MvPoly n R cmp) :
  Hex.MvPoly.coeff m (p + q) =
    Hex.MvPoly.coeff m p + Hex.MvPoly.coeff m q
Hex.MvPoly.coeff_add.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [BEq R] [LawfulBEq R]
  [Lean.Grind.Semiring R] [DecidableEq R]
  (m : Hex.Mono n)
  (p q : Hex.MvPoly n R cmp) :
  Hex.MvPoly.coeff m (p + q) =
    Hex.MvPoly.coeff m p +
      Hex.MvPoly.coeff m q

Coefficients distribute over polynomial addition.

theorem

Hex.MvPoly.coeff_neg.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Ring R]
  [DecidableEq R] (m : Hex.Mono n) (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly.coeff m (-p) = -Hex.MvPoly.coeff m p
Hex.MvPoly.coeff_neg.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [BEq R] [LawfulBEq R]
  [Lean.Grind.Ring R] [DecidableEq R]
  (m : Hex.Mono n)
  (p : Hex.MvPoly n R cmp) :
  Hex.MvPoly.coeff m (-p) =
    -Hex.MvPoly.coeff m p

Coefficients commute with polynomial negation.

theorem

Hex.MvPoly.coeff_mul.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R]
  [DecidableEq R] (m : Hex.Mono n) (p q : Hex.MvPoly n R cmp) :
  Hex.MvPoly.coeff m (p * q) =
    List.foldl
      (fun acc ab =>
        acc + Hex.MvPoly.coeff ab.1 p * Hex.MvPoly.coeff ab.2 q)
      0 m.splits
Hex.MvPoly.coeff_mul.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [BEq R] [LawfulBEq R]
  [Lean.Grind.Semiring R] [DecidableEq R]
  (m : Hex.Mono n)
  (p q : Hex.MvPoly n R cmp) :
  Hex.MvPoly.coeff m (p * q) =
    List.foldl
      (fun acc ab =>
        acc +
          Hex.MvPoly.coeff ab.1 p *
            Hex.MvPoly.coeff ab.2 q)
      0 m.splits

A product coefficient is the convolution over monomial splittings.

The executable operations satisfy the complete commutative-semiring and commutative-ring law set. HexMvPolyMathlib packages those laws as standard Mathlib structures; the computational library itself remains independent of Mathlib.