structure Hex.Berlekamp.DegreeBucket (p : Nat) [ZMod64.Bounds p] : Type

One distinct-degree bucket: the product of factors of the recorded degree.

• degree : Nat

  The common degree of the irreducible factors in this bucket.

• factor : FpPoly p

  The product of all irreducible factors of the recorded degree.

structure Hex.Berlekamp.DistinctDegreeFactorization (p : Nat) [ZMod64.Bounds p] : Type

Public result of executable distinct-degree factorization. residual is kept explicit so downstream callers can inspect any part not separated by the bounded executable pass.

• input : FpPoly p

  The monic square-free polynomial supplied to the algorithm.

• buckets : List (DegreeBucket p)

  Products grouped by irreducible-factor degree.

• residual : FpPoly p

  The part not separated by the bounded pass.

def Hex.Berlekamp.degreeBucketFactors {p : Nat} [ZMod64.Bounds p] (buckets : List (DegreeBucket p)) : List (FpPoly p)

Extract the polynomial factors recorded in distinct-degree buckets.

Equations

• Hex.Berlekamp.degreeBucketFactors buckets = List.map Hex.Berlekamp.DegreeBucket.factor buckets

@[simp]

theorem Hex.Berlekamp.degreeBucketFactors_nil {p : Nat} [ZMod64.Bounds p] : degreeBucketFactors [] = []

degreeBucketFactors of the empty bucket list is the empty factor list. Definitional rewrite (by rfl) characterising degreeBucketFactors.

@[simp]

theorem Hex.Berlekamp.degreeBucketFactors_cons {p : Nat} [ZMod64.Bounds p] (bucket : DegreeBucket p) (buckets : List (DegreeBucket p)) : degreeBucketFactors (bucket :: buckets) = bucket.factor :: degreeBucketFactors buckets

degreeBucketFactors distributes over ::, pulling the head bucket's .factor to the front of the recovered factor list. Definitional rewrite (by rfl) characterising degreeBucketFactors.

@[simp]

theorem Hex.Berlekamp.degreeBucketFactors_append {p : Nat} [ZMod64.Bounds p] (buckets₁ buckets₂ : List (DegreeBucket p)) : degreeBucketFactors (buckets₁ ++ buckets₂) = degreeBucketFactors buckets₁ ++ degreeBucketFactors buckets₂

degreeBucketFactors distributes over ++: the factors of a concatenated bucket list are the concatenation of each part's factors.

def Hex.Berlekamp.degreeBucketProduct {p : Nat} [ZMod64.Bounds p] (buckets : List (DegreeBucket p)) : FpPoly p

Multiply the polynomial factors recorded in distinct-degree buckets.

Equations

• Hex.Berlekamp.degreeBucketProduct buckets = Hex.Berlekamp.factorProduct (Hex.Berlekamp.degreeBucketFactors buckets)

@[simp]

theorem Hex.Berlekamp.degreeBucketProduct_nil {p : Nat} [ZMod64.Bounds p] : degreeBucketProduct [] = 1

The product over the empty bucket list is 1. Definitional rewrite (by rfl) characterising degreeBucketProduct.

def Hex.Berlekamp.DistinctDegreeFactorization.product {p : Nat} [ZMod64.Bounds p] (result : DistinctDegreeFactorization p) : FpPoly p

Product represented by a distinct-degree factorization result.

Equations

• result.product = Hex.Berlekamp.degreeBucketProduct result.buckets * result.residual

@[simp]

theorem Hex.Berlekamp.DistinctDegreeFactorization.product_eq {p : Nat} [ZMod64.Bounds p] (result : DistinctDegreeFactorization p) : result.product = degreeBucketProduct result.buckets * result.residual

Unfold DistinctDegreeFactorization.product to the product of the bucket factors times the residual. Definitional rewrite (by rfl) characterising DistinctDegreeFactorization.product.

def Hex.Berlekamp.distinctDegreeCandidate {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (residual : FpPoly p) (d : Nat) : FpPoly p

The degree-d gcd candidate against the current residual polynomial.

Equations

• Hex.Berlekamp.distinctDegreeCandidate f hmonic residual d = Hex.DensePoly.gcd residual (Hex.Berlekamp.frobeniusDiffMod f hmonic d)

def Hex.Berlekamp.distinctDegreeStep {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (residual : FpPoly p) (d : Nat) : Option (DegreeBucket p) × FpPoly p

One executable DDF step, returning an optional newly found bucket.

Equations

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

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

Compute the distinct-degree factorization surface of a monic polynomial over F_p.

Equations

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

def Hex.Berlekamp.DegreeBucket.matchesFrobeniusDegree {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (bucket : DegreeBucket p) : Prop

Predicate used by the bucket invariant theorem: the recorded factor divides the corresponding X^(p^d) - X mod f. The unnormalised executable DensePoly.gcd does not return bucket.factor literally on the left of gcd bucket.factor (frobeniusDiffMod ...) = bucket.factor (e.g. gcd X (2*X) = 2*X over F_3), so the morally-correct invariant is the divisibility statement that gcd_dvd_right already supplies.

Equations

• Hex.Berlekamp.DegreeBucket.matchesFrobeniusDegree f hmonic bucket = (bucket.factor ∣ Hex.Berlekamp.frobeniusDiffMod f hmonic bucket.degree)

theorem Hex.Berlekamp.DegreeBucket.matchesFrobeniusDegree_iff {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (bucket : DegreeBucket p) : matchesFrobeniusDegree f hmonic bucket ↔ bucket.factor ∣ frobeniusDiffMod f hmonic bucket.degree

Restate DegreeBucket.matchesFrobeniusDegree as the divisibility bucket.factor ∣ frobeniusDiffMod f hmonic bucket.degree, the morally-correct bucket invariant. Definitional rewrite (by rfl).

theorem Hex.Berlekamp.distinctDegreeCandidate_spec {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (residual : FpPoly p) (d : Nat) : distinctDegreeCandidate f hmonic residual d = DensePoly.gcd residual (frobeniusDiffMod f hmonic d)

The degree-d candidate unfolds to DensePoly.gcd residual (frobeniusDiffMod f hmonic d). Definitional rewrite (by rfl) characterising distinctDegreeCandidate.

theorem Hex.Berlekamp.degreeBucketProduct_append {p : Nat} [ZMod64.Bounds p] (buckets₁ buckets₂ : List (DegreeBucket p)) : degreeBucketProduct (buckets₁ ++ buckets₂) = degreeBucketProduct buckets₁ * degreeBucketProduct buckets₂

Bucket products distribute over list append in stored bucket order.

theorem Hex.Berlekamp.degreeBucketProduct_singleton {p : Nat} [ZMod64.Bounds p] (bucket : DegreeBucket p) : degreeBucketProduct [bucket] = bucket.factor

The product of a singleton bucket list is its recorded factor. Not @[simp]: simp already closes it from degreeBucketProduct_cons, degreeBucketProduct_nil, and FpPoly.mul_one.

@[simp]

theorem Hex.Berlekamp.degreeBucketProduct_cons {p : Nat} [ZMod64.Bounds p] (bucket : DegreeBucket p) (buckets : List (DegreeBucket p)) : degreeBucketProduct (bucket :: buckets) = bucket.factor * degreeBucketProduct buckets

Pull the first bucket factor out of a bucket product.

theorem Hex.Berlekamp.prod_distinctDegreeFactor {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (_hsquareFree : DensePoly.gcd f (DensePoly.derivative f) = 1) : (distinctDegreeFactor f hmonic).product = f

The executable distinct-degree factorization preserves the input polynomial as the product of recorded degree buckets and the residual factor.

theorem Hex.Berlekamp.distinctDegreeFactor_bucket_invariants {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (hsquareFree : DensePoly.gcd f (DensePoly.derivative f) = 1) (bucket : DegreeBucket p) : bucket ∈ (distinctDegreeFactor f hmonic).buckets → 0 < bucket.degree ∧ DegreeBucket.matchesFrobeniusDegree f hmonic bucket

Every recorded bucket is associated with a positive degree and satisfies the corresponding Frobenius-degree divisibility invariant.

theorem Hex.Berlekamp.distinctDegreeFactor_bucket_degree_pos {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (hsquareFree : DensePoly.gcd f (DensePoly.derivative f) = 1) {bucket : DegreeBucket p} (hmem : bucket ∈ (distinctDegreeFactor f hmonic).buckets) : 0 < bucket.degree

Every bucket emitted by distinctDegreeFactor records a positive Frobenius degree.

theorem Hex.Berlekamp.distinctDegreeFactor_bucket_matchesFrobeniusDegree {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (hsquareFree : DensePoly.gcd f (DensePoly.derivative f) = 1) {bucket : DegreeBucket p} (hmem : bucket ∈ (distinctDegreeFactor f hmonic).buckets) : DegreeBucket.matchesFrobeniusDegree f hmonic bucket

Every bucket emitted by distinctDegreeFactor divides its matching Frobenius difference.