11.5. Key correctness theorems🔗

The executable operations are pinned to their mathematical meaning. Modular composition agrees with the spelled-out "compose then take the remainder" definition, and the Frobenius iterate reduces to X^(pᵏ) mod f. That last identity is the one Rabin's irreducibility test relies on.

theorem

Hex.FpPoly.composeModMonic_eq_mod {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] (f g modulus : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic modulus) :
  f.composeModMonic g modulus hmonic =
    Hex.DensePoly.compose f g % modulus
Hex.FpPoly.composeModMonic_eq_mod
  {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (f g modulus : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic modulus) :
  f.composeModMonic g modulus hmonic =
    Hex.DensePoly.compose f g % modulus

Executable modular composition agrees with DensePoly.compose f g % modulus, the quotient-ring spelling preferred by downstream callers that reason with % rather than modByMonic.

theorem

Hex.FpPoly.frobeniusXPowMod_mod_eq_monomial_mod {p : Nat}
  [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (f : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic f) (k : Nat) :
  f.frobeniusXPowMod hmonic k % f = Hex.DensePoly.monomial (p ^ k) 1 % f
Hex.FpPoly.frobeniusXPowMod_mod_eq_monomial_mod
  {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (f : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic f)
  (k : Nat) :
  f.frobeniusXPowMod hmonic k % f =
    Hex.DensePoly.monomial (p ^ k) 1 % f

frobeniusXPowMod f hmonic k reduces modulo f to the absolute monomial X^(p^k) reduced modulo f. This is the key identity relating the executable Frobenius computation to the absolute polynomial it represents.

Square-free decomposition is correct in two senses: every emitted factor is genuinely square-free, and the unit-times-weighted-product reconstructs the original polynomial. The multiplicities are positive, so the factor list carries no padding.

theorem

Hex.FpPoly.squareFreeDecomposition_factors_squareFree {p : Nat}
  [Hex.ZMod64.Bounds p] (hp : Hex.Nat.Prime p) (f : Hex.FpPoly p) :
  have d := Hex.FpPoly.squareFreeDecomposition hp f;
  ∀ (sf : Hex.FpPoly.SquareFreeFactor p),
    sf ∈ d.factors →
      (Hex.FpPoly.normalizeMonic
            (Hex.DensePoly.gcd sf.factor
              (Hex.DensePoly.derivative sf.factor))).snd =
        1
Hex.FpPoly.squareFreeDecomposition_factors_squareFree
  {p : Nat} [Hex.ZMod64.Bounds p]
  (hp : Hex.Nat.Prime p)
  (f : Hex.FpPoly p) :
  have d :=
    Hex.FpPoly.squareFreeDecomposition hp
      f;
  ∀ (sf : Hex.FpPoly.SquareFreeFactor p),
    sf ∈ d.factors →
      (Hex.FpPoly.normalizeMonic
            (Hex.DensePoly.gcd sf.factor
              (Hex.DensePoly.derivative
                sf.factor))).snd =
        1

Public square-freeness wrapper: every factor emitted by squareFreeDecomposition is square-free, witnessed by the normalized gcd with its derivative reducing to 1. The provider instantiation is closed internally, so no provider arguments appear in the statement.

theorem

Hex.FpPoly.squareFreeDecomposition_weightedProduct {p : Nat}
  [Hex.ZMod64.Bounds p] (hp : Hex.Nat.Prime p) (f : Hex.FpPoly p) :
  have d := Hex.FpPoly.squareFreeDecomposition hp f;
  Hex.DensePoly.C d.unit * Hex.FpPoly.weightedProduct d.factors = f
Hex.FpPoly.squareFreeDecomposition_weightedProduct
  {p : Nat} [Hex.ZMod64.Bounds p]
  (hp : Hex.Nat.Prime p)
  (f : Hex.FpPoly p) :
  have d :=
    Hex.FpPoly.squareFreeDecomposition hp
      f;
  Hex.DensePoly.C d.unit *
      Hex.FpPoly.weightedProduct
        d.factors =
    f

Public reconstruction wrapper: the emitted unit and weighted factor product recover the input. The provider instantiation is closed internally, so no provider arguments appear in the statement.

theorem

Hex.FpPoly.squareFreeDecomposition_multiplicity_pos {p : Nat}
  [Hex.ZMod64.Bounds p] (hp : Hex.Nat.Prime p) (f : Hex.FpPoly p) :
  have d := Hex.FpPoly.squareFreeDecomposition hp f;
  ∀ (sf : Hex.FpPoly.SquareFreeFactor p),
    sf ∈ d.factors → 0 < sf.multiplicity
Hex.FpPoly.squareFreeDecomposition_multiplicity_pos
  {p : Nat} [Hex.ZMod64.Bounds p]
  (hp : Hex.Nat.Prime p)
  (f : Hex.FpPoly p) :
  have d :=
    Hex.FpPoly.squareFreeDecomposition hp
      f;
  ∀ (sf : Hex.FpPoly.SquareFreeFactor p),
    sf ∈ d.factors → 0 < sf.multiplicity

Every factor emitted by squareFreeDecomposition carries a strictly positive multiplicity, so no factor is recorded at multiplicity 0. A caller iterating the factor list can therefore treat each recorded exponent as a genuine power and need not special-case a zero exponent.

The field-promoting laws on the quotient are the inverse-cancellation theorems. Each carries FpPoly.Irreducible g as a hypothesis: for an irreducible modulus every nonzero quotient element has a genuine two-sided multiplicative inverse, which is exactly what fails for a reducible modulus (where a nonzero zero-divisor has no inverse).

theorem

Hex.FpPoly.Quotient.mul_inv_cancel {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] {g : Hex.FpPoly p}
  {hmonic : Hex.DensePoly.Monic g}
  {hg_pos : 0 < (Hex.DensePoly.degree? g).getD 0}
  (hg_irr : g.Irreducible) {a : g.Quotient hmonic hg_pos} (ha : a ≠ 0) :
  a * a⁻¹ = 1
Hex.FpPoly.Quotient.mul_inv_cancel
  {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  {g : Hex.FpPoly p}
  {hmonic : Hex.DensePoly.Monic g}
  {hg_pos :
    0 < (Hex.DensePoly.degree? g).getD 0}
  (hg_irr : g.Irreducible)
  {a : g.Quotient hmonic hg_pos}
  (ha : a ≠ 0) : a * a⁻¹ = 1

Multiplicative cancellation: when g is irreducible, every nonzero quotient element a satisfies a * a⁻¹ = 1. This is the field-inverse axiom that promotes Quotient g hmonic hg_pos from a commutative ring to a Field; the FpPoly.Irreducible g hypothesis is essential, since for reducible g a nonzero zero-divisor has no inverse.

theorem

Hex.FpPoly.Quotient.inv_mul_cancel {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] {g : Hex.FpPoly p}
  {hmonic : Hex.DensePoly.Monic g}
  {hg_pos : 0 < (Hex.DensePoly.degree? g).getD 0}
  (hg_irr : g.Irreducible) {a : g.Quotient hmonic hg_pos} (ha : a ≠ 0) :
  a⁻¹ * a = 1
Hex.FpPoly.Quotient.inv_mul_cancel
  {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  {g : Hex.FpPoly p}
  {hmonic : Hex.DensePoly.Monic g}
  {hg_pos :
    0 < (Hex.DensePoly.degree? g).getD 0}
  (hg_irr : g.Irreducible)
  {a : g.Quotient hmonic hg_pos}
  (ha : a ≠ 0) : a⁻¹ * a = 1

The inverse candidate also cancels on the left for nonzero quotient elements modulo an irreducible polynomial.