structure Hex.FpPoly.SquareFreeFactor (p : Nat) [ZMod64.Bounds p] : Type

One square-free factor together with its multiplicity.

• factor : FpPoly p

  The square-free factor polynomial.

• multiplicity : Nat

  The exponent with which factor divides the original polynomial.

structure Hex.FpPoly.SquareFreeDecomposition (p : Nat) [ZMod64.Bounds p] : Type

A square-free decomposition records the scalar unit and the nonconstant factors.

• unit : ZMod64 p

  The leading-coefficient scalar unit pulled out of the polynomial.

• factors : List (SquareFreeFactor p)

  The square-free factors together with their multiplicities.

def Hex.FpPoly.isOne {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : Bool

Detect the unit polynomial 1.

Equations

• f.isOne = match Hex.DensePoly.degree? f with | some 0 => if Hex.DensePoly.coeff f 0 = 1 then true else false | x => false

def Hex.FpPoly.pow {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (n : Nat) : FpPoly p

Polynomial exponentiation uses square-and-multiply on the exponent bits.

Equations

• f.pow n = Hex.FpPoly.pow.go 1 f n

@[irreducible]

def Hex.FpPoly.pow.go {p : Nat} [ZMod64.Bounds p] (acc base : FpPoly p) (k : Nat) : FpPoly p

Equations

• Hex.FpPoly.pow.go acc base k = if hk : k = 0 then acc else have acc' := if k % 2 = 1 then acc * base else acc; Hex.FpPoly.pow.go acc' (base * base) (k / 2)

def Hex.FpPoly.weightedProduct {p : Nat} [ZMod64.Bounds p] (factors : List (SquareFreeFactor p)) : FpPoly p

Multiply the factors in a square-free decomposition with their multiplicities.

Equations

• Hex.FpPoly.weightedProduct factors = List.foldl (fun (acc : Hex.FpPoly p) (sf : Hex.FpPoly.SquareFreeFactor p) => acc * sf.factor.pow sf.multiplicity) 1 factors

def Hex.FpPoly.pthRoot {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : FpPoly p

Extract the formal p-th root by keeping exactly the coefficients whose degrees are multiples of p.

Equations

• f.pthRoot = Hex.FpPoly.ofCoeffs (List.map (fun (i : Nat) => Hex.DensePoly.coeff f (i * p)) (List.range ((Hex.DensePoly.size f + p - 1) / p))).toArray

theorem Hex.FpPoly.fpPoly_leadingCoeff_ne_zero_of_isZero_false {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hzero : DensePoly.isZero f = false) : DensePoly.leadingCoeff f ≠ 0

Nonzero executable FpPoly values have nonzero leading coefficient.

The proof converts isZero = false to positive dense-polynomial size, then uses the invariant that the last stored coefficient of a positive-size dense polynomial is nonzero.

def Hex.FpPoly.normalizeMonic {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : ZMod64 p × FpPoly p

Split off the leading coefficient so the recursive Yun loop can work on a monic input.

Equations

• f.normalizeMonic = if Hex.DensePoly.isZero f = true then (0, 0) else have unit := Hex.DensePoly.leadingCoeff f; (unit, Hex.DensePoly.scale unit⁻¹ f)

@[irreducible]

def Hex.FpPoly.monicGcd {p : Nat} [ZMod64.Bounds p] (c w : FpPoly p) : FpPoly p

Monic-normalized gcd: the canonical monic associate of DensePoly.gcd c w.

Handling the Yun square-free loop's gcd through this keeps every intermediate polynomial monic. A raw DensePoly.gcd of a coprime pair can be a non-trivial constant unit over F_p for p > 2 (e.g. gcd (x^2+1) (x+1) = 2 over F_5); emitting c / gcd c w then leaks that scalar into the square-free factor, breaking the exact reconstruction weightedProduct = f. The monic associate divides c and w exactly as the raw gcd does, so every reconstruction identity carries over, but the emitted quotient stays monic.

Equations

• c.monicGcd w = (Hex.FpPoly.normalizeMonic (Hex.DensePoly.gcd c w)).snd