Documentation

MIPRE.Foundations.LowDegree.BinaryPrimePowerTrace

Exact degree of the odd-prime Shoup trace #

source
def MIPRE.LowDegree.BinaryPrimePowerTrace.traceElement {E : Type u_1} [CommRing E] (β : E) (m r : ℕ) :
E

The Frobenius trace used by Shoup's prime-power construction.

Equations
Instances For
    source
    theorem MIPRE.LowDegree.BinaryPrimePowerTrace.traceElement_not_mem_range {L : Type u_1} {E : Type u_2} [Field L] [Field E] [Algebra L E] (β : E) (w : L) (m r q : ℕ) (hm : 0 < m) (hq : 1 < q) (hw : (algebraMap L E) w = β ^ q) (hinj : Function.Injective fun (i : Fin m) => 2 ^ (r * ↑i) % q) (hdeg : q ≤ (minpoly L β).natDegree) :
    traceElement β m r ∉ (algebraMap L E).range

    Reducing the trace exponents modulo q yields a nonzero polynomial of degree less than q; hence the trace cannot belong to the q-th-power root field.

    source
    theorem MIPRE.LowDegree.BinaryPrimePowerTrace.traceElement_closed {E : Type u_1} [CommRing E] [CharP E 2] (β : E) (m r : ℕ) (hβ : β ^ 2 ^ (r * m) = β) :
    traceElement β m r ^ 2 ^ r = traceElement β m r

    The trace's Frobenius orbit closes after r when the original orbit closes after m*r.

    source
    theorem MIPRE.LowDegree.BinaryPrimePowerTrace.exponent_residues_injective (m r q : ℕ) (horder : orderOf 2 = m) (hcop : r.Coprime m) :
    Function.Injective fun (i : Fin m) => 2 ^ (r * ↑i) % q

    The seed's multiplicative-order specification makes the reduced trace exponents distinct.

    source
    theorem MIPRE.LowDegree.BinaryPrimePowerTrace.traceElement_natDegree {L : Type u_1} {E : Type u_2} [Field L] [Field E] [Finite L] [Algebra L E] [Algebra (ZMod 2) E] [FiniteDimensional (ZMod 2) E] (β : E) (w : L) (m q e : ℕ) (hm : 0 < m) (hq : Nat.Prime q) (hw : (algebraMap L E) w = β ^ q) (horder : orderOf 2 = m) (hcop : q.Coprime m) (hcard : Nat.card L = 2 ^ (m * q ^ e)) (hdeg : q ≤ (minpoly L β).natDegree) (hβ : β ^ 2 ^ (q ^ (e + 1) * m) = β) :
    (minpoly (ZMod 2) (traceElement β m (q ^ (e + 1)))).natDegree = q ^ (e + 1)

    The closed Shoup trace has the full requested prime-power degree. The smaller root field is used only in this proof, never as an executable representation.

    source
    theorem MIPRE.LowDegree.BinaryPrimePowerTrace.traceElement_natDegree_of_root_degrees {E : Type u_1} [Field E] [Finite E] [Algebra (ZMod 2) E] [FiniteDimensional (ZMod 2) E] (β : E) (m q e : ℕ) (hm : 0 < m) (hq : Nat.Prime q) (horder : orderOf 2 = m) (hcop : q.Coprime m) (hprim : (ZMod 2)⟮β⟯ = ⊤) (hβ : (minpoly (ZMod 2) β).natDegree = m * q ^ (e + 1)) (hβq : (minpoly (ZMod 2) (β ^ q)).natDegree = m * q ^ e) :
    (minpoly (ZMod 2) (traceElement β m (q ^ (e + 1)))).natDegree = q ^ (e + 1)

    The intermediate-field premises follow from the two exact root degrees. This form applies directly to the flat Kummer quotient.

    source
    theorem MIPRE.LowDegree.BinaryPrimePowerTrace.flat_trace_natDegree (f : Polynomial (ZMod 2)) (hf : f.Monic) (hi : Irreducible f) (q e : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hn : ∀ (b : AdjoinRoot f), b ^ q ≠ AdjoinRoot.root f) (horder : orderOf 2 = f.natDegree) (hcop : q.Coprime f.natDegree) :
    (minpoly (ZMod 2) (traceElement (AdjoinRoot.root (f.comp (Polynomial.X ^ q ^ (e + 1)))) f.natDegree (q ^ (e + 1)))).natDegree = q ^ (e + 1)

    The trace in the explicitly specified flat odd-prime-power quotient has exactly the requested prime-power degree over the binary field.