@[instance_reducible]

instance Hex.GF2Poly.instDecidableEq : DecidableEq GF2Poly

Decidable equality on packed GF(2) polynomials, derived from the underlying Array UInt64 representation. The wf field is a Prop, so its proofs are irrelevant for the structural comparison.

Equations

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

@[instance_reducible]

instance Hex.GF2Poly.instBEq : BEq GF2Poly

Boolean equality on packed GF(2) polynomials, computed by decide on the decidable propositional equality.

Equations

• Hex.GF2Poly.instBEq = { beq := fun (p q : Hex.GF2Poly) => decide (p = q) }

instance Hex.GF2Poly.instLawfulBEq : LawfulBEq GF2Poly

instBEq is lawful: its boolean equality agrees with propositional equality in both directions, via of_decide_eq_true and decide_eq_true.

def Hex.GF2Poly.sqMod (f g : GF2Poly) : GF2Poly

Square a polynomial modulo f.

Equations

• f.sqMod g = g * g % f

def Hex.GF2Poly.xpow2kMod (f : GF2Poly) : Nat → GF2Poly

Iterated squaring k times starting from X mod f, computing X^(2^k) mod f over the packed GF(2) representation.

Equations

• f.xpow2kMod 0 = Hex.GF2Poly.monomial 1 % f
• f.xpow2kMod k.succ = f.sqMod (f.xpow2kMod k)

@[simp]

theorem Hex.GF2Poly.xpow2kMod_zero (f : GF2Poly) : f.xpow2kMod 0 = monomial 1 % f

The zeroth Rabin Frobenius power is X reduced modulo f.

@[simp]

theorem Hex.GF2Poly.xpow2kMod_succ (f : GF2Poly) (k : Nat) : f.xpow2kMod (k + 1) = f.sqMod (f.xpow2kMod k)

The next Rabin Frobenius power is obtained by squaring the previous remainder modulo f.

def Hex.GF2Poly.frobeniusDiffMod (f : GF2Poly) (k : Nat) : GF2Poly

The polynomial X^(2^k) - X reduced modulo f. Since the packed representation is over characteristic two, subtraction collapses to addition.

Equations

• f.frobeniusDiffMod k = f.xpow2kMod k + Hex.GF2Poly.monomial 1 % f

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

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

Equations

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

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

The maximal proper divisors of n: those proper divisors not strictly below any other proper divisor of n.

Equations

• Hex.GF2Poly.maximalProperDivisors n = List.filter (fun (d : Nat) => !(Hex.GF2Poly.properDivisors n).any fun (e : Nat) => decide (d < e) && decide (e % d = 0)) (Hex.GF2Poly.properDivisors n)

def Hex.GF2Poly.isUnitPolynomial (g : GF2Poly) : Bool

true exactly when g is a nonzero constant polynomial.

Equations

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

def Hex.GF2Poly.rabinDividesTest (f : GF2Poly) : Bool

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

Equations

• f.rabinDividesTest = (f.frobeniusDiffMod f.natDegree).isZero

def Hex.GF2Poly.rabinCoprimeTest (f : GF2Poly) (d : Nat) : Bool

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

Equations

• f.rabinCoprimeTest d = (f.gcd (f.frobeniusDiffMod d)).isUnitPolynomial

def Hex.GF2Poly.rabinWitnesses (f : GF2Poly) : List (Nat × Bool)

Per-divisor Rabin gcd outcomes for downstream factorization use.

Equations

• f.rabinWitnesses = List.map (fun (d : Nat) => (d, f.rabinCoprimeTest d)) (Hex.GF2Poly.maximalProperDivisors f.natDegree)

@[simp]

theorem Hex.GF2Poly.rabinWitnesses_all (f : GF2Poly) : f.rabinWitnesses.all Prod.snd = (maximalProperDivisors f.natDegree).all fun (d : Nat) => f.rabinCoprimeTest d

Checking all stored Rabin witnesses is the same as checking the Rabin coprime test over every maximal proper divisor.

def Hex.GF2Poly.rabinTest (f : GF2Poly) : Bool

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

Equations

• f.rabinTest = (decide (0 < f.natDegree) && f.rabinDividesTest && f.rabinWitnesses.all Prod.snd)

structure Hex.GF2Poly.RabinBezoutWitness : Type

Bezout evidence that one Rabin gcd leg is coprime.

• left : GF2Poly

  Cofactor multiplying f in the Bezout identity left * f + right * (X^(2^d) - X mod f) = 1.

• right : GF2Poly

  Cofactor multiplying the Rabin gcd leg in the Bezout identity left * f + right * (X^(2^d) - X mod f) = 1.

structure Hex.GF2Poly.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^(2^d) - X mod f by the executable identity left * f + right * (X^(2^d) - X mod f) = 1.

• n : Nat

  The degree n = deg(f) whose maximal proper divisors index the checks.

• powChain : Array GF2Poly

  The chain of X^(2^d) - X mod f residues, one per relevant divisor of n.

• bezout : Array RabinBezoutWitness

  Bezout witnesses, indexed like maximalProperDivisors n.

def Hex.GF2Poly.IrreducibilityCertificate.powWitness? (cert : IrreducibilityCertificate) (k : Nat) : Option GF2Poly

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

Equations

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

@[simp]

theorem Hex.GF2Poly.IrreducibilityCertificate.powWitness?_eq_getElem? (cert : IrreducibilityCertificate) (k : Nat) : cert.powWitness? k = cert.powChain[k]?

Certificate pow witnesses are backed directly by the pow-chain array.

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

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

Equations

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

@[simp]

theorem Hex.GF2Poly.IrreducibilityCertificate.bezoutWitness?_eq_getElem? (cert : IrreducibilityCertificate) (i : Nat) : cert.bezoutWitness? i = cert.bezout[i]?

Certificate Bezout witnesses are backed directly by the Bezout array.

def Hex.GF2Poly.certifiedFrobeniusDiffMod (f powWitness : GF2Poly) : GF2Poly

The Rabin difference polynomial represented by a certificate pow-chain entry. Equivalently powWitness + (X mod f) since char 2 collapses subtraction to addition.

Equations

• f.certifiedFrobeniusDiffMod powWitness = powWitness + Hex.GF2Poly.monomial 1 % f

def Hex.GF2Poly.checkPowChain (f : GF2Poly) (cert : IrreducibilityCertificate) : Bool

Check that a certificate's pow chain matches the executable iteration xpow2kMod. The first entry must equal X mod f, and each subsequent entry must equal the squaring step sqMod f of the previous.

Equations

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

def Hex.GF2Poly.checkRabinBezoutWitness (f : GF2Poly) (cert : IrreducibilityCertificate) (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.GF2Poly.checkRabinBezoutWitnesses (f : GF2Poly) (cert : IrreducibilityCertificate) : Bool

Check all Bezout witnesses against maximalProperDivisors cert.n.

Equations

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

def Hex.GF2Poly.checkIrreducibilityCertificate (f : GF2Poly) (cert : IrreducibilityCertificate) : Bool

Executable checker for a Rabin irreducibility certificate.

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

Consumer-facing soundness target: checkIrreducibilityCertificate_imp_irreducible in HexGF2/RabinSoundness.lean lifts a true outcome to GF2Poly.Irreducible f.

Equations

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

def Hex.GF2Poly.checkPowChainLinear (f : GF2Poly) (cert : IrreducibilityCertificate) : Bool

Linear-time pow-chain check: each entry must be the squaring step of the previous, with the first entry equal to X mod f.

This is logically equivalent to checkPowChain but uses only O(n) squarings during kernel reduction, where checkPowChain recomputes xpow2kMod f k from scratch for each k and is O(n^2). The linear form is intended for kernel-reducible decide checks on certificates whose modulus has degree comparable to a few machine words.

Equations

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

def Hex.GF2Poly.checkIrreducibilityCertificateLinear (f : GF2Poly) (cert : IrreducibilityCertificate) : Bool

Linear-time variant of checkIrreducibilityCertificate. The only difference is that it uses checkPowChainLinear for the pow-chain leg.

Consumer-facing soundness target: checkIrreducibilityCertificateLinear_imp_irreducible in HexGF2/RabinSoundness.lean lifts a true outcome to GF2Poly.Irreducible f.

Equations

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

theorem Hex.GF2Poly.rabinDividesTest_spec (f : GF2Poly) : f.rabinDividesTest = (f.frobeniusDiffMod f.natDegree).isZero

The executable Rabin divisibility test is definitionally the zero-remainder test for X^(2^deg f) - X modulo f.

theorem Hex.GF2Poly.checkPowChain_spec (f : GF2Poly) (cert : IrreducibilityCertificate) : f.checkPowChain cert = true → ∀ (k : Nat), k ≤ cert.n → cert.powChain[k]? = some (f.xpow2kMod k)

A successful quadratic pow-chain check certifies every stored X^(2^k) mod f value up to the certificate degree.

theorem Hex.GF2Poly.checkIrreducibilityCertificate_rabinTest (f : GF2Poly) (cert : IrreducibilityCertificate) : f.checkIrreducibilityCertificate cert = true → f.rabinTest = true

The executable certificate checker is sound against the parallel rabinTest Bool predicate.

The irreducibility-level theorem is provided in HexGF2/RabinSoundness.lean as checkIrreducibilityCertificate_imp_irreducible.

theorem Hex.GF2Poly.checkPowChainLinear_spec (f : GF2Poly) (cert : IrreducibilityCertificate) : f.checkPowChainLinear cert = true → ∀ (k : Nat), k ≤ cert.n → cert.powChain[k]? = some (f.xpow2kMod k)

A successful linear pow-chain check certifies every stored X^(2^k) mod f value up to the certificate degree.

theorem Hex.GF2Poly.checkIrreducibilityCertificateLinear_rabinTest (f : GF2Poly) (cert : IrreducibilityCertificate) : f.checkIrreducibilityCertificateLinear cert = true → f.rabinTest = true

A successful linear irreducibility certificate checker implies the executable Rabin test succeeds.