hex

14.4. Key correctness theorems🔗

A small set of laws connects representatives to canonical reduction. The first two establish that the representation is canonical: a quotient element is exactly its reduced representative, and that representative has degree strictly below the modulus.

🔗theorem
Hex.GFqRing.repr_ofPoly {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] (f : Hex.FpPoly p) (hf : 0 < f.degree)
  (g : Hex.FpPoly p) :
  Hex.GFqRing.repr (Hex.GFqRing.ofPoly f hf g) =
    Hex.GFqRing.reduceMod f g
Hex.GFqRing.repr_ofPoly {p : Nat}
  [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (f : Hex.FpPoly p) (hf : 0 < f.degree)
  (g : Hex.FpPoly p) :
  Hex.GFqRing.repr
      (Hex.GFqRing.ofPoly f hf g) =
    Hex.GFqRing.reduceMod f g

The canonical representative of ofPoly f hf g is reduceMod f g.

🔗theorem
Hex.GFqRing.degree_repr_lt_degree {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree}
  (x : Hex.GFqRing.PolyQuotient f hf) :
  (Hex.GFqRing.repr x).degree < f.degree
Hex.GFqRing.degree_repr_lt_degree
  {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  (x : Hex.GFqRing.PolyQuotient f hf) :
  (Hex.GFqRing.repr x).degree < f.degree

Canonical representatives have degree strictly below the modulus.

Reduction is idempotent, so calling reduceMod on something already reduced is a no-op, and the modulus reduces to zero:

🔗theorem
Hex.GFqRing.reduceMod_idem {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] (f g : Hex.FpPoly p) :
  Hex.GFqRing.reduceMod f (Hex.GFqRing.reduceMod f g) =
    Hex.GFqRing.reduceMod f g
Hex.GFqRing.reduceMod_idem {p : Nat}
  [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (f g : Hex.FpPoly p) :
  Hex.GFqRing.reduceMod f
      (Hex.GFqRing.reduceMod f g) =
    Hex.GFqRing.reduceMod f g

Reducing a representative a second time is a no-op: reduceMod is idempotent.

🔗theorem
Hex.GFqRing.reduceMod_self {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] (f : Hex.FpPoly p) :
  Hex.GFqRing.reduceMod f f = 0
Hex.GFqRing.reduceMod_self {p : Nat}
  [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (f : Hex.FpPoly p) :
  Hex.GFqRing.reduceMod f f = 0

The modulus itself reduces to the zero representative modulo itself.

Reduction commutes with addition and multiplication in the strong sense that reducing either operand before combining does not change the final canonical representative. These laws justify lifting addition and multiplication to the quotient.

🔗theorem
Hex.GFqRing.reduceMod_add_reduceMod_congr {p : Nat}
  [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p]
  (f a b : Hex.FpPoly p) :
  Hex.GFqRing.reduceMod f (a + b) =
    Hex.GFqRing.reduceMod f
      (Hex.GFqRing.reduceMod f a + Hex.GFqRing.reduceMod f b)
Hex.GFqRing.reduceMod_add_reduceMod_congr
  {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (f a b : Hex.FpPoly p) :
  Hex.GFqRing.reduceMod f (a + b) =
    Hex.GFqRing.reduceMod f
      (Hex.GFqRing.reduceMod f a +
        Hex.GFqRing.reduceMod f b)

Reducing both summands before quotient reduction preserves the canonical representative.

🔗theorem
Hex.GFqRing.reduceMod_mul_reduceMod_congr {p : Nat}
  [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p]
  (f a b : Hex.FpPoly p) :
  Hex.GFqRing.reduceMod f (a * b) =
    Hex.GFqRing.reduceMod f
      (Hex.GFqRing.reduceMod f a * Hex.GFqRing.reduceMod f b)
Hex.GFqRing.reduceMod_mul_reduceMod_congr
  {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (f a b : Hex.FpPoly p) :
  Hex.GFqRing.reduceMod f (a * b) =
    Hex.GFqRing.reduceMod f
      (Hex.GFqRing.reduceMod f a *
        Hex.GFqRing.reduceMod f b)

Reducing both factors before quotient reduction preserves the canonical representative.

The full ring axioms over canonical representatives are bundled into the Lean.Grind.CommRing instance on Hex.GFqRing.PolyQuotient, which is the entry point for downstream proof automation.