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

The basis size used for the Berlekamp matrix of f.

Equations

• Hex.Berlekamp.basisSize f = Hex.DensePoly.natDegree f

def Hex.Berlekamp.coeffVector {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : Vector (ZMod64 p) (basisSize f)

Read a polynomial's first degree f coefficients as a vector.

Equations

• Hex.Berlekamp.coeffVector f g = Vector.ofFn fun (i : Fin (Hex.Berlekamp.basisSize f)) => Hex.DensePoly.coeff g ↑i

def Hex.Berlekamp.berlekampColumn {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (j : Fin (basisSize f)) : Vector (ZMod64 p) (basisSize f)

The j-th Berlekamp-matrix column, obtained by reducing (X^p mod f)^j modulo f and reading the result in the monomial basis.

Equations

• Hex.Berlekamp.berlekampColumn f hmonic j = Hex.Berlekamp.coeffVector f ((f.frobeniusXMod hmonic).powModMonic f hmonic ↑j)

theorem Hex.Berlekamp.berlekampColumn_poly_mod_eq_linearPow_X {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (j : Fin (basisSize f)) : (f.frobeniusXMod hmonic).powModMonic f hmonic ↑j % f = FpPoly.X.linearPow (p * ↑j) % f

The executable j-th Berlekamp column represents X^(p*j) modulo f.

def Hex.Berlekamp.berlekampColumnPolys {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (frobX : FpPoly p) : Nat → FpPoly p → Array (FpPoly p) → Array (FpPoly p)

Iteratively build the array of Berlekamp-matrix column polynomials [1, frobX, frobX^2, …, frobX^(n - 1)], each reduced modulo f. Each step costs one polynomial product and one monic reduction, both quadratic in n, so the array of n columns is built in O(n^3) total.

Equations

• Hex.Berlekamp.berlekampColumnPolys f hmonic frobX 0 x✝¹ x✝ = x✝
• Hex.Berlekamp.berlekampColumnPolys f hmonic frobX k.succ x✝¹ x✝ = Hex.Berlekamp.berlekampColumnPolys f hmonic frobX k (f.modByMonic (x✝¹ * frobX) hmonic) (x✝.push x✝¹)

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

The Berlekamp matrix Q_f, whose j-th column records the coordinates of X^(p * j) mod f in the basis {1, X, ..., X^(n - 1)}. Columns are computed iteratively from the recurrence column (j + 1) = column j * (X^p mod f) mod f to avoid the per-column fast-exponentiation log factor.

Equations

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

theorem Hex.Berlekamp.berlekampMatrix_entry_eq_columnPolys_coeff {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (i j : Fin (basisSize f)) : (berlekampMatrix f hmonic)[i][j] = DensePoly.coeff ((berlekampColumnPolys f hmonic (f.frobeniusXMod hmonic) (basisSize f) 1 #[])[↑j]?.getD 0) ↑i

A Berlekamp matrix entry is the corresponding coefficient of the executable column-polynomial array used by berlekampMatrix.

theorem Hex.Berlekamp.berlekampMatrix_entry_eq_powModMonic_coeff {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (i j : Fin (basisSize f)) : (berlekampMatrix f hmonic)[i][j] = DensePoly.coeff ((f.frobeniusXMod hmonic).powModMonic f hmonic ↑j) ↑i

A Berlekamp matrix entry is the corresponding coefficient of the public powModMonic column representative.

theorem Hex.Berlekamp.berlekampColumn_entry_eq_powModMonic_coeff {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (i j : Fin (basisSize f)) : (berlekampColumn f hmonic j)[i] = DensePoly.coeff ((f.frobeniusXMod hmonic).powModMonic f hmonic ↑j) ↑i

A public Berlekamp column entry is the corresponding coefficient of the powModMonic column representative.

theorem Hex.Berlekamp.berlekampColumn_powModMonic_mod_eq_linearPow_X {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (j : Fin (basisSize f)) : (f.frobeniusXMod hmonic).powModMonic f hmonic ↑j % f = FpPoly.X.linearPow (p * ↑j) % f

The public Berlekamp column representative has the expected X^(p*j) residue modulo f.

theorem Hex.Berlekamp.berlekampMatrix_mulVec_coeffVector_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (w : FpPoly p) (hw : DensePoly.size w ≤ basisSize f) : (berlekampMatrix f hmonic).mulVec (coeffVector f w) = coeffVector f (w.linearPow p % f)

The Berlekamp matrix acts on the basis-{1, X, …, X^(n-1)} coefficient vector of w as the Frobenius map on F_p[X] / (f): when w has degree less than n = basisSize f, multiplying coeffVector f w by berlekampMatrix f hmonic returns the coefficient vector of w^p mod f. The proof factors through the compose-form Frobenius identity compose w (linearPow X p) = linearPow w p from HexPolyFp/Compose.lean.

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

The fixed-space matrix Q_f - I used in Berlekamp's kernel computation. Built in place: only the diagonal of Q_f is decremented, via mapRowsIdx setting one entry per row, rather than rebuilding the whole matrix with ofFn.

Equations

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

theorem Hex.Berlekamp.getElem_fixedSpaceMatrix {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (i j : Fin (basisSize f)) : (fixedSpaceMatrix f hmonic)[i][j] = (berlekampMatrix f hmonic)[i][j] - if i = j then 1 else 0

Entrywise characterization of fixedSpaceMatrix: it is Q_f with 1 subtracted on the diagonal.

theorem Hex.Berlekamp.fixedSpaceMatrix_eq_sub {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) : fixedSpaceMatrix f hmonic = berlekampMatrix f hmonic - Matrix.identity (basisSize f)

fixedSpaceMatrix agrees with the Q_f - I matrix-subtraction form; lets the sub_identity_mulVec algebra apply to the in-place definition.

def Hex.Berlekamp.vectorToPoly {p : Nat} [ZMod64.Bounds p] {n : Nat} (v : Vector (ZMod64 p) n) : FpPoly p

Convert a coefficient vector back to its polynomial representative.

Equations

• Hex.Berlekamp.vectorToPoly v = Hex.FpPoly.ofCoeffs v.toArray

theorem Hex.Berlekamp.coeffVector_vectorToPoly {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (v : Vector (ZMod64 p) (basisSize f)) : coeffVector f (vectorToPoly v) = v

Re-reading the coefficients of a polynomial built from a Berlekamp-basis coefficient vector recovers the original vector.

def Hex.Berlekamp.fixedSpaceKernelVectors {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [ZMod64.PrimeModulus p] : Vector (Vector (ZMod64 p) (basisSize f)) (basisSize f - (fixedSpaceMatrix f hmonic).rowReduce_rank)

The fixed-space kernel of Q_f - I, reusing HexMatrix.nullspace instead of a Berlekamp-local linear-algebra implementation.

Equations

• Hex.Berlekamp.fixedSpaceKernelVectors f hmonic = (Hex.Berlekamp.fixedSpaceMatrix f hmonic).nullspace

def Hex.Berlekamp.IsFixedSpaceKernelVector {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (v : Vector (ZMod64 p) (basisSize f)) : Prop

Vector-level executable Berlekamp kernel condition for the fixed-space matrix Q_f - I.

Equations

• Hex.Berlekamp.IsFixedSpaceKernelVector f hmonic v = ((Hex.Berlekamp.fixedSpaceMatrix f hmonic).mulVec v = 0)

theorem Hex.Berlekamp.isFixedSpaceKernelVector_iff_berlekampMatrix_mulVec_eq {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (v : Vector (ZMod64 p) (basisSize f)) : IsFixedSpaceKernelVector f hmonic v ↔ (berlekampMatrix f hmonic).mulVec v = v

The executable kernel predicate for Q_f - I is equivalent to the usual fixed-space equation Q_f * v = v.

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

Polynomial-level executable Berlekamp kernel condition, by reading the representative in the quotient basis used by fixedSpaceMatrix.

Equations

• Hex.Berlekamp.IsFixedSpaceKernelPolynomial f hmonic g = Hex.Berlekamp.IsFixedSpaceKernelVector f hmonic (Hex.Berlekamp.coeffVector f g)

theorem Hex.Berlekamp.fixedSpaceKernelVectors_sound {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [ZMod64.PrimeModulus p] (k : Fin (basisSize f - (fixedSpaceMatrix f hmonic).rowReduce_rank)) : IsFixedSpaceKernelVector f hmonic ((fixedSpaceKernelVectors f hmonic).get k)

Every vector returned by fixedSpaceKernelVectors satisfies the executable fixed-space kernel condition.

theorem Hex.Berlekamp.fixedSpaceKernelVectors_complete {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [ZMod64.PrimeModulus p] (v : Vector (ZMod64 p) (basisSize f)) : IsFixedSpaceKernelVector f hmonic v → ∃ (c : Vector (ZMod64 p) (basisSize f - (fixedSpaceMatrix f hmonic).rowReduce_rank)), (fixedSpaceMatrix f hmonic).nullspaceBasisMatrix.mulVec c = v

Every vector satisfying the executable fixed-space kernel condition is a linear combination of the public nullspace-basis matrix for Q_f - I.

theorem Hex.Berlekamp.fixedSpaceKernelPolynomial_coeffVector_complete {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [ZMod64.PrimeModulus p] (g : FpPoly p) : IsFixedSpaceKernelPolynomial f hmonic g → ∃ (c : Vector (ZMod64 p) (basisSize f - (fixedSpaceMatrix f hmonic).rowReduce_rank)), (fixedSpaceMatrix f hmonic).nullspaceBasisMatrix.mulVec c = coeffVector f g

Polynomial representatives satisfying the executable fixed-space kernel condition have coefficient vectors in the span of the nullspace basis.

theorem Hex.Berlekamp.isFixedSpaceKernelPolynomial_iff_dvd_linearPow_sub_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (w : FpPoly p) (hw : DensePoly.size w ≤ basisSize f) : IsFixedSpaceKernelPolynomial f hmonic w ↔ f ∣ w.linearPow p - w

Polynomial-level kernel form of the Berlekamp / fixed-space kernel condition: for w of degree below basisSize f, w represents a fixed-space kernel polynomial iff f divides w^p - w.