def Hex.GF2Poly.divModAux (q : GF2Poly) (fuel : Nat) (quot rem : GF2Poly) : GF2Poly × GF2Poly

Tail-recursive long division for packed GF(2) polynomials.

Equations

• One or more equations did not get rendered due to their size.
• q.divModAux 0 quot rem = (quot, rem)

def Hex.GF2Poly.divMod (p q : GF2Poly) : GF2Poly × GF2Poly

Polynomial long division over GF(2). Division by 0 returns (0, p).

Equations

• p.divMod q = q.divModAux (p.natDegree + 1) 0 p

def Hex.GF2Poly.div (p q : GF2Poly) : GF2Poly

Quotient from polynomial long division over GF(2).

Equations

• p.div q = (p.divMod q).fst

def Hex.GF2Poly.mod (p q : GF2Poly) : GF2Poly

Remainder from polynomial long division over GF(2).

Equations

• p.mod q = (p.divMod q).snd

@[instance_reducible]

instance Hex.GF2Poly.instDiv : Div GF2Poly

Equations

• Hex.GF2Poly.instDiv = { div := Hex.GF2Poly.div }

@[instance_reducible]

instance Hex.GF2Poly.instMod : Mod GF2Poly

Equations

• Hex.GF2Poly.instMod = { mod := Hex.GF2Poly.mod }

@[instance_reducible]

instance Hex.GF2Poly.instDvd : Dvd GF2Poly

Divisibility in GF(2)[x] is witnessed by an explicit quotient.

Equations

• Hex.GF2Poly.instDvd = { dvd := fun (p q : Hex.GF2Poly) => ∃ (r : Hex.GF2Poly), q = p * r }

def Hex.GF2Poly.Irreducible (f : GF2Poly) : Prop

Polynomial irreducibility over GF(2) phrased in terms of nontrivial factorizations inside the packed Hex.GF2Poly execution model.

Equations

• f.Irreducible = (f ≠ 0 ∧ ∀ (a b : Hex.GF2Poly), a * b = f → a.natDegree = 0 ∨ b.natDegree = 0)

def Hex.GF2Poly.lowerMask (n : Nat) : UInt64

Bitmask for coefficients of degree < n inside one UInt64 word.

Equations

• Hex.GF2Poly.lowerMask n = if n < 64 then 1 <<< n.toUInt64 - 1 else 0 - 1

def Hex.GF2Poly.ofUInt64Monic (lower : UInt64) (n : Nat) : GF2Poly

Build the monic degree-n polynomial x^n + lower, truncating lower to degrees < n as required by the packed GF(2^n) modulus convention.

Equations

• Hex.GF2Poly.ofUInt64Monic lower n = Hex.GF2Poly.monomial n + Hex.GF2Poly.ofUInt64 (lower &&& Hex.GF2Poly.lowerMask n)

def Hex.GF2Poly.packedReduceWord (n : Nat) (irr : UInt64) (p : GF2Poly) : UInt64

Reduce a packed polynomial modulo a single-word extension modulus and read back the low canonical word.

Equations

• Hex.GF2Poly.packedReduceWord n irr p = (p % Hex.GF2Poly.ofUInt64Monic irr n).toWords.getD 0 0 &&& Hex.GF2Poly.lowerMask n

def Hex.GF2Poly.canonicalWordLT (n : Nat) (hn64 : n < 64) (w : UInt64) : UInt64

Repackage a word as a canonical representative below 2^n.

Equations

• Hex.GF2Poly.canonicalWordLT n hn64 w = UInt64.ofNatLT (w.toNat % 2 ^ n) ⋯

theorem Hex.GF2Poly.quotient_step_reconstruct (quot rem q : GF2Poly) (k : Nat) : have term := monomial k; (quot + term) * q + (rem + q.mulXk k) = quot * q + rem

A single long-division update preserves quotient/remainder reconstruction.

structure Hex.GF2Poly.XGCDResult : Type

Result package for the packed extended Euclidean algorithm.

• gcd : GF2Poly

  The gcd of the two input polynomials.

• left : GF2Poly

  Bezout cofactor multiplying the first input: left * a + right * b = gcd.

• right : GF2Poly

  Bezout cofactor multiplying the second input: left * a + right * b = gcd.

def Hex.GF2Poly.xgcdAux (r₀ s₀ t₀ r₁ s₁ t₁ : GF2Poly) (fuel : Nat) : XGCDResult

Tail-recursive extended Euclidean algorithm over packed GF(2) polynomials.

Equations

• One or more equations did not get rendered due to their size.
• r₀.xgcdAux s₀ t₀ r₁ s₁ t₁ 0 = { gcd := r₀, left := s₀, right := t₀ }

def Hex.GF2Poly.xgcd (p q : GF2Poly) : XGCDResult

Extended gcd for packed GF(2) polynomials, returning the gcd together with Bezout coefficients.

Equations

• p.xgcd q = p.xgcdAux 1 0 q 0 1 (p.natDegree + q.natDegree + 2)

def Hex.GF2Poly.packedInvWord (n : Nat) (irr w : UInt64) : UInt64

The single-word xgcd inverse candidate reduced modulo the packed irreducible modulus.

Equations

• Hex.GF2Poly.packedInvWord n irr w = Hex.GF2Poly.packedReduceWord n irr ((Hex.GF2Poly.ofUInt64 w).xgcd (Hex.GF2Poly.ofUInt64Monic irr n)).left

def Hex.GF2Poly.gcd (p q : GF2Poly) : GF2Poly

Polynomial gcd over packed GF(2).

Equations

• p.gcd q = (p.xgcd q).gcd

theorem Hex.GF2Poly.divMod_spec (p q : GF2Poly) : have qr := p.divMod q; qr.fst * q + qr.snd = p

The division output reconstructs the dividend.

@[simp]

theorem Hex.GF2Poly.divMod_fst (p q : GF2Poly) : (p.divMod q).fst = p / q

The first component of divMod is the public quotient operation.

@[simp]

theorem Hex.GF2Poly.divMod_snd (p q : GF2Poly) : (p.divMod q).snd = p % q

The second component of divMod is the public remainder operation.

@[simp]

theorem Hex.GF2Poly.divMod_zero_right (p : GF2Poly) : p.divMod 0 = (0, p)

Dividing by zero returns zero quotient and leaves the dividend as the remainder.

@[simp]

theorem Hex.GF2Poly.divMod_zero_left (q : GF2Poly) : divMod 0 q = (0, 0)

Zero has zero quotient and zero remainder against any divisor.

@[simp]

theorem Hex.GF2Poly.div_zero_right (p : GF2Poly) : p / 0 = 0

Division by zero has quotient zero for packed GF(2) polynomials.

@[simp]

theorem Hex.GF2Poly.mod_zero_right (p : GF2Poly) : p % 0 = p

Remainder modulo zero is the dividend for packed GF(2) polynomials.

@[simp]

theorem Hex.GF2Poly.zero_div (q : GF2Poly) : 0 / q = 0

Zero divided by any packed GF(2) polynomial has quotient zero.

@[simp]

theorem Hex.GF2Poly.zero_mod (q : GF2Poly) : 0 % q = 0

Zero has zero remainder modulo any packed GF(2) polynomial.

theorem Hex.GF2Poly.one_ne_zero : 1 ≠ 0

The packed zero and one polynomials are distinct.

theorem Hex.GF2Poly.div_mul_add_mod (p q : GF2Poly) : p / q * q + p % q = p

Quotient/remainder reconstruction through the public / and % operations.

theorem Hex.GF2Poly.mod_degree_lt (p q : GF2Poly) : q ≠ 0 → (p % q).isZero = true ∨ (p % q).natDegree < q.natDegree

The computed remainder has smaller degree than a nonzero divisor.

theorem Hex.GF2Poly.xgcd_bezout (p q : GF2Poly) : have r := p.xgcd q; r.left * p + r.right * q = r.gcd

The extended-gcd output satisfies the Bezout identity.

theorem Hex.GF2Poly.xgcd_left_mul_add_right_mul (p q : GF2Poly) : (p.xgcd q).left * p + (p.xgcd q).right * q = (p.xgcd q).gcd

Let-free Bezout form for automation over the computed extended-gcd record.

theorem Hex.GF2Poly.gcd_dvd_left (p q : GF2Poly) : p.gcd q ∣ p

The gcd divides the left input.

theorem Hex.GF2Poly.gcd_dvd_right (p q : GF2Poly) : p.gcd q ∣ q

The gcd divides the right input.

theorem Hex.GF2Poly.dvd_gcd (d p q : GF2Poly) : d ∣ p → d ∣ q → d ∣ p.gcd q

Any common divisor divides the computed gcd.

@[simp]

theorem Hex.GF2Poly.gcd_zero_right (p : GF2Poly) : p.gcd 0 = p

The gcd with a zero right input is the left input.

@[simp]

theorem Hex.GF2Poly.gcd_zero_left (q : GF2Poly) : gcd 0 q = q

The gcd with a zero left input is the right input.

theorem Hex.GF2Poly.eq_one_of_degree_zero {p : GF2Poly} (hp : p ≠ 0) (hdegree : p.natDegree = 0) : p = 1

A nonzero packed polynomial of degree 0 equals 1, the only degree-0 GF(2) polynomial.

theorem Hex.GF2Poly.natDegree_le_of_dvd_nonzero {p q : GF2Poly} (hp : p ≠ 0) (hq : q ≠ 0) : p ∣ q → p.natDegree ≤ q.natDegree

A nonzero divisor of a nonzero packed polynomial has degree no larger than the dividend.

theorem Hex.GF2Poly.dvd_antisymm {p q : GF2Poly} (hpq : p ∣ q) (hqp : q ∣ p) : p = q

Divisibility is antisymmetric for packed GF(2) polynomials. There is no unit ambiguity because 1 is the only nonzero degree-zero polynomial.

@[simp]

theorem Hex.GF2Poly.degree?_ofUInt64Monic_of_lt_64 (lower : UInt64) {n : Nat} (hn64 : n < 64) : (ofUInt64Monic lower n).degree? = some n

The packed single-word monic modulus has the advertised degree when n < 64.

@[simp]

theorem Hex.GF2Poly.natDegree_ofUInt64Monic_of_lt_64 (lower : UInt64) {n : Nat} (hn64 : n < 64) : (ofUInt64Monic lower n).natDegree = n

The degree of ofUInt64Monic lower n is exactly n when n < 64.

theorem Hex.GF2Poly.coeff_ofUInt64Monic (lower : UInt64) {n : Nat} (hn64 : n < 64) (i : Nat) : (ofUInt64Monic lower n).coeff i = (decide (i = n) != if i < n then (ofUInt64 lower).coeff i else false)

The coefficients of the packed single-word monic modulus: the implicit leading x^n term sets degree n, and the lower degrees read the bits of lower.

theorem Hex.GF2Poly.packedReduceWord_toNat_lt {n : Nat} {irr : UInt64} (hn64 : n < 64) (p : GF2Poly) : (packedReduceWord n irr p).toNat < 2 ^ n

packedReduceWord always returns a canonical word below 2^n for single-word extension degrees.

theorem Hex.GF2Poly.ofUInt64_packedReduceWord_eq_of_degree_lt {n : Nat} {irr : UInt64} (hn64 : n < 64) (p : GF2Poly) (hred : (p % ofUInt64Monic irr n).isZero = true ∨ (p % ofUInt64Monic irr n).natDegree < n) : ofUInt64 (packedReduceWord n irr p) = p % ofUInt64Monic irr n

Masking the low word of a degree-< n residue preserves the represented polynomial.

theorem Hex.GF2Poly.gcd_eq_one_of_irreducible_of_nonzero_reduced {a f : GF2Poly} (hf : f.Irreducible) (ha : a ≠ 0) (hred : a.IsZero ∨ a.natDegree < f.natDegree) : a.gcd f = 1

Any nonzero reduced residue modulo an irreducible packed polynomial is coprime to the modulus, as computed by the packed Euclidean algorithm.

@[simp]

theorem Hex.GF2Poly.mod_add_mul_right_eq_mod (a c f : GF2Poly) : (a + c * f) % f = a % f

Adding a right multiple of the modulus does not change the computed remainder. This is the quotient-congruence form used with Bezout witnesses.

@[simp]

theorem Hex.GF2Poly.mod_eq_self_of_reduced (p f : GF2Poly) (hred : p.isZero = true ∨ p.natDegree < f.natDegree) : p % f = p

A reduced packed polynomial is its own remainder modulo f.

theorem Hex.GF2Poly.mod_eq_of_eq_add_mul_right {a r c f : GF2Poly} (h : a = r + c * f) (hred : r.isZero = true ∨ r.natDegree < f.natDegree) : a % f = r

Validate a remainder using an explicit quotient witness.

theorem Hex.GF2Poly.xgcd_left_mul_mod_eq_gcd_mod (a f : GF2Poly) : a * (a.xgcd f).left % f = a.gcd f % f

The Bezout identity for xgcd gives a congruence between the left inverse candidate and the computed gcd modulo the right input.

theorem Hex.GF2Poly.xgcd_left_mul_mod_eq_one_of_irreducible_of_nonzero_reduced {a f : GF2Poly} (hf : f.Irreducible) (ha : a ≠ 0) (hred : a.IsZero ∨ a.natDegree < f.natDegree) : a * (a.xgcd f).left % f = 1

For a nonzero reduced residue modulo an irreducible packed polynomial, the left Bezout coefficient computed by xgcd is a multiplicative inverse modulo the modulus.

theorem Hex.GF2Poly.mul_mod_xgcd_left_mod_eq_one_of_irreducible_of_nonzero_reduced {a f : GF2Poly} (hf : f.Irreducible) (ha : a ≠ 0) (hred : a.IsZero ∨ a.natDegree < f.natDegree) : a * ((a.xgcd f).left % f) % f = 1 % f

Reducing the xgcd left coefficient before multiplying preserves the left-inverse congruence for nonzero reduced residues modulo an irreducible.

theorem Hex.GF2Poly.packedReduceWord_clmul_packedInvWord_eq_one {n : Nat} {irr w : UInt64} (hn64 : n < 64) (hf : (ofUInt64Monic irr n).Irreducible) (hw : w ≠ 0) (hwlt : w.toNat < 2 ^ n) : packedReduceWord n irr (ofWords #[(clmul w (canonicalWordLT n hn64 (packedInvWord n irr w))).snd, (clmul w (canonicalWordLT n hn64 (packedInvWord n irr w))).fst]) = packedReduceWord n irr 1

The packed single-word CLMUL/reduction path agrees with the polynomial xgcd inverse for nonzero canonical representatives.