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

X^(p^k) - X reduced modulo f.

Equations

• Hex.Berlekamp.frobeniusDiffMod f hmonic k = f.frobeniusXPowMod hmonic k - f.modByMonic Hex.FpPoly.X hmonic

def Hex.Berlekamp.properDivisors (n : Nat) : List Nat

Positive divisors of n below n, listed in ascending order.

These are the candidates from which Rabin's test extracts the maximal proper divisors.

Equations

• Hex.Berlekamp.properDivisors n = List.filter (fun (d : Nat) => decide (n % d = 0)) (List.map Nat.succ (List.range (n - 1)))

def Hex.Berlekamp.maximalProperDivisors (n : Nat) : List Nat

The maximal proper divisors of n, i.e. those proper divisors not strictly below any other proper divisor of n.

Equations

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

def Hex.Berlekamp.isUnitPolynomial {p : Nat} [ZMod64.Bounds p] (g : FpPoly p) : Bool

true exactly when g is a nonzero constant polynomial.

Equations

• Hex.Berlekamp.isUnitPolynomial g = match Hex.DensePoly.degree? g with | some 0 => true | x => false

def Hex.Berlekamp.berlekampRankTest {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [Lean.Grind.Field (ZMod64 p)] : Bool

Berlekamp's executable rank criterion: a nonconstant monic f passes when rank(Q_f - I) = deg(f) - 1.

Equations

• Hex.Berlekamp.berlekampRankTest f hmonic = decide (0 < Hex.Berlekamp.basisSize f ∧ (Hex.Berlekamp.fixedSpaceMatrix f hmonic).rowReduce_rank = Hex.Berlekamp.basisSize f - 1)

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

The divisibility leg of Rabin's criterion: f divides X^(p^n) - X, with n = deg(f), exactly when the reduced remainder vanishes.

Equations

• Hex.Berlekamp.rabinDividesTest f hmonic = Hex.DensePoly.isZero (Hex.Berlekamp.frobeniusDiffMod f hmonic (Hex.Berlekamp.basisSize f))

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

The gcd leg of Rabin's criterion at a single maximal proper divisor d of deg(f).

Equations

• Hex.Berlekamp.rabinCoprimeTest f hmonic d = Hex.Berlekamp.isUnitPolynomial (Hex.DensePoly.gcd f (Hex.Berlekamp.frobeniusDiffMod f hmonic d))

def Hex.Berlekamp.rabinWitnesses {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) : List (Nat × Bool)

Record the per-divisor Rabin gcd checks so downstream factorization code can see which maximal proper divisor rejected a candidate polynomial.

Equations

• Hex.Berlekamp.rabinWitnesses f hmonic = List.map (fun (d : Nat) => (d, Hex.Berlekamp.rabinCoprimeTest f hmonic d)) (Hex.Berlekamp.maximalProperDivisors (Hex.Berlekamp.basisSize f))

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

Bezout evidence that one Rabin gcd leg is coprime.

• left : FpPoly p

  Coefficient multiplying the polynomial under test.

• right : FpPoly p

  Coefficient multiplying the corresponding Frobenius difference.

structure Hex.Berlekamp.IrreducibilityCertificate : Type

Self-describing certificate data for Rabin irreducibility checking.

The bezout array is indexed in the same order as maximalProperDivisors n. Each witness proves coprimality of f and X^(p^d) - X mod f by the executable identity left * f + right * (X^(p^d) - X) = 1.

• p : Nat

  The characteristic of the finite field.

• bounds : ZMod64.Bounds self.p

  The modulus bound, carried so the certificate is self-describing.

• n : Nat

  The degree claimed for the polynomial under test.

• powChain : Array (FpPoly self.p)

  Successive Frobenius powers used by the Rabin checks.

• bezout : Array (RabinBezoutWitness self.p)

  Bezout witnesses for the maximal proper divisors of n.

def Hex.Berlekamp.IrreducibilityCertificate.powWitness? (cert : IrreducibilityCertificate) (k : Nat) : Option (FpPoly cert.p)

Read the certified X^(p^k) mod f witness, if present.

Equations

• cert.powWitness? k = cert.powChain[k]?

def Hex.Berlekamp.IrreducibilityCertificate.bezoutWitness? (cert : IrreducibilityCertificate) (i : Nat) : Option (RabinBezoutWitness cert.p)

Read the Bezout witness for the i-th maximal proper divisor, if present.

Equations

• cert.bezoutWitness? i = cert.bezout[i]?

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

Same-prime view of a self-contained certificate after its stored p has been matched against the ambient field.

• n : Nat

  The degree claimed for the polynomial under test.

• powChain : Array (FpPoly p)

  Successive Frobenius powers used by the Rabin checks.

• bezout : Array (RabinBezoutWitness p)

  Bezout witnesses for the maximal proper divisors of n.

def Hex.Berlekamp.IrreducibilityCertificate.toAmbient? (cert : IrreducibilityCertificate) (p : Nat) [ZMod64.Bounds p] : Option (SamePrimeIrreducibilityCertificate p)

Match a certificate's stored prime against the ambient p. Returns the same-prime view on success, or none if the certificate is for a different prime.

Equations

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

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

The Rabin difference polynomial represented by a certificate pow-chain entry.

Equations

• Hex.Berlekamp.certifiedFrobeniusDiffMod f hmonic powWitness = powWitness - f.modByMonic Hex.FpPoly.X hmonic

def Hex.Berlekamp.checkPowChain {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate p) : Bool

Check that a certificate's pow chain matches the committed Frobenius routine.

Equations

• Hex.Berlekamp.checkPowChain f hmonic cert = (cert.powChain.size == cert.n + 1 && (List.range (cert.n + 1)).all fun (k : Nat) => cert.powChain[k]? == some (f.frobeniusXPowMod hmonic k))

def Hex.Berlekamp.checkPowChainLinear {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate p) : Bool

Kernel-reducible pow-chain check for small closed polynomials. It checks the same mathematical witnesses as checkPowChain, but compares against the structural Frobenius evaluator so decide can reduce concrete certificates.

Equations

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

def Hex.Berlekamp.checkRabinBezoutWitness {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate p) (i d : Nat) : Bool

Check one Bezout witness for a Rabin maximal-proper-divisor leg.

Equations

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

def Hex.Berlekamp.checkRabinBezoutWitnesses {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate p) : Bool

Check all Bezout witnesses against maximalProperDivisors cert.n.

Equations

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

def Hex.Berlekamp.checkIrreducibilityCertificate {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : IrreducibilityCertificate) : Bool

Executable checker for a Rabin irreducibility certificate.

It validates the self-described p and n, recomputes every pow-chain entry, checks the divisibility leg X^(p^n) = X mod f, and verifies each Bezout identity for the maximal proper divisors of n.

Equations

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

def Hex.Berlekamp.checkIrreducibilityCertificateLinear {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : IrreducibilityCertificate) : Bool

Kernel-reducible Rabin certificate checker. This is intended for small record-literal polynomials where the theorem input rabinTest f hmonic = true should be discharged by decide.

@[expose] because that is the whole point: without an exposed body, decide in a downstream module file gets stuck on the unreduced application, and the only way to discharge the check is a hand-written simp unfolding, which is what this definition exists to avoid.

Equations

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

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

Rabin's executable irreducibility test: f must be nonconstant, divide X^(p^n) - X, and be coprime to X^(p^d) - X for every maximal proper divisor d of n = deg(f).

Equations

• Hex.Berlekamp.rabinTest f hmonic = (decide (0 < Hex.Berlekamp.basisSize f) && Hex.Berlekamp.rabinDividesTest f hmonic && (Hex.Berlekamp.rabinWitnesses f hmonic).all Prod.snd)

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

Bezout witness that f and the Rabin difference X^(p^d) - X mod f are coprime, computed by the extended Euclidean algorithm.

The extended gcd returns left₀ * f + right₀ * diff = g with g a nonzero constant when the two are coprime; scaling both coefficients by g⁻¹ (as its leading coefficient, i.e. its constant value) normalises the identity to left * f + right * diff = 1, which is exactly the equation checkRabinBezoutWitness verifies. This is compiled, never-in-kernel prep: a wrong witness simply makes the downstream check return false.

Equations

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

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

Assemble a Rabin irreducibility certificate for the monic polynomial f, when rabinTest accepts it.

The pow chain records X^(p^k) mod f for k = 0, …, deg f, matching checkPowChain, and the Bezout array records one normalised rabinBezoutWitness per maximal proper divisor of deg f, in the same order as maximalProperDivisors, matching checkRabinBezoutWitnesses. Returns none when f fails Rabin's test.

This is the prep half of the certifying-irreducibility pattern: the expensive Frobenius-chain and extended-gcd work runs in compiled code here, so the kernel only has to replay the cheap checkIrreducibilityCertificate reduction on the finished data. The generator carries no soundness proof of its own; a wrong certificate makes checkIrreducibilityCertificate return false, never a false pass.

Equations

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

theorem Hex.Berlekamp.berlekampRankTest_spec {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [Lean.Grind.Field (ZMod64 p)] : berlekampRankTest f hmonic = true ↔ 0 < basisSize f ∧ (fixedSpaceMatrix f hmonic).rowReduce_rank = basisSize f - 1

berlekampRankTest succeeds exactly when the fixed-space matrix has rank deg(f) - 1, the Berlekamp rank criterion.

theorem Hex.Berlekamp.rabinDividesTest_spec {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) : rabinDividesTest f hmonic = DensePoly.isZero (frobeniusDiffMod f hmonic (basisSize f))

rabinDividesTest reduces to checking that frobeniusDiffMod f _ n vanishes, where n = deg(f).

theorem Hex.Berlekamp.checkPowChain_spec {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate p) : checkPowChain f hmonic cert = true → ∀ (k : Nat), k ≤ cert.n → cert.powChain[k]? = some (f.frobeniusXPowMod hmonic k)

If checkPowChain accepts, every entry cert.powChain[k] (for k ≤ cert.n) agrees with the committed Frobenius routine FpPoly.frobeniusXPowMod.

theorem Hex.Berlekamp.checkPowChainLinear_spec {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate p) : checkPowChainLinear f hmonic cert = true → ∀ (k : Nat), k ≤ cert.n → cert.powChain[k]? = some (f.frobeniusXPowMod hmonic k)

Linear-kernel companion to checkPowChain_spec: if checkPowChainLinear accepts, every entry agrees with FpPoly.frobeniusXPowMod, after rewriting the structural Frobenius evaluator through FpPoly.frobeniusXPowModLinear_eq_frobeniusXPowMod.

theorem Hex.Berlekamp.checkIrreducibilityCertificate_rabinTest {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : IrreducibilityCertificate) : checkIrreducibilityCertificate f hmonic cert = true → rabinTest f hmonic = true

If checkIrreducibilityCertificate accepts a self-describing certificate, the corresponding rabinTest succeeds. Downstream irreducibility soundness (FpPoly.Irreducible) is then chained via HexBerlekamp.RabinSoundness.rabinTest_imp_irreducible.

theorem Hex.Berlekamp.checkIrreducibilityCertificateLinear_rabinTest {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : IrreducibilityCertificate) : checkIrreducibilityCertificateLinear f hmonic cert = true → rabinTest f hmonic = true

Kernel-reducible counterpart of checkIrreducibilityCertificate_rabinTest, suited to decide-discharged certificates over small concrete polynomials.

def Hex.Berlekamp.checkPowChainLinearIncrementalStep {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate p) (k : Nat) : Bool

The single-step recurrence: powChain[k+1] must equal (powChain[k])^p mod f.

Equations

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

def Hex.Berlekamp.checkPowChainLinearIncremental {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate p) : Bool

Kernel-reducible incremental pow-chain check. Validates that powChain[0] = X mod f and that each successor is the previous entry's p-th power modulo f. Total work is O(n · p) instead of O(Σ p^k).

Equations

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

def Hex.Berlekamp.checkPowChainLinearIncrementalQuotientWitnessStep (f : FpPoly 2) (cert : SamePrimeIrreducibilityCertificate 2) (quotients : Array (FpPoly 2)) (k : Nat) : Bool

Quotient-witness checker for FpPoly 2 pow chains. Entry k of quotients certifies powChain[k] * powChain[k] = powChain[k+1] + quotients[k] * f, with both chain entries already reduced modulo f.

Equations

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

theorem Hex.Berlekamp.checkPowChainLinearIncrementalQuotientWitnessStep_of_entries (f prev curr quot : FpPoly 2) (cert : SamePrimeIrreducibilityCertificate 2) (quotients : Array (FpPoly 2)) (k : Nat) (hprev : cert.powChain[k]? = some prev) (hcurr : cert.powChain[k + 1]? = some curr) (hquot : quotients[k]? = some quot) (hprevRed : DensePoly.natDegree prev < DensePoly.natDegree f) (hcurrRed : DensePoly.natDegree curr < DensePoly.natDegree f) (hmulCoeffs : (prev * prev).coeffs = (curr + quot * f).coeffs) : checkPowChainLinearIncrementalQuotientWitnessStep f cert quotients k = true

Soundness of checkPowChainLinearIncrementalQuotientWitnessStep from explicit chain and quotient entries: given powChain[k] = prev, powChain[k+1] = curr, quotients[k] = quot, both entries reduced below deg f, and the witnessed identity prev * prev = curr + quot * f on coefficients, the checker returns true.

theorem Hex.Berlekamp.checkPowChainLinearIncrementalQuotientWitnessStep_of_entry_bools (f prev curr quot : FpPoly 2) (cert : SamePrimeIrreducibilityCertificate 2) (quotients : Array (FpPoly 2)) (k : Nat) (hprev : cert.powChain[k]? = some prev) (hcurr : cert.powChain[k + 1]? = some curr) (hquot : quotients[k]? = some quot) (hprevRed : decide (DensePoly.natDegree prev < DensePoly.natDegree f) = true) (hcurrRed : decide (DensePoly.natDegree curr < DensePoly.natDegree f) = true) (hmulCoeffs : ((prev * prev).coeffs == (curr + quot * f).coeffs) = true) : checkPowChainLinearIncrementalQuotientWitnessStep f cert quotients k = true

_of_entries restated with the two degree bounds and the coefficient equality supplied as decide/== Booleans, matching the form the checker itself evaluates.

theorem Hex.Berlekamp.degree?_getD_lt_of_size_le {R : Type u} [Zero R] [DecidableEq R] (g : DensePoly R) {n : Nat} (hnpos : 0 < n) (hsize : g.size ≤ n) : g.natDegree < n

A DensePoly whose coefficient size is at most n (with 0 < n) has natDegree < n. Converts a coefficient-count bound into the degree bound consumed by the quotient-witness step lemmas.

theorem Hex.Berlekamp.checkPowChainLinearIncrementalQuotientWitnessStep_of_entry_size_bounds (f prev curr quot : FpPoly 2) (cert : SamePrimeIrreducibilityCertificate 2) (quotients : Array (FpPoly 2)) (k : Nat) (hprev : cert.powChain[k]? = some prev) (hcurr : cert.powChain[k + 1]? = some curr) (hquot : quotients[k]? = some quot) (hfpos : 0 < DensePoly.natDegree f) (hprevSize : DensePoly.size prev ≤ DensePoly.natDegree f) (hcurrSize : DensePoly.size curr ≤ DensePoly.natDegree f) (hmulCoeffs : (prev * prev).coeffs = (curr + quot * f).coeffs) : checkPowChainLinearIncrementalQuotientWitnessStep f cert quotients k = true

_of_entries restated with the two reducedness hypotheses replaced by size bounds on the chain entries, discharged through degree?_getD_lt_of_size_le.

def Hex.Berlekamp.gf2BitCoeff (bits : UInt64) (i : Nat) : ZMod64 2

The i-th coefficient in ZMod64 2 of a packed UInt64 bit-word: 1 when bit i of bits is set, 0 otherwise.

Equations

• Hex.Berlekamp.gf2BitCoeff bits i = if bits >>> i.toUInt64 &&& 1 = 0 then 0 else 1

def Hex.Berlekamp.gf2WordPoly (bits : UInt64) (width : Nat) : FpPoly 2

Reinterpret the low width bits of bits as an FpPoly 2, with coefficient i given by gf2BitCoeff bits i.

Equations

• Hex.Berlekamp.gf2WordPoly bits width = Hex.FpPoly.ofCoeffs (List.map (fun (i : Nat) => Hex.Berlekamp.gf2BitCoeff bits i) (List.range width)).toArray

theorem Hex.Berlekamp.gf2WordPoly_size_le (bits : UInt64) (width : Nat) : DensePoly.size (gf2WordPoly bits width) ≤ width

gf2WordPoly bits width has coefficient size at most width.

theorem Hex.Berlekamp.gf2WordPoly_degree?_getD_lt (bits : UInt64) {width bound : Nat} (hwidth_pos : 0 < bound) (hwidth : width ≤ bound) : DensePoly.natDegree (gf2WordPoly bits width) < bound

If width ≤ bound and 0 < bound, then (gf2WordPoly bits width).natDegree < bound; the degree bound used when feeding a bit-word polynomial to the witness step.

theorem Hex.Berlekamp.gf2WordPoly_coeff (bits : UInt64) (width i : Nat) : DensePoly.coeff (gf2WordPoly bits width) i = if i < width then gf2BitCoeff bits i else 0

Coefficient i of gf2WordPoly bits width is gf2BitCoeff bits i when i < width, and 0 otherwise.

def Hex.Berlekamp.coeffsEqUpTo (bound : Nat) (a b : FpPoly 2) : Bool

true exactly when a and b agree on every coefficient 0 … bound-1; the bounded executable prefix-equality check over List.range bound.

Equations

• Hex.Berlekamp.coeffsEqUpTo bound a b = (List.range bound).all fun (i : Nat) => Hex.DensePoly.coeff a i == Hex.DensePoly.coeff b i

def Hex.Berlekamp.quotientStepCoeffCheck (bound : Nat) (prev curr quot f : FpPoly 2) : Bool

Bounded per-step quotient-witness test: prev * prev and curr + quot * f agree on coefficients below bound.

Equations

• Hex.Berlekamp.quotientStepCoeffCheck bound prev curr quot f = Hex.Berlekamp.coeffsEqUpTo bound (prev * prev) (curr + quot * f)

theorem Hex.Berlekamp.coeff_eq_of_coeffsEqUpTo {bound : Nat} {a b : FpPoly 2} (h : coeffsEqUpTo bound a b = true) (i : Nat) : i < bound → DensePoly.coeff a i = DensePoly.coeff b i

A passing coeffsEqUpTo yields coefficient equality on every index below the bound.

theorem Hex.Berlekamp.coeffs_eq_of_size_le_of_coeff_eq {bound : Nat} {a b : FpPoly 2} (ha : DensePoly.size a ≤ bound) (hb : DensePoly.size b ≤ bound) (hcoeff : ∀ (i : Nat), i < bound → DensePoly.coeff a i = DensePoly.coeff b i) : a.coeffs = b.coeffs

If both polynomials have size at most bound and agree on coefficients below bound, their full coefficient arrays are equal.

theorem Hex.Berlekamp.coeffs_eq_of_size_le_of_coeffsEqUpTo {bound : Nat} {a b : FpPoly 2} (ha : DensePoly.size a ≤ bound) (hb : DensePoly.size b ≤ bound) (h : coeffsEqUpTo bound a b = true) : a.coeffs = b.coeffs

Upgrade a passing coeffsEqUpTo to full coefficient-array equality, given that both polynomials have size at most bound.

theorem Hex.Berlekamp.quotientStep_coeffs_eq_of_check {bound : Nat} {prev curr quot f : FpPoly 2} (hleft : DensePoly.size (prev * prev) ≤ bound) (hright : DensePoly.size (curr + quot * f) ≤ bound) (hcheck : quotientStepCoeffCheck bound prev curr quot f = true) : (prev * prev).coeffs = (curr + quot * f).coeffs

A passing quotientStepCoeffCheck, with both sides bounded in size by bound, certifies (prev * prev).coeffs = (curr + quot * f).coeffs.

def Hex.Berlekamp.gf2WordQuotientStepCoeffCheck (bound width : Nat) (prevBits currBits quotBits fBits : UInt64) : Bool

quotientStepCoeffCheck specialised to GF(2) operands packed as UInt64 bit-words, decoded through gf2WordPoly.

Equations

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

theorem Hex.Berlekamp.gf2WordQuotientStep_coeffs_eq_of_check {bound width : Nat} {prevBits currBits quotBits fBits : UInt64} (hleft : DensePoly.size (gf2WordPoly prevBits width * gf2WordPoly prevBits width) ≤ bound) (hright : DensePoly.size (gf2WordPoly currBits width + gf2WordPoly quotBits width * gf2WordPoly fBits width) ≤ bound) (hcheck : gf2WordQuotientStepCoeffCheck bound width prevBits currBits quotBits fBits = true) : (gf2WordPoly prevBits width * gf2WordPoly prevBits width).coeffs = (gf2WordPoly currBits width + gf2WordPoly quotBits width * gf2WordPoly fBits width).coeffs

Word-packed analogue of quotientStep_coeffs_eq_of_check: a passing gf2WordQuotientStepCoeffCheck under the size bounds yields coefficient-array equality of the decoded GF(2) polynomials.

theorem Hex.Berlekamp.checkRabinBezoutWitness_of_coeffsEqUpTo (f : FpPoly 2) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate 2) {i d bound : Nat} {powWitness : FpPoly 2} {witness : RabinBezoutWitness 2} (hpow : cert.powChain[d]? = some powWitness) (hbezout : cert.bezout[i]? = some witness) (hleft : DensePoly.size (witness.left * f + witness.right * certifiedFrobeniusDiffMod f hmonic powWitness) ≤ bound) (hright : DensePoly.size 1 ≤ bound) (hcoeffs : coeffsEqUpTo bound (witness.left * f + witness.right * certifiedFrobeniusDiffMod f hmonic powWitness) 1 = true) : checkRabinBezoutWitness f hmonic cert i d = true

Prefix-check entry point to checkRabinBezoutWitness: if the Bezout combination left * f + right * diff agrees with 1 on every coefficient up to bound (with both sides bounded by bound), the witness check accepts. Used when the certifier carries a coeffsEqUpTo prefix comparison rather than full polynomial equality.

theorem Hex.Berlekamp.checkRabinBezoutWitness_of_coeffs_eq (f : FpPoly 2) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate 2) {i d : Nat} {powWitness : FpPoly 2} {witness : RabinBezoutWitness 2} (hpow : cert.powChain[d]? = some powWitness) (hbezout : cert.bezout[i]? = some witness) (hcoeffs : (witness.left * f + witness.right * certifiedFrobeniusDiffMod f hmonic powWitness).coeffs = DensePoly.coeffs 1) : checkRabinBezoutWitness f hmonic cert i d = true

Coefficient-equality entry point to checkRabinBezoutWitness: if the Bezout combination left * f + right * diff has the same coefficient array as 1, the witness check accepts.

theorem Hex.Berlekamp.checkRabinBezoutWitness_of_poly_eq (f : FpPoly 2) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate 2) {i d : Nat} {powWitness : FpPoly 2} {witness : RabinBezoutWitness 2} (hpow : cert.powChain[d]? = some powWitness) (hbezout : cert.bezout[i]? = some witness) (hpoly : witness.left * f + witness.right * certifiedFrobeniusDiffMod f hmonic powWitness = 1) : checkRabinBezoutWitness f hmonic cert i d = true

Polynomial-equality entry point to checkRabinBezoutWitness: if the Bezout combination left * f + right * diff equals 1 as a polynomial, the witness check accepts. The terminal form the two coefficient-level entry points reduce to.

theorem Hex.Berlekamp.checkPowChainLinearIncrementalQuotientWitnesses_first_of_coeffs (f first : FpPoly 2) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate 2) (hfirst : cert.powChain[0]? = some first) (hcoeffs : first.coeffs = (f.modByMonic FpPoly.X hmonic).coeffs) : (cert.powChain[0]? == some (f.modByMonic FpPoly.X hmonic)) = true

Discharge the first-entry condition of checkPowChainLinearIncrementalQuotientWitnesses from coefficient equality: if powChain[0] has the same coefficient array as X mod f, then powChain[0]? == some (X mod f).

theorem Hex.Berlekamp.checkPowChainLinearIncrementalQuotientWitnesses_first_of_coeffs_beq (f first : FpPoly 2) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate 2) (hfirst : cert.powChain[0]? = some first) (hcoeffs : (first.coeffs == (f.modByMonic FpPoly.X hmonic).coeffs) = true) : (cert.powChain[0]? == some (f.modByMonic FpPoly.X hmonic)) = true

Bool-valued variant of checkPowChainLinearIncrementalQuotientWitnesses_first_of_coeffs: accepts the first-entry condition from a == coefficient comparison that evaluates to true.

def Hex.Berlekamp.checkPowChainLinearIncrementalQuotientWitnesses (f : FpPoly 2) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate 2) (quotients : Array (FpPoly 2)) : Bool

Quotient-witness form of the incremental pow-chain check: validates the chain size, that powChain[0] = X mod f, and every per-step witness via checkPowChainLinearIncrementalQuotientWitnessStep. Avoids recomputing the modular squarings by reading the quotients off the certificate.

Equations

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

theorem Hex.Berlekamp.checkPowChainLinearIncrementalQuotientWitnesses_of_steps (f : FpPoly 2) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate 2) (quotients : Array (FpPoly 2)) (hpowSize : (cert.powChain.size == cert.n + 1) = true) (hquotSize : (quotients.size == cert.n) = true) (hfirst : (cert.powChain[0]? == some (f.modByMonic FpPoly.X hmonic)) = true) (hsteps : ∀ (k : Nat), k < cert.n → checkPowChainLinearIncrementalQuotientWitnessStep f cert quotients k = true) : checkPowChainLinearIncrementalQuotientWitnesses f hmonic cert quotients = true

Introduction rule for checkPowChainLinearIncrementalQuotientWitnesses: assemble acceptance from the two size conditions, the first-entry condition, and a per-step witness check for every k < cert.n.

theorem Hex.Berlekamp.checkPowChainLinearIncremental_of_quotientWitnesses (f : FpPoly 2) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate 2) (quotients : Array (FpPoly 2)) : checkPowChainLinearIncrementalQuotientWitnesses f hmonic cert quotients = true → checkPowChainLinearIncremental f hmonic cert = true

Soundness of the quotient-witness chain check against the squaring-based one: if checkPowChainLinearIncrementalQuotientWitnesses accepts, then so does checkPowChainLinearIncremental. Each accepted quotient witness prev * prev = curr + quot * f (both entries reduced) pins curr = powModMonicLinear prev f _ 2, recovering the step recurrence.

def Hex.Berlekamp.checkIrreducibilityCertificateLinearIncremental {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : IrreducibilityCertificate) : Bool

Incremental Rabin certificate checker, suitable for (p, n) regimes where p^n is too large for checkIrreducibilityCertificateLinear but n · p remains in budget (e.g. (5, 6) or (7, 6)).

Equations

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

theorem Hex.Berlekamp.checkPowChainLinearIncremental_spec {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : SamePrimeIrreducibilityCertificate p) : checkPowChainLinearIncremental f hmonic cert = true → ∀ (k : Nat), k ≤ cert.n → cert.powChain[k]? = some (f.frobeniusXPowMod hmonic k)

Incremental companion to checkPowChain_spec: if checkPowChainLinearIncremental accepts, every entry agrees with FpPoly.frobeniusXPowMod. The proof inducts on k, using the chain identity X^(p^(k+1)) ≡ (X^(p^k))^p (mod f).

theorem Hex.Berlekamp.checkIrreducibilityCertificateLinearIncremental_rabinTest {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : IrreducibilityCertificate) : checkIrreducibilityCertificateLinearIncremental f hmonic cert = true → rabinTest f hmonic = true

Incremental counterpart of checkIrreducibilityCertificate_rabinTest, suited to (p, n) regimes where the per-step O(n · p) cost fits the decide kernel budget but the bulk O(Σ p^k) of the non-incremental checker does not.

theorem Hex.Berlekamp.checkIrreducibilityCertificate_of_linearIncremental {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : IrreducibilityCertificate) (hcheck : checkIrreducibilityCertificateLinearIncremental f hmonic cert = true) : checkIrreducibilityCertificate f hmonic cert = true

The incremental kernel checker implies the committed checker: a certificate accepted by checkIrreducibilityCertificateLinearIncremental is accepted by checkIrreducibilityCertificate. This lets kernel-replayed certificates feed consumers stated over the committed checker without restating their soundness.