17.3. Generic constructors🔗

The headline type is Hex.GFq: given an explicit Hex.Conway.SupportedEntry p n, it is the HexGFqField finite field over the committed Conway modulus, with the positive-degree, primality, and irreducibility hypotheses discharged from the entry. Its ergonomic sibling Hex.GFqC is the same field with the entry resolved by Hex.Conway.CommittedEntry synthesis, so GFqC 2 3 denotes GF(8) with no further arguments.

Each field element is a polynomial over F_p of degree below n: the remainder of an FpPoly modulo the field's Conway polynomial. repr returns that remainder. The generic constructor reduces an arbitrary FpPoly to it:

def

Hex.GFq.ofPoly {p n : ℕ} [Hex.ZMod64.Bounds p]
  (h : Hex.Conway.SupportedEntry p n) (g : Hex.FpPoly p) : Hex.GFq p n h
Hex.GFq.ofPoly {p n : ℕ}
  [Hex.ZMod64.Bounds p]
  (h : Hex.Conway.SupportedEntry p n)
  (g : Hex.FpPoly p) : Hex.GFq p n h

Reduce a polynomial into the canonical field selected by a committed Conway entry.

The committed-entry constructor delegates to it, resolving the witness from the ambient instance:

def

Hex.GFqC.ofPoly {p n : ℕ} [Hex.ZMod64.Bounds p]
  [h : Hex.Conway.CommittedEntry p n] (g : Hex.FpPoly p) : Hex.GFqC p n
Hex.GFqC.ofPoly {p n : ℕ}
  [Hex.ZMod64.Bounds p]
  [h : Hex.Conway.CommittedEntry p n]
  (g : Hex.FpPoly p) : Hex.GFqC p n

Reduce a polynomial into the committed GFqC p n field.

A family of *_eq_gfq lemmas characterises the GFqC spelling against the explicit GFq one, so a proof may always unfold the convenience spelling back to the entry-explicit form. The modulus delegation is representative:

theorem

Hex.GFqC.modulus_eq_gfq {p n : ℕ} [Hex.ZMod64.Bounds p]
  [h : Hex.Conway.CommittedEntry p n] :
  Hex.GFqC.modulus = Hex.GFq.modulus Hex.GFqC.entry
Hex.GFqC.modulus_eq_gfq {p n : ℕ}
  [Hex.ZMod64.Bounds p]
  [h : Hex.Conway.CommittedEntry p n] :
  Hex.GFqC.modulus =
    Hex.GFq.modulus Hex.GFqC.entry

GFqC.modulus delegates to the explicit-entry GFq.modulus.

Both families provide the full executable field API: repr, the ring and field operations, and the Frobenius endomorphism a ↦ aᵖ as the p-th power map.

def

Hex.GFq.frob {p n : ℕ} [Hex.ZMod64.Bounds p]
  {h : Hex.Conway.SupportedEntry p n} (x : Hex.GFq p n h) :
  Hex.GFq p n h
Hex.GFq.frob {p n : ℕ}
  [Hex.ZMod64.Bounds p]
  {h : Hex.Conway.SupportedEntry p n}
  (x : Hex.GFq p n h) : Hex.GFq p n h

The Frobenius endomorphism on the canonical Conway-backed field, computed as the p-th power on the underlying quotient representation.