structure Hex.Berlekamp.DegreePattern : Type

What a bounded distinct-degree pass learned about the irreducible factors of a monic square-free polynomial.

• separated : Array Nat

  Degrees of the irreducible factors already separated, ascending.

• residual : Nat

  Degree of the part not separated; 0 when the pattern is complete.

• minResidualDegree : Nat

  Every irreducible factor of the unseparated part has at least this degree. Always positive.

@[instance_reducible]

instance Hex.Berlekamp.instReprDegreePattern : Repr DegreePattern

Equations

• Hex.Berlekamp.instReprDegreePattern = { reprPrec := Hex.Berlekamp.instReprDegreePattern.repr }

def Hex.Berlekamp.instReprDegreePattern.repr : DegreePattern → Nat → Std.Format

Equations

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

def Hex.Berlekamp.instDecidableEqDegreePattern.decEq (x✝ x✝¹ : DegreePattern) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.Berlekamp.instDecidableEqDegreePattern : DecidableEq DegreePattern

Equations

• Hex.Berlekamp.instDecidableEqDegreePattern = Hex.Berlekamp.instDecidableEqDegreePattern.decEq

def Hex.Berlekamp.DegreePattern.complete (pattern : DegreePattern) : Bool

A complete pattern separated the whole polynomial.

Equations

• pattern.complete = (pattern.residual == 0)

def Hex.Berlekamp.DegreePattern.lowerBound (pattern : DegreePattern) : Nat

Fewest irreducible factors the polynomial can have: those already separated, plus at least one more if anything is left.

Equations

• pattern.lowerBound = pattern.separated.size + if pattern.residual = 0 then 0 else 1

def Hex.Berlekamp.DegreePattern.upperBound (pattern : DegreePattern) : Nat

Most irreducible factors the polynomial can have: those already separated, plus the residual degree divided by the smallest degree any unseparated factor can have.

Equations

• pattern.upperBound = pattern.separated.size + pattern.residual / pattern.minResidualDegree

def Hex.Berlekamp.degreePatternStep {p : Nat} [ZMod64.Bounds p] (d : Nat) (diff residual : FpPoly p) : Array Nat × FpPoly p

One degree-pattern step against the residual carrying X^(p^d) - X mod f.

The returned degrees are m / d copies of d, where m is the degree of the gcd; for square-free input whose factors all have degree at least d, that gcd is exactly the product of the degree-d irreducible factors of the residual.

Equations

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

def Hex.Berlekamp.aboveTarget : Option Nat → Nat → Bool

Whether k separated factors and a nonempty residual already put the factor count above target. The residual carries at least one more factor, so the count is at least k + 1, and target ≤ k settles it.

Equations

• Hex.Berlekamp.aboveTarget none x✝ = false
• Hex.Berlekamp.aboveTarget (some target) x✝ = decide (target ≤ x✝)

def Hex.Berlekamp.degreePatternLoop {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (xMod : FpPoly p) (target : Option Nat) : Nat → Nat → FpPoly p → FpPoly p → Array Nat → DegreePattern

Fuel-bounded degree-pattern loop, maintaining the Frobenius power X^(p^d) mod f across degrees exactly as distinctDegreeFactor does. prevFrob is X^(p^(d-1)) mod f, so the next power is computed only when the loop has decided to separate another degree.

With target = some t the loop abandons the pattern as soon as the factors it has separated show that f has more than t of them; otherwise, and always with target = none, it runs until the pattern is complete.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Berlekamp.degreePatternLoop f hmonic xMod target 0 x✝³ x✝² x✝¹ x✝ = { separated := x✝, residual := Hex.DensePoly.natDegree x✝¹, minResidualDegree := max x✝³ 1 }

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

Separate the monic square-free f by irreducible-factor degree, abandoning the pattern as soon as it is clear that f has more than target irreducible factors.

So a complete result records the exact degree multiset, and an incomplete one records that the factor count exceeds target -- its lowerBound is the witness. Work is bounded by one Frobenius power and one gcd per separated degree, and by the largest factor degree overall.

Equations

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

def Hex.Berlekamp.degreePattern? {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) : Option (Array Nat)

Degrees of the irreducible factors of a monic square-free f over F_p, with multiplicity, in ascending order, obtained without splitting any equal-degree product.

none when the bounded loop did not separate the whole input. The degrees sum to deg f whenever the result is some.

Equations

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