@[instance_reducible]

instance Hex.ZMod64.instZero_hexPolyFp {p : Nat} [Bounds p] : Zero (ZMod64 p)

Equations

• Hex.ZMod64.instZero_hexPolyFp = { zero := Hex.ZMod64.zero }

@[instance_reducible]

instance Hex.ZMod64.instOne_hexPolyFp {p : Nat} [Bounds p] : One (ZMod64 p)

Equations

• Hex.ZMod64.instOne_hexPolyFp = { one := Hex.ZMod64.one }

@[instance_reducible]

instance Hex.ZMod64.instAdd_hexPolyFp {p : Nat} [Bounds p] : Add (ZMod64 p)

Equations

• Hex.ZMod64.instAdd_hexPolyFp = { add := Hex.ZMod64.add }

@[instance_reducible]

instance Hex.ZMod64.instSub_hexPolyFp {p : Nat} [Bounds p] : Sub (ZMod64 p)

Equations

• Hex.ZMod64.instSub_hexPolyFp = { sub := Hex.ZMod64.sub }

@[instance_reducible]

instance Hex.ZMod64.instMul_hexPolyFp {p : Nat} [Bounds p] : Mul (ZMod64 p)

Equations

• Hex.ZMod64.instMul_hexPolyFp = { mul := Hex.ZMod64.mul }

@[instance_reducible]

instance Hex.ZMod64.instDiv_hexPolyFp {p : Nat} [Bounds p] : Div (ZMod64 p)

Equations

• Hex.ZMod64.instDiv_hexPolyFp = { div := fun (a b : Hex.ZMod64 p) => a.mul b.inv }

instance Hex.ZMod64.instAddZeroLaw_hexPolyFp {p : Nat} [Bounds p] : DensePoly.AddZeroLaw (ZMod64 p)

instance Hex.ZMod64.instSubZeroLaw_hexPolyFp {p : Nat} [Bounds p] : DensePoly.SubZeroLaw (ZMod64 p)

instance Hex.ZMod64.instZeroSubNegLaw_hexPolyFp {p : Nat} [Bounds p] : DensePoly.ZeroSubNegLaw (ZMod64 p)

theorem Hex.ZMod64.coeff_mul_at_top {p : Nat} [Bounds p] (f g : DensePoly (ZMod64 p)) (hf : 0 < f.size) (hg : 0 < g.size) : (f * g).coeff (f.size - 1 + (g.size - 1)) = f.coeff (f.size - 1) * g.coeff (g.size - 1)

The top coefficient of a product of nonzero ZMod64-valued polynomials is the product of the leading coefficients.

theorem Hex.ZMod64.zmod_div_one {p : Nat} [Bounds p] [PrimeModulus p] (a : ZMod64 p) : a / 1 = a

Division by 1 is the identity on ZMod64 p. Callers normalizing a value against a unit denominator (for example a leading coefficient already equal to 1) can discharge the division outright.

instance Hex.ZMod64.instDivModLawsZMod64Fp (p : Nat) [Bounds p] [PrimeModulus p] : DensePoly.DivModLaws (ZMod64 p)

The F_p[x] division law obligations used by quotient constructions.

These are the concrete finite-field instances of the generic DensePoly.DivModLaws proof surface used by downstream quotient-ring code; the executable division operations themselves are inherited from DensePoly.

instance Hex.ZMod64.instGcdLawsZMod64Fp {p : Nat} [Bounds p] [PrimeModulus p] : DensePoly.GcdLaws (ZMod64 p)

The F_p[x] gcd law obligations used by finite-field inverse construction.

@[reducible, inline]

abbrev Hex.FpPoly (p : Nat) [ZMod64.Bounds p] : Type

Executable dense polynomials over the prime-field candidate ZMod64 p.

Equations

• Hex.FpPoly p = Hex.DensePoly (Hex.ZMod64 p)

def Hex.FpPoly.modCached {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : FpPoly p

Finite-field remainder with the divisor's coefficient inverse computed once for the whole long-division pass.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.FpPoly.modCached_eq {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : f.modCached g = DensePoly.mod f g

Caching the divisor-leading inverse leaves the executable remainder unchanged. This equality is definitional for the ZMod64 division instance and does not require primality of the modulus.

def Hex.FpPoly.gcdAuxCached {p : Nat} [ZMod64.Bounds p] (r₀ r₁ : FpPoly p) (fuel : Nat) : FpPoly p

Euclidean GCD with one coefficient inverse per division rather than one per eliminated coefficient.

Equations

• r₀.gcdAuxCached r₁ 0 = r₀
• r₀.gcdAuxCached r₁ fuel_2.succ = if Hex.DensePoly.isZero r₁ = true then r₀ else r₁.gcdAuxCached (r₀.modCached r₁) fuel_2

theorem Hex.FpPoly.gcdAuxCached_eq {p : Nat} [ZMod64.Bounds p] (r₀ r₁ : FpPoly p) (fuel : Nat) : r₀.gcdAuxCached r₁ fuel = DensePoly.gcdAux r₀ r₁ fuel

The inverse-cached loop computes the reference Euclidean remainder sequence exactly, including its unnormalised representative.

def Hex.FpPoly.gcdCached {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : FpPoly p

Inverse-cached finite-field polynomial GCD.

Equations

• f.gcdCached g = f.gcdAuxCached g (Hex.DensePoly.size f + Hex.DensePoly.size g + 1)

theorem Hex.FpPoly.gcdCached_eq {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : f.gcdCached g = DensePoly.gcd f g

The inverse-cached finite-field GCD returns the exact reference representative.