instance Hex.GFqField.Example.boundsFive : ZMod64.Bounds 5

Word bounds for the example characteristic.

theorem Hex.GFqField.Example.prime_five : Nat.Prime 5

The example characteristic is prime.

instance Hex.GFqField.Example.instPrimeModulusOfNatNat_hexGFqField : ZMod64.PrimeModulus 5

def Hex.GFqField.Example.modulus : FpPoly 5

A monic degree-four modulus x⁴ + 2 over 𝔽₅, committed with its irreducibility certificate so that a small GF(5⁴) is available without hand-writing one. Used by the manual's worked examples and by conformance.

Equations

• Hex.GFqField.Example.modulus = Hex.DensePoly.ofCoeffs #[2, 0, 0, 0, 1]

theorem Hex.GFqField.Example.modulus_pos_degree : 0 < modulus.degree

The example modulus is nonconstant, which is what the field wrapper needs beside irreducibility.

theorem Hex.GFqField.Example.modulus_monic : DensePoly.Monic modulus

The example modulus is monic.

def Hex.GFqField.Example.cert : Berlekamp.IrreducibilityCertificate

Rabin irreducibility certificate for the example modulus: the Frobenius pow chain and the Bézout witness the kernel replays.

Equations

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

theorem Hex.GFqField.Example.cert_check : Berlekamp.checkIrreducibilityCertificateLinear modulus modulus_monic cert = true

The committed certificate passes the kernel-reducible checker. The heartbeat and recursion bumps live here rather than at every call site: replaying a certificate is the expensive step, and doing it once means downstream users of modulus_irreducible pay nothing.

theorem Hex.GFqField.Example.modulus_irreducible : modulus.Irreducible

The example modulus is irreducible, by routing the checked certificate through Rabin soundness.

@[reducible, inline]

abbrev Hex.GFqField.Example.F : Type

The example field GF(5⁴).

Equations

• Hex.GFqField.Example.F = Hex.GFqField.FiniteField Hex.GFqField.Example.modulus Hex.GFqField.Example.modulus_pos_degree Hex.GFqField.Example.prime_five Hex.GFqField.Example.modulus_irreducible

def Hex.GFqField.Example.ofPoly (f : FpPoly 5) : F

Inject a polynomial into the example field by reducing it.

Equations

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