def Hex.MvPoly.Kernel.residueAdd (p a b : Nat) : Nat

Modular addition of coefficients.

Equations

• Hex.MvPoly.Kernel.residueAdd p a b = (a.add b).mod p

def Hex.MvPoly.Kernel.residueMul (p a b : Nat) : Nat

Modular multiplication of coefficients.

Equations

• Hex.MvPoly.Kernel.residueMul p a b = (a.mul b).mod p

def Hex.MvPoly.Kernel.residueNeg (p a : Nat) : Nat

Negation by multiplication by the residue of -1. Pattern matching on the modulus keeps the coefficient path within natural addition, multiplication, modulus, and structural recursion.

Equations

• Hex.MvPoly.Kernel.residueNeg 0 a = 0
• Hex.MvPoly.Kernel.residueNeg k.succ a = Hex.MvPoly.Kernel.residueMul k.succ k a

def Hex.MvPoly.Kernel.addMod (p : Nat) (a b : PolyList Nat) : PolyList Nat

Merge canonical residue lists, reducing every coefficient collision.

Equations

• Hex.MvPoly.Kernel.addMod p a b = Hex.MvPoly.Kernel.add a b

def Hex.MvPoly.Kernel.mulMod (p : Nat) (a b : PolyList Nat) : PolyList Nat

Multiply translated rows with modular products and balanced modular merges.

Equations

• Hex.MvPoly.Kernel.mulMod p a b = Hex.MvPoly.Kernel.mul a b

def Hex.MvPoly.Kernel.negMod (p : Nat) (a : PolyList Nat) : PolyList Nat

Negate residue coefficients and remove zero results.

Equations

• Hex.MvPoly.Kernel.negMod p a = Hex.MvPoly.Kernel.mapCoeffs (Hex.MvPoly.Kernel.residueNeg p) a

def Hex.MvPoly.Kernel.smulMod (p c : Nat) (a : PolyList Nat) : PolyList Nat

Multiply by an arbitrary natural-number scalar modulo the modulus.

Equations

• Hex.MvPoly.Kernel.smulMod p c a = Hex.MvPoly.Kernel.mapCoeffs (Hex.MvPoly.Kernel.residueMul p c) a

def Hex.MvPoly.Kernel.subMod (p : Nat) (a b : PolyList Nat) : PolyList Nat

Subtraction of canonical residue lists.

Equations

• Hex.MvPoly.Kernel.subMod p a b = Hex.MvPoly.Kernel.addMod p a (Hex.MvPoly.Kernel.negMod p b)

def Hex.MvPoly.Kernel.CanonicalMod (p n : Nat) (a : PolyList Nat) : Prop

Canonical exponents and nonzero coefficients strictly below the modulus.

Equations

• Hex.MvPoly.Kernel.CanonicalMod p n a = (Hex.MvPoly.Kernel.Canonical n a ∧ ∀ (t : Hex.MvPoly.Kernel.Term Nat), t ∈ a → t.snd < p)

def Hex.MvPoly.Kernel.isCanonicalMod (p n : Nat) (a : PolyList Nat) : Bool

Check canonical form and the residue bound on untrusted certificate data.

Equations

• Hex.MvPoly.Kernel.isCanonicalMod p n a = (Hex.MvPoly.Kernel.isCanonical n a && List.all a fun (t : Hex.MvPoly.Kernel.Term Nat) => t.snd.blt p)

theorem Hex.MvPoly.Kernel.isCanonicalMod_iff {p n : Nat} {a : PolyList Nat} : isCanonicalMod p n a = true ↔ CanonicalMod p n a

The Boolean check is equivalent to canonical residue form.

def Hex.MvPoly.Kernel.oneMod (p n : Nat) : PolyList Nat

The multiplicative identity, including the trivial residue ring.

Equations

• Hex.MvPoly.Kernel.oneMod p n = if Nat.blt 1 p = true then [(Hex.MvPoly.Kernel.zeroExp n, 1)] else []

theorem Hex.MvPoly.Kernel.oneMod_canonical (p n : Nat) : CanonicalMod p n (oneMod p n)

The modular identity is canonical for every modulus.

theorem Hex.MvPoly.Kernel.addMod_canonical (p : Nat) {n : Nat} {a b : PolyList Nat} (ha : CanonicalMod p n a) (hb : CanonicalMod p n b) : CanonicalMod p n (addMod p a b)

Modular addition preserves canonical residue form for every modulus.

theorem Hex.MvPoly.Kernel.mulMod_canonical (p : Nat) {n : Nat} {a b : PolyList Nat} (ha : CanonicalMod p n a) (hb : CanonicalMod p n b) : CanonicalMod p n (mulMod p a b)

Modular multiplication preserves canonical residue form for every modulus.

theorem Hex.MvPoly.Kernel.negMod_canonical (p : Nat) {n : Nat} {a : PolyList Nat} (ha : CanonicalMod p n a) : CanonicalMod p n (negMod p a)

Modular negation preserves canonical residue form for every modulus.

theorem Hex.MvPoly.Kernel.smulMod_canonical (p c : Nat) {n : Nat} {a : PolyList Nat} (ha : CanonicalMod p n a) : CanonicalMod p n (smulMod p c a)

Modular scaling preserves canonical form for every modulus and scalar.

theorem Hex.MvPoly.Kernel.subMod_canonical (p : Nat) {n : Nat} {a b : PolyList Nat} (ha : CanonicalMod p n a) (hb : CanonicalMod p n b) : CanonicalMod p n (subMod p a b)

Modular subtraction preserves canonical residue form for every modulus.