def Hex.FpPoly.composeModMonicList {p : Nat} [ZMod64.Bounds p] (g modulus : FpPoly p) (hmonic : DensePoly.Monic modulus) : List (ZMod64 p) → FpPoly p

List-level Horner form of modular composition, reading coefficients from low to high degree and preserving the acc * g + C c step orientation. The body of the composeModMonic specification.

Equations

• g.composeModMonicList modulus hmonic [] = 0
• g.composeModMonicList modulus hmonic (c :: cs) = modulus.modByMonic (g.composeModMonicList modulus hmonic cs * g + Hex.FpPoly.C c) hmonic

noncomputable def Hex.FpPoly.composeModMonic {p : Nat} [ZMod64.Bounds p] (f g modulus : FpPoly p) (hmonic : DensePoly.Monic modulus) : FpPoly p

Horner-style modular composition in the quotient F_p[x] / (modulus).

The reduction after each multiplication keeps the intermediate polynomials bounded by the modulus degree while preserving the same result as composing first and reducing once at the end.

Kernel-facing specification: one cons walk of the coefficient list. Compiled code uses the value-equal downward Array.foldr loop below through @[csimp].

Equations

• f.composeModMonic g modulus hmonic = g.composeModMonicList modulus hmonic (Hex.DensePoly.toList f)

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

Runtime implementation of composeModMonic: a downward Array.foldr Horner loop (value-equal to composeModMonic by composeModMonic_eq_impl, registered @[csimp]).

Equations

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

theorem Hex.FpPoly.composeModMonic_eq_composeModMonicImpl {p : Nat} [ZMod64.Bounds p] (f g modulus : FpPoly p) (hmonic : DensePoly.Monic modulus) : f.composeModMonic g modulus hmonic = f.composeModMonicImpl g modulus hmonic

The reference composeModMonic and the Array.foldr runtime loop compute the same polynomial.

@[csimp]

theorem Hex.FpPoly.composeModMonic_eq_impl : @composeModMonic = @composeModMonicImpl

Register the Array.foldr loop as the compiled implementation of composeModMonic.

@[simp]

theorem Hex.FpPoly.composeModMonic_zero {p : Nat} [ZMod64.Bounds p] (g modulus : FpPoly p) (hmonic : DensePoly.Monic modulus) : composeModMonic 0 g modulus hmonic = 0

Modular composition of the zero polynomial is 0.

@[simp]

theorem Hex.FpPoly.composeModMonic_C {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) (g modulus : FpPoly p) (hmonic : DensePoly.Monic modulus) : (C c).composeModMonic g modulus hmonic = modulus.modByMonic (C c) hmonic

Modular composition of a constant C c reduces C c modulo the monic modulus.

theorem Hex.FpPoly.composeModMonic_eq_modByMonic_compose {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g modulus : FpPoly p) (hmonic : DensePoly.Monic modulus) : f.composeModMonic g modulus hmonic = modulus.modByMonic (DensePoly.compose f g) hmonic

Executable modular composition agrees with ordinary dense-polynomial composition followed by one reduction modulo the monic modulus.

theorem Hex.FpPoly.modByMonic_compose_eq_composeModMonic {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g modulus : FpPoly p) (hmonic : DensePoly.Monic modulus) : modulus.modByMonic (DensePoly.compose f g) hmonic = f.composeModMonic g modulus hmonic

The converse rewrite direction for composeModMonic_eq_modByMonic_compose. This is useful when a proof has already produced the reduced ordinary composition and needs to recover the executable modular-composition spelling.

theorem Hex.FpPoly.composeModMonic_eq_mod {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g modulus : FpPoly p) (hmonic : DensePoly.Monic modulus) : f.composeModMonic g modulus hmonic = DensePoly.compose f g % modulus

Executable modular composition agrees with DensePoly.compose f g % modulus, the quotient-ring spelling preferred by callers that reason with % rather than Hex.FpPoly.modByMonic.

@[simp]

theorem Hex.FpPoly.composeModMonic_mod_eq_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g modulus : FpPoly p) (hmonic : DensePoly.Monic modulus) : f.composeModMonic g modulus hmonic % modulus = f.composeModMonic g modulus hmonic

The result of composeModMonic is already reduced modulo the monic modulus.

@[simp]

theorem Hex.FpPoly.modByMonic_composeModMonic_eq_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g modulus : FpPoly p) (hmonic : DensePoly.Monic modulus) : modulus.modByMonic (f.composeModMonic g modulus hmonic) hmonic = f.composeModMonic g modulus hmonic

The modByMonic spelling of composeModMonic_mod_eq_self, useful for callers that state reduction via modByMonic rather than %.