def Hex.FpPoly.squareFreeDecomposition {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) : SquareFreeDecomposition p

Compute a square-free decomposition by normalizing away the leading scalar and running Yun's algorithm on the resulting monic polynomial.

Equations

• Hex.FpPoly.squareFreeDecomposition hp f = { unit := f.normalizeMonic.fst, factors := f.normalizeMonic.snd.squareFreeAux 1 (Hex.DensePoly.size f.normalizeMonic.snd + 1) }

theorem Hex.FpPoly.squareFree_pairwise_coprime {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) : have d := squareFreeDecomposition hp f; List.Pairwise (fun (a b : SquareFreeFactor p) => (normalizeMonic (DensePoly.gcd a.factor b.factor)).snd = 1) d.factors

The factors emitted by squareFreeDecomposition are pairwise coprime, witnessed by the normalized gcd of any two distinct factors reducing to 1. This is the underlying coprimality result that the public squareFreeDecomposition_pairwise_coprime wrapper delegates to; callers reason about distinct square-free parts in isolation, relying on this to know no common factor links them.

theorem Hex.FpPoly.squareFree_weightedProduct {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) : have d := squareFreeDecomposition hp f; DensePoly.C d.unit * weightedProduct d.factors = f

The decomposition reconstructs its input: multiplying the emitted unit by the weighted product of the factors (each raised to its recorded multiplicity) recovers f. This is the underlying reconstruction identity that the public squareFreeDecomposition_weightedProduct wrapper delegates to; it certifies the decomposition loses no information, so a caller can substitute the factored form for f anywhere.

theorem Hex.FpPoly.squareFree_factors_squareFree {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) : have d := squareFreeDecomposition hp f; ∀ (sf : SquareFreeFactor p), sf ∈ d.factors → (normalizeMonic (DensePoly.gcd sf.factor (DensePoly.derivative sf.factor))).snd = 1

Each factor emitted by Hex.FpPoly.squareFreeDecomposition is itself square-free, witnessed by the normalized gcd of the factor with its derivative reducing to 1. This is the underlying square-freeness result that the public squareFreeDecomposition_factors_squareFree wrapper delegates to; it is the defining guarantee of the decomposition, letting a caller treat every emitted factor as having no repeated irreducible part.

theorem Hex.FpPoly.squareFreeDecomposition_factors_squareFree {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) : have d := squareFreeDecomposition hp f; ∀ (sf : SquareFreeFactor p), sf ∈ d.factors → (normalizeMonic (DensePoly.gcd sf.factor (DensePoly.derivative sf.factor))).snd = 1

Every factor emitted by Hex.FpPoly.squareFreeDecomposition is square-free, witnessed by the normalized gcd with its derivative reducing to 1. All facts about intermediate Yun states are proved internally, so the statement needs no auxiliary hypotheses.

theorem Hex.FpPoly.squareFreeDecomposition_multiplicity_pos {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) : have d := squareFreeDecomposition hp f; ∀ (sf : SquareFreeFactor p), sf ∈ d.factors → 0 < sf.multiplicity

Every factor emitted by Hex.FpPoly.squareFreeDecomposition carries a strictly positive multiplicity, so no factor is recorded at multiplicity 0. A caller iterating the factor list can therefore treat each recorded exponent as a genuine power and need not special-case a zero exponent.

theorem Hex.FpPoly.squareFreeDecomposition_weightedProduct {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) : have d := squareFreeDecomposition hp f; DensePoly.C d.unit * weightedProduct d.factors = f

Public reconstruction wrapper: the emitted unit and weighted factor product recover the input. All facts about intermediate Yun states are proved internally, so the statement needs no auxiliary hypotheses.

theorem Hex.FpPoly.squareFreeDecomposition_pairwise_coprime {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) : have d := squareFreeDecomposition hp f; List.Pairwise (fun (a b : SquareFreeFactor p) => (normalizeMonic (DensePoly.gcd a.factor b.factor)).snd = 1) d.factors

Public coprimality wrapper: the emitted factors are pairwise coprime, witnessed by the normalized gcd reducing to 1. All facts about intermediate Yun states are proved internally, so the statement needs no auxiliary hypotheses.

theorem Hex.FpPoly.linearPow_add_prime {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f g : FpPoly p) : (f + g).linearPow p = f.linearPow p + g.linearPow p

Freshman's dream for FpPoly.linearPow: in characteristic p, raising to the prime power is additive.

theorem Hex.FpPoly.linearPow_mul_base {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) (n : Nat) : (f * g).linearPow n = f.linearPow n * g.linearPow n

FpPoly.linearPow of a product factors over the base.