def Hex.Conway.frobeniusBase {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) : FpPoly p

x ^ p reduced modulo a monic f, computed by the structurally recursive binary modular exponentiation so the kernel can replay it in logarithmically many modular multiplications.

Equations

• Hex.Conway.frobeniusBase f hmonic = Hex.Conway.powMod Hex.FpPoly.X f hmonic p

def Hex.Conway.frobeniusIter {p : Nat} [ZMod64.Bounds p] (f xp : FpPoly p) (hmonic : DensePoly.Monic f) : Nat → FpPoly p → FpPoly p

Apply the Frobenius g ↦ g ^ p to a residue k times, as k modular compositions with xp = x ^ p mod f.

Composition rather than exponentiation is the point: g(x) ^ p = g(x ^ p) in characteristic p, so one Frobenius step costs a Horner walk over g's coefficients instead of p modular multiplications.

Equations

• Hex.Conway.frobeniusIter f xp hmonic 0 x✝ = x✝
• Hex.Conway.frobeniusIter f xp hmonic k.succ x✝ = Hex.Conway.frobeniusIter f xp hmonic k (Hex.Conway.compose x✝ xp f hmonic)

def Hex.Conway.normAux {p : Nat} [ZMod64.Bounds p] (f xp : FpPoly p) (hmonic : DensePoly.Monic f) (m : Nat) : Nat → FpPoly p → FpPoly p → FpPoly p

The norm accumulator: multiply together k successive p^m-th powers of the residue of x, reducing modulo f at each step.

cur is α ^ (p ^ (i m)) on entry to the i-th step, and advances by m Frobenius applications.

Equations

• Hex.Conway.normAux f xp hmonic m 0 x✝¹ x✝ = x✝¹
• Hex.Conway.normAux f xp hmonic m k.succ x✝¹ x✝ = Hex.Conway.normAux f xp hmonic m k (f.modByMonic (x✝¹ * x✝) hmonic) (Hex.Conway.frobeniusIter f xp hmonic m x✝)

def Hex.Conway.normX {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (m k : Nat) : FpPoly p

The norm N_{F_{p^n} / F_{p^m}}(α) of the residue α of x, as a reduced representative modulo f.

f is the degree-n modulus and m divides n; k = n / m is passed explicitly so that the recursion is structural.

Equations

• Hex.Conway.normX f hmonic m k = Hex.Conway.normAux f (Hex.Conway.frobeniusBase f hmonic) hmonic m k 1 Hex.FpPoly.X

def Hex.Conway.normExponent (q : Nat) : Nat → Nat

The exponent 1 + q + ⋯ + q^(k-1), in a structural-recursion spelling that follows the norm accumulator.

Equations

• Hex.Conway.normExponent q 0 = 0
• Hex.Conway.normExponent q k.succ = 1 + q * Hex.Conway.normExponent q k

theorem Hex.Conway.reduce_frobeniusBase_eq_pow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hmonic : DensePoly.Monic f} {hf_pos : 0 < DensePoly.natDegree f} : FpPoly.Quotient.reduce (frobeniusBase f hmonic) = FpPoly.Quotient.X ^ p

The executable Frobenius base represents the p-th power of the quotient indeterminate.

theorem Hex.Conway.reduce_frobeniusIter_eq_pow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f xp : FpPoly p} {hmonic : DensePoly.Monic f} {hf_pos : 0 < DensePoly.natDegree f} (hxp : FpPoly.Quotient.reduce xp = FpPoly.Quotient.X ^ p) (k : Nat) (a : FpPoly p) : FpPoly.Quotient.reduce (frobeniusIter f xp hmonic k a) = FpPoly.Quotient.reduce a ^ p ^ k

Iterating executable modular composition k times represents raising a quotient element to p^k.

theorem Hex.Conway.reduce_normAux_eq_pow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hmonic : DensePoly.Monic f} {hf_pos : 0 < DensePoly.natDegree f} (m k : Nat) (acc cur : FpPoly p) : FpPoly.Quotient.reduce (normAux f (frobeniusBase f hmonic) hmonic m k acc cur) = FpPoly.Quotient.reduce acc * FpPoly.Quotient.reduce cur ^ normExponent (p ^ m) k

The norm accumulator represents its initial accumulator multiplied by the geometric sequence of Frobenius powers of its initial current value.

theorem Hex.Conway.normX_eq_pow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hmonic : DensePoly.Monic f} {hf_pos : 0 < DensePoly.natDegree f} (m k : Nat) : FpPoly.Quotient.reduce (normX f hmonic m k) = FpPoly.Quotient.X ^ normExponent (p ^ m) k

The quotient class of normX is the geometric-sum power of the quotient indeterminate.

theorem Hex.Conway.normExponent_eq_div {q : Nat} (hq : 1 < q) (k : Nat) : normExponent q k = (q ^ k - 1) / (q - 1)

The structural geometric exponent is the usual geometric-series quotient.

def Hex.Conway.compatCheck {p : Nat} [ZMod64.Bounds p] (fm fn : FpPoly p) (hmonic : DensePoly.Monic fn) (m k : Nat) : Bool

The Tier 2 compatibility check for a committed pair of entries: is the norm of α down to the degree-m subfield a root of C(p, m)?

fm is the smaller modulus, fn the larger, and k = n / m. Evaluating fm at the norm is exactly a modular composition.

Equations

• Hex.Conway.compatCheck fm fn hmonic m k = (Hex.Conway.compose fm (Hex.Conway.normX fn hmonic m k) fn hmonic == 0)

@[reducible, inline]

abbrev Hex.Conway.Compatible (p m n : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (hm : SupportedEntry p m) (hn : SupportedEntry p n) : Prop

Compatibility of two committed Conway entries across the subfield lattice.

Compatible p m n says that the residue of x in F_p[x] / (C(p, n)), raised to the power (p^n - 1) / (p^m - 1), is a root of C(p, m). Phrased through Hex.Conway.compatCheck, which computes that power as a product of Frobenius images rather than as a modular exponentiation, so the statement is decide-able for the committed entries.

The hypothesis m ∣ n is carried rather than derived: the quotient n / m is what the check recurses on, and outside the divisor case it would not be the right number of factors.

Equations

• Hex.Conway.Compatible p m n hm hn = (Hex.Conway.compatCheck (Hex.Conway.conwayPoly p m hm) (Hex.Conway.conwayPoly p n hn) ⋯ m (n / m) = true)

theorem Hex.Conway.conwayPoly_degree_pos (p n : Nat) [ZMod64.Bounds p] (hn : SupportedEntry p n) : 0 < DensePoly.natDegree (conwayPoly p n hn)

The committed modulus has positive degree, in the degree?.getD spelling the quotient type is indexed by. conwayPoly_nonconstant says the same thing through FpPoly.degree; the two are definitionally equal, but instance search on Quotient wants this shape.

def Hex.Conway.subfieldGen (p m n : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (hn : SupportedEntry p n) : (conwayPoly p n hn).Quotient ⋯ ⋯

The generator of the canonical degree-m subfield of F_p[x] / (C(p, n)), as an element of the quotient rather than as a representative: the class of the norm of x.

Equations

• Hex.Conway.subfieldGen p m n hn = Hex.FpPoly.Quotient.reduce (Hex.Conway.normX (Hex.Conway.conwayPoly p n hn) ⋯ m (n / m))

theorem Hex.Conway.subfieldGen_eq_norm {p m n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (hn : SupportedEntry p n) (hm_pos : 0 < m) (hmn : m ∣ n) : subfieldGen p m n hn = FpPoly.Quotient.X ^ ((p ^ n - 1) / (p ^ m - 1))

The canonical subfield generator is the field norm of the ambient Conway generator.

The positivity assumption excludes the meaningless degree-zero denominator; divisibility identifies p ^ (m * (n / m)) with p ^ n.

theorem Hex.Conway.eval_conwayPoly_subfieldGen_eq_zero {p m n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (hm : SupportedEntry p m) (hn : SupportedEntry p n) (hcompat : Compatible p m n hm hn) : FpPoly.Quotient.eval (conwayPoly p m hm) (subfieldGen p m n hn) = FpPoly.Quotient.zero

The subfield generator is a root of the smaller Conway polynomial.

This is compatibility as a statement about field elements: evaluating C(p, m) at Hex.Conway.subfieldGen in F_p[x] / (C(p, n)) gives zero. The Bool-valued Hex.Conway.Compatible is the computation; this is what the computation establishes, and it is the well-definedness input a subfield embedding needs.

theorem Hex.Conway.eval_norm_eq_zero {p m n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (hm : SupportedEntry p m) (hn : SupportedEntry p n) (hcompat : Compatible p m n hm hn) (hm_pos : 0 < m) (hmn : m ∣ n) : FpPoly.Quotient.eval (conwayPoly p m hm) (FpPoly.Quotient.X ^ ((p ^ n - 1) / (p ^ m - 1))) = FpPoly.Quotient.zero

The explicit finite-field norm power is a root of the smaller Conway polynomial.