structure Hex.Conway.SupportedEntry (p n : Nat) [ZMod64.Bounds p] : Type

A lookup witness for a committed polynomial.

• poly : FpPoly p

  The selected polynomial.

• prime : Nat.Prime p

  Its characteristic is prime.

• isSupported : luebeckConwayPolynomial? p n = some self.poly

  The table selects this polynomial.

def Hex.Conway.conwayPoly (p n : Nat) [ZMod64.Bounds p] (h : SupportedEntry p n) : FpPoly p

Recover the committed Conway modulus for a supported entry.

Equations

• Hex.Conway.conwayPoly p n h = h.poly

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_conwayPoly {p n : Nat} [ZMod64.Bounds p] (h : SupportedEntry p n) : luebeckConwayPolynomial? p n = some (conwayPoly p n h)

A SupportedEntry packages the lookup hit for the committed Tier 1 Conway table entry selected by conwayPoly.

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_degree_pos {p n : Nat} [ZMod64.Bounds p] {f : FpPoly p} (h : luebeckConwayPolynomial? p n = some f) : 0 < f.degree

Every committed Tier 1 Conway entry in the current table is nonconstant.

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_degree_eq {p n : Nat} [ZMod64.Bounds p] {f : FpPoly p} (h : luebeckConwayPolynomial? p n = some f) : f.degree = n

Every committed Tier 1 Conway entry has the degree requested by its lookup key.

@[simp]

theorem Hex.Conway.conwayPoly_nonconstant (p n : Nat) [ZMod64.Bounds p] (h : SupportedEntry p n) : 0 < (conwayPoly p n h).degree

Supported Conway entries produce nonconstant moduli.

theorem Hex.Conway.conwayPoly_irreducible (p n : Nat) [ZMod64.Bounds p] (h : SupportedEntry p n) : (conwayPoly p n h).Irreducible

Supported Conway entries carry the imported irreducibility witness.

@[simp]

theorem Hex.Conway.conwayPoly_monic (p n : Nat) [ZMod64.Bounds p] (h : SupportedEntry p n) : DensePoly.Monic (conwayPoly p n h)

Supported Conway entries carry the imported monicity witness.