HexPolyFp.Frobenius

@[irreducible]

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

Exponentiation by squaring in the quotient F_p[x] / (f), reducing after every multiplication with the executable DensePoly.modByMonic routine.

Equations

f.powModMonicAux hmonic 0 x✝¹ x✝ = x✝
f.powModMonicAux hmonic n.succ x✝¹ x✝ = f.powModMonicAux hmonic ((n + 1) / 2) (f.modByMonic (x✝¹ * x✝¹) hmonic) (if (n + 1) % 2 = 0 then x✝ else f.modByMonic (x✝ * x✝¹) hmonic)

Instances For

source

def Hex.FpPoly.powModMonic {p : Nat} [ZMod64.Bounds p] (base f : FpPoly p) (hmonic : DensePoly.Monic f) (n : Nat) :

FpPoly p

Compute base^n mod f for monic f.

Equations

base.powModMonic f hmonic n = f.powModMonicAux hmonic n (f.modByMonic base hmonic) 1

Instances For

source

def Hex.FpPoly.powFastCutoff :

Nat

Modulus-size boundary for compiled fast-multiplication modular powers. Below this size the reduced operands stay in the schoolbook kernel range, so the retained loop also avoids repeated dispatcher checks.

Equations

Hex.FpPoly.powFastCutoff = 18

Instances For

source

@[irreducible]

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

Nat → FpPoly p → FpPoly p → FpPoly p

Compiled square-and-multiply loop using the coefficient-owner dispatcher.

Equations

One or more equations did not get rendered due to their size.
f.powModMonicFastAux hmonic 0 x✝¹ x✝ = x✝

Instances For

source

@[inline]

def Hex.FpPoly.powModMonicImpl {p : Nat} [ZMod64.Bounds p] (base f : FpPoly p) (hmonic : DensePoly.Monic f) (n : Nat) :

FpPoly p

Compiled modular-power dispatcher. Tiny moduli retain the reference loop; larger moduli use mulPackedFast while retaining ordinary monic reduction.

Equations

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

Instances For

source

@[csimp]

theorem Hex.FpPoly.powModMonic_eq_impl :

@powModMonic = @powModMonicImpl

source

@[simp]

theorem Hex.FpPoly.powModMonic_zero {p : Nat} [ZMod64.Bounds p] (base f : FpPoly p) (hmonic : DensePoly.Monic f) :

base.powModMonic f hmonic 0 = 1

The zeroth modular power is 1.

source

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

Nat → FpPoly p

Structurally recursive modular exponentiation. This is intentionally linear in the exponent: unlike powModMonic, it reduces by kernel computation on small closed terms.

Equations

base.powModMonicLinear f hmonic 0 = 1
base.powModMonicLinear f hmonic n.succ = f.modByMonic (base.powModMonicLinear f hmonic n * base) hmonic

Instances For

source

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

FpPoly p

Compute X^p mod f, the basic Frobenius generator used downstream.

Equations

f.frobeniusXMod hmonic = Hex.FpPoly.X.powModMonic f hmonic p

Instances For

source

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

FpPoly p

Kernel-reducible variant of frobeniusXMod for small closed terms.

Equations

f.frobeniusXModLinear hmonic = Hex.FpPoly.X.powModMonicLinear f hmonic p

Instances For

source

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

FpPoly p

Compute X^(p^k) mod f for arbitrary k.

Equations

f.frobeniusXPowMod hmonic k = Hex.FpPoly.X.powModMonic f hmonic (p ^ k)

Instances For

source

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

FpPoly p

Kernel-reducible variant of frobeniusXPowMod for small closed terms.

Equations

f.frobeniusXPowModLinear hmonic k = Hex.FpPoly.X.powModMonicLinear f hmonic (p ^ k)

Instances For

source

@[simp]

theorem Hex.FpPoly.frobeniusXPowMod_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) :

f.frobeniusXPowMod hmonic 0 = f.modByMonic X hmonic

The zeroth Frobenius power is the canonical representative of X modulo f.

source

theorem Hex.FpPoly.linearPow_mod_eq_of_mod_eq_mod {p : Nat} [ZMod64.Bounds p] (f h r : FpPoly p) (n : Nat) [ZMod64.PrimeModulus p] (hmod : h % f = r % f) :

h.linearPow n % f = r.linearPow n % f

linearPow has the same canonical remainder for bases with the same canonical remainder.

source

theorem Hex.FpPoly.powModMonic_pos_self_mod {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (base f : FpPoly p) (hmonic : DensePoly.Monic f) (n : Nat) (hn : 0 < n) :

base.powModMonic f hmonic n % f = base.powModMonic f hmonic n

For a positive exponent, powModMonic returns an already-reduced value.

source

@[simp]

theorem Hex.FpPoly.modByMonic_powModMonic_pos_eq_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (base f : FpPoly p) (hmonic : DensePoly.Monic f) (n : Nat) (hn : 0 < n) :

f.modByMonic (base.powModMonic f hmonic n) hmonic = base.powModMonic f hmonic n

The modByMonic spelling of powModMonic_pos_self_mod, useful for callers working entirely with the executable monic-reduction API.

source

theorem Hex.FpPoly.powModMonic_mod_eq_linearPow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (base f : FpPoly p) (hmonic : DensePoly.Monic f) (n : Nat) :

base.powModMonic f hmonic n % f = base.linearPow n % f

powModMonic computes the same residue as linearPow.

source

theorem Hex.FpPoly.powModMonicLinear_eq_powModMonic {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (base f : FpPoly p) (hmonic : DensePoly.Monic f) (n : Nat) :

base.powModMonicLinear f hmonic n = base.powModMonic f hmonic n

The kernel-reducible linear exponentiation path agrees with the production square-and-multiply implementation. It is intentionally not a global simp rule: some conformance proofs unfold the linear evaluator to get kernel-reduced closed terms.

source

theorem Hex.FpPoly.frobeniusXModLinear_eq_frobeniusXMod {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) :

f.frobeniusXModLinear hmonic = f.frobeniusXMod hmonic

The kernel-reducible X^p mod f evaluator agrees with the production Frobenius generator.

source

theorem Hex.FpPoly.frobeniusXPowModLinear_eq_frobeniusXPowMod {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (k : Nat) :

f.frobeniusXPowModLinear hmonic k = f.frobeniusXPowMod hmonic k

The kernel-reducible X^(p^k) mod f evaluator agrees with the production Frobenius power routine.

source

theorem Hex.FpPoly.frobeniusXMod_eq_frobeniusXPowMod_one {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) :

f.frobeniusXMod hmonic = f.frobeniusXPowMod hmonic 1

The basic Frobenius generator is the first indexed Frobenius power.

source

@[simp]

theorem Hex.FpPoly.frobeniusXMod_mod_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) :

f.frobeniusXMod hmonic % f = f.frobeniusXMod hmonic

frobeniusXMod outputs an already-reduced polynomial.

source

@[simp]

theorem Hex.FpPoly.modByMonic_frobeniusXMod_eq_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) :

f.modByMonic (f.frobeniusXMod hmonic) hmonic = f.frobeniusXMod hmonic

The modByMonic spelling of frobeniusXMod_mod_self.

source

theorem Hex.FpPoly.frobeniusXPowMod_succ {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (k : Nat) :

f.frobeniusXPowMod hmonic (k + 1) = (f.frobeniusXPowMod hmonic k).powModMonic f hmonic p

Successor step for frobeniusXPowMod: raising the previous Frobenius image to the p-th power (mod f) advances the index by one.

source

theorem Hex.FpPoly.frobeniusXPowMod_mod_eq_monomial_mod {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (k : Nat) :

f.frobeniusXPowMod hmonic k % f = DensePoly.monomial (p ^ k) 1 % f

frobeniusXPowMod f hmonic k reduces modulo f to the absolute monomial X^(p^k) reduced modulo f. This is the key identity relating the executable Frobenius computation to the absolute polynomial it represents.

source

@[simp]

theorem Hex.FpPoly.frobeniusXPowMod_mod_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (k : Nat) :

f.frobeniusXPowMod hmonic k % f = f.frobeniusXPowMod hmonic k

frobeniusXPowMod outputs an already-reduced polynomial.

source

@[simp]

theorem Hex.FpPoly.modByMonic_frobeniusXPowMod_eq_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (k : Nat) :

f.modByMonic (f.frobeniusXPowMod hmonic k) hmonic = f.frobeniusXPowMod hmonic k

The modByMonic spelling of frobeniusXPowMod_mod_self.