def Hex.MvPoly.Kernel.ofResidues (p : Nat) [ZMod64.Bounds p] (a : PolyList (ZMod64 p)) : PolyList Nat

Producer-side conversion from machine-word residues to quoted naturals.

Equations

• Hex.MvPoly.Kernel.ofResidues p a = Hex.MvPoly.Kernel.CoeffMap.map Hex.ZMod64.toNat a

def Hex.MvPoly.Kernel.toResidues (p : Nat) [ZMod64.Bounds p] (a : PolyList Nat) : PolyList (ZMod64 p)

Interpret natural coefficients as residues. This is a semantic conversion, never part of the closed Boolean certificate computation.

Equations

• Hex.MvPoly.Kernel.toResidues p a = Hex.MvPoly.Kernel.CoeffMap.map (fun (c : Nat) => Hex.ZMod64.ofNat p c) a

@[simp]

theorem Hex.MvPoly.Kernel.toResidues_ofResidues (p : Nat) [ZMod64.Bounds p] (a : PolyList (ZMod64 p)) : toResidues p (ofResidues p a) = a

Reading back producer residues is exact, with no support assumptions.

theorem Hex.MvPoly.Kernel.ofResidues_toResidues (p : Nat) [ZMod64.Bounds p] {a : PolyList Nat} (ha : ∀ (t : Term Nat), t ∈ a → t.snd < p) : ofResidues p (toResidues p a) = a

Reading and quoting a bounded natural coefficient leaves it unchanged.

theorem Hex.MvPoly.Kernel.ofResidues_injective (p : Nat) [ZMod64.Bounds p] : Function.Injective (ofResidues p)

The encoding is injective on the executable coefficient carrier.

theorem Hex.MvPoly.Kernel.ofResidues_canonical (p : Nat) [ZMod64.Bounds p] {n : Nat} {a : PolyList (ZMod64 p)} : CanonicalMod p n (ofResidues p a) ↔ Canonical n a

Executable canonical lists quote to canonical residue lists.

theorem Hex.MvPoly.Kernel.toResidues_canonical (p : Nat) [ZMod64.Bounds p] {n : Nat} {a : PolyList Nat} (ha : CanonicalMod p n a) : Canonical n (toResidues p a)

Canonical natural residues have canonical executable denotation lists.

theorem Hex.MvPoly.Kernel.ofResidues_add (p : Nat) [ZMod64.Bounds p] (a b : PolyList (ZMod64 p)) : ofResidues p (add a b) = addMod p (ofResidues p a) (ofResidues p b)

Quoting commutes with modular addition.

theorem Hex.MvPoly.Kernel.ofResidues_mul (p : Nat) [ZMod64.Bounds p] (a b : PolyList (ZMod64 p)) : ofResidues p (mul a b) = mulMod p (ofResidues p a) (ofResidues p b)

Quoting commutes with modular multiplication.

theorem Hex.MvPoly.Kernel.ofResidues_smul (p : Nat) [ZMod64.Bounds p] (c : ZMod64 p) (a : PolyList (ZMod64 p)) : ofResidues p (smul c a) = smulMod p c.toNat (ofResidues p a)

Quoting commutes with scalar multiplication.

theorem Hex.MvPoly.Kernel.ofResidues_neg (p : Nat) [ZMod64.Bounds p] (a : PolyList (ZMod64 p)) : ofResidues p (neg a) = negMod p (ofResidues p a)

Quoting commutes with negation.

theorem Hex.MvPoly.Kernel.ofResidues_smul_nat (p : Nat) [ZMod64.Bounds p] (c : Nat) (a : PolyList (ZMod64 p)) : ofResidues p (smul (ZMod64.ofNat p c) a) = smulMod p c (ofResidues p a)

Natural scalars may be unreduced; multiplication reduces them modulo p.

theorem Hex.MvPoly.Kernel.toResidues_addMod (p : Nat) [ZMod64.Bounds p] {a b : PolyList Nat} (ha : ∀ (t : Term Nat), t ∈ a → t.snd < p) (hb : ∀ (t : Term Nat), t ∈ b → t.snd < p) : toResidues p (addMod p a b) = add (toResidues p a) (toResidues p b)

Reading modular addition agrees with executable addition on bounded inputs.

theorem Hex.MvPoly.Kernel.toResidues_mulMod (p : Nat) [ZMod64.Bounds p] {a b : PolyList Nat} (ha : ∀ (t : Term Nat), t ∈ a → t.snd < p) (hb : ∀ (t : Term Nat), t ∈ b → t.snd < p) : toResidues p (mulMod p a b) = mul (toResidues p a) (toResidues p b)

Reading modular multiplication agrees with executable multiplication.

theorem Hex.MvPoly.Kernel.toResidues_negMod (p : Nat) [ZMod64.Bounds p] {a : PolyList Nat} (ha : ∀ (t : Term Nat), t ∈ a → t.snd < p) : toResidues p (negMod p a) = neg (toResidues p a)

Reading modular negation agrees with executable negation.

theorem Hex.MvPoly.Kernel.toResidues_smulMod (p : Nat) [ZMod64.Bounds p] (c : Nat) {a : PolyList Nat} (ha : ∀ (t : Term Nat), t ∈ a → t.snd < p) : toResidues p (smulMod p c a) = smul (ZMod64.ofNat p c) (toResidues p a)

Reading modular scalar multiplication agrees with executable scaling.

theorem Hex.MvPoly.Kernel.toResidues_oneMod (p : Nat) [ZMod64.Bounds p] (n : Nat) : toResidues p (oneMod p n) = one n

Reading the modular identity gives the executable list identity.

def Hex.MvPoly.Kernel.denoteMod (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (a : PolyList Nat) : MvPoly n (ZMod64 p) cmp

Semantic denotation in the executable residue polynomial ring.

Equations

• Hex.MvPoly.Kernel.denoteMod p a = Hex.MvPoly.Kernel.denote (Hex.MvPoly.Kernel.toResidues p a)

@[simp]

theorem Hex.MvPoly.Kernel.denoteMod_nil (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : denoteMod p [] = 0

The empty residue list denotes zero.

@[simp]

theorem Hex.MvPoly.Kernel.denoteMod_oneMod (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : denoteMod p (oneMod p n) = 1

The residue-list identity denotes the polynomial identity.

theorem Hex.MvPoly.Kernel.denoteMod_addMod (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a b : PolyList Nat} (ha : CanonicalMod p n a) (hb : CanonicalMod p n b) : denoteMod p (addMod p a b) = denoteMod p a + denoteMod p b

Modular addition denotes polynomial addition on canonical inputs.

theorem Hex.MvPoly.Kernel.denoteMod_mulMod (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a b : PolyList Nat} (ha : CanonicalMod p n a) (hb : CanonicalMod p n b) : denoteMod p (mulMod p a b) = denoteMod p a * denoteMod p b

Modular multiplication denotes polynomial multiplication on canonical inputs.

theorem Hex.MvPoly.Kernel.denoteMod_negMod (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a : PolyList Nat} (ha : CanonicalMod p n a) : denoteMod p (negMod p a) = -denoteMod p a

Modular negation denotes polynomial negation on canonical inputs.

theorem Hex.MvPoly.Kernel.denoteMod_smulMod (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (c : Nat) {a : PolyList Nat} (ha : CanonicalMod p n a) : denoteMod p (smulMod p c a) = C (ZMod64.ofNat p c) * denoteMod p a

Modular scalar multiplication denotes multiplication by a residue constant.

theorem Hex.MvPoly.Kernel.denoteMod_subMod (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a b : PolyList Nat} (ha : CanonicalMod p n a) (hb : CanonicalMod p n b) : denoteMod p (subMod p a b) = denoteMod p a - denoteMod p b

Modular subtraction denotes polynomial subtraction on canonical inputs.

theorem Hex.MvPoly.Kernel.denoteMod_injective (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a b : PolyList Nat} (ha : CanonicalMod p n a) (hb : CanonicalMod p n b) (h : denoteMod p a = denoteMod p b) : a = b

Canonical residue lists are uniquely determined by their denotation.

theorem Hex.MvPoly.Kernel.isZero_mod_iff (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a : PolyList Nat} (ha : CanonicalMod p n a) : isZero a = true ↔ denoteMod p a = 0

The existing structural zero test is exact for canonical residue lists.

theorem Hex.MvPoly.Kernel.beq_mod_iff (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a b : PolyList Nat} (ha : CanonicalMod p n a) (hb : CanonicalMod p n b) : beq a b = true ↔ denoteMod p a = denoteMod p b

The existing structural equality test is exact for canonical residue lists.

theorem Hex.MvPoly.Kernel.ofResidues_toList_canonical (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (a : MvPoly n (ZMod64 p) cmp) : CanonicalMod p n (ofResidues p (toList a))

A producer polynomial quotes to a canonical residue list.

@[simp]

theorem Hex.MvPoly.Kernel.denoteMod_ofResidues (p : Nat) [ZMod64.Bounds p] {n : Nat} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (a : MvPoly n (ZMod64 p) cmp) : denoteMod p (ofResidues p (toList a)) = a

The complete producer-to-kernel encoding round trip.