def HexGF2Mathlib.GF2Poly.toFpPoly (p : Hex.GF2Poly) : Hex.FpPoly 2

Unpack a packed GF2Poly into the generic dense polynomial over Hex.ZMod64 2.

Equations

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

def HexGF2Mathlib.GF2Poly.ofFpPoly (p : Hex.FpPoly 2) : Hex.GF2Poly

Repack a generic dense polynomial over Hex.ZMod64 2 into the packed GF2Poly representation.

Equations

• HexGF2Mathlib.GF2Poly.ofFpPoly p = Hex.GF2Poly.ofWords (Hex.Array.ofFn' fun (i : Fin ((Hex.DensePoly.size p + 63) / 64)) => HexGF2Mathlib.GF2Poly.packWord✝ p ↑i)

theorem HexGF2Mathlib.GF2Poly.coeff_toFpPoly (p : Hex.GF2Poly) (i : ℕ) : Hex.DensePoly.coeff (toFpPoly p) i = if p.coeff i = true then 1 else 0

The i-th coefficient of toFpPoly p is the ZMod64 2 lift of the packed bit p.coeff i.

@[simp]

theorem HexGF2Mathlib.GF2Poly.toFpPoly_zero : toFpPoly 0 = 0

Unpacking the packed zero gives the generic zero.

@[simp]

theorem HexGF2Mathlib.GF2Poly.ofFpPoly_zero : ofFpPoly 0 = 0

Repacking the generic zero gives the packed zero.

@[simp]

theorem HexGF2Mathlib.GF2Poly.toFpPoly_one : toFpPoly 1 = 1

Unpacking the packed unit gives the generic unit.

theorem HexGF2Mathlib.GF2Poly.coeff_ofFpPoly (p : Hex.FpPoly 2) (j : ℕ) : (ofFpPoly p).coeff j = decide (Hex.DensePoly.coeff p j ≠ 0)

The j-th coefficient of the repacked polynomial records whether the generic coefficient p.coeff j is nonzero.

@[simp]

theorem HexGF2Mathlib.GF2Poly.ofFpPoly_toFpPoly (p : Hex.GF2Poly) : ofFpPoly (toFpPoly p) = p

Unpacking then repacking recovers the packed polynomial: ofFpPoly is a left inverse of toFpPoly.

@[simp]

theorem HexGF2Mathlib.GF2Poly.toFpPoly_ofFpPoly (p : Hex.FpPoly 2) : toFpPoly (ofFpPoly p) = p

Repacking then unpacking recovers the generic polynomial. The generic side is degree-normalized, so no trailing zero coefficients are introduced.

@[simp]

theorem HexGF2Mathlib.GF2Poly.toFpPoly_add (p q : Hex.GF2Poly) : toFpPoly (p + q) = toFpPoly p + toFpPoly q

Unpacking is additive: packed XOR addition becomes generic coefficientwise addition. Half of the RingEquiv obligation for equiv.

@[simp]

theorem HexGF2Mathlib.GF2Poly.toFpPoly_mul (p q : Hex.GF2Poly) : toFpPoly (p * q) = toFpPoly p * toFpPoly q

Unpacking is multiplicative: the packed carry-less product becomes the generic convolution product. The other half of the RingEquiv obligation for equiv, and the reason the packed representation may be used as a drop-in for FpPoly 2 in ring-level reasoning.

def HexGF2Mathlib.GF2Poly.equiv : Hex.GF2Poly ≃+* Hex.FpPoly 2

The packed GF2Poly representation is ring-equivalent to the generic degree-normalized FpPoly 2 representation.

Equations

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

@[simp]

theorem HexGF2Mathlib.GF2Poly.equiv_apply (p : Hex.GF2Poly) : equiv p = toFpPoly p

The forward direction of equiv is toFpPoly.

@[simp]

theorem HexGF2Mathlib.GF2Poly.equiv_symm_apply (p : Hex.FpPoly 2) : equiv.symm p = ofFpPoly p

The inverse direction of equiv is ofFpPoly.

theorem HexGF2Mathlib.GF2Poly.toFpPoly_injective : Function.Injective toFpPoly

toFpPoly is injective: ofFpPoly is a left inverse.

theorem HexGF2Mathlib.GF2Poly.degree?_toFpPoly (p : Hex.GF2Poly) : Hex.DensePoly.degree? (toFpPoly p) = p.degree?

toFpPoly preserves degree?: the high bit of a packed polynomial becomes the leading ZMod64 2 coefficient, and everything above it vanishes.

theorem HexGF2Mathlib.GF2Poly.irreducible_toFpPoly {p : Hex.GF2Poly} (h : p.Irreducible) : (toFpPoly p).Irreducible

Packed GF(2) irreducibility transports to FpPoly 2 irreducibility across toFpPoly. Both predicates are the project-local executable defs, so the transport runs through the conversion layer directly.

def HexGF2Mathlib.GF2Poly.toNat (p : Hex.GF2Poly) : ℕ

Interpret a packed polynomial as the natural number with the same binary coefficient bits. This gives correspondence modules a finite index for bounded-degree representatives without changing the executable HexGF2 representation.

Equations

• HexGF2Mathlib.GF2Poly.toNat p = HexGF2Mathlib.GF2Poly.wordsToNatAux✝ p.toWords.toList 0

theorem HexGF2Mathlib.GF2Poly.toNat_testBit_eq_coeff (p : Hex.GF2Poly) (j : ℕ) : (toNat p).testBit j = p.coeff j

The binary index and the packed representation agree bit for bit: bit j of toNat p is the coefficient of x ^ j. This is the characterising lemma for toNat, and callers should use it rather than unfolding the word fold.

def HexGF2Mathlib.GF2Poly.ofNatBelowDegree (degree n : ℕ) : Hex.GF2Poly

Rebuild the low degree bits of a natural number as a packed polynomial. The input is expected to be bounded by 2 ^ degree by callers that need a canonical finite representative.

Equations

• HexGF2Mathlib.GF2Poly.ofNatBelowDegree degree n = Hex.GF2Poly.ofWords (Array.ofFn fun (i : Fin ((degree + 63) / 64)) => UInt64.ofNat (n / 2 ^ (64 * ↑i)))

theorem HexGF2Mathlib.GF2Poly.coeff_ofNatBelowDegree_of_lt (degree n j : ℕ) (hj : j < degree) : (ofNatBelowDegree degree n).coeff j = n.testBit j

Below the degree bound, ofNatBelowDegree reproduces the binary digits of its input: the characterising lemma for the decoding direction.

theorem HexGF2Mathlib.GF2Poly.coeff_ofNatBelowDegree_eq_false_of_bound {degree n j : ℕ} (hn : n < 2 ^ degree) (hj : degree ≤ j) : (ofNatBelowDegree degree n).coeff j = false

At or above the degree bound, a decoded index has no coefficients: together with coeff_ofNatBelowDegree_of_lt this pins down ofNatBelowDegree on every index, and it is what makes the decoded value a reduced representative.

theorem HexGF2Mathlib.GF2Poly.toNat_lt_of_degree_lt {p : Hex.GF2Poly} {degree : ℕ} (h : p.IsZero ∨ p.natDegree < degree) : toNat p < 2 ^ degree

A polynomial known to have degree < degree has an index below 2 ^ degree under the packed binary interpretation.

theorem HexGF2Mathlib.GF2Poly.ofNatBelowDegree_reduced (degree : ℕ) (i : Fin (2 ^ degree)) : (ofNatBelowDegree degree ↑i).IsZero ∨ (ofNatBelowDegree degree ↑i).natDegree < degree

Decoding a bounded index as low binary bits produces a reduced packed representative for that degree bound.

theorem HexGF2Mathlib.GF2Poly.toNat_ofNatBelowDegree (degree : ℕ) (i : Fin (2 ^ degree)) : toNat (ofNatBelowDegree degree ↑i) = ↑i

Encoding after decoding a bounded packed index preserves the index.

theorem HexGF2Mathlib.GF2Poly.ofNatBelowDegree_toNat {p : Hex.GF2Poly} {degree : ℕ} (h : p.IsZero ∨ p.natDegree < degree) : ofNatBelowDegree degree (toNat p) = p

Decoding after encoding a reduced packed representative preserves the polynomial.

noncomputable def HexGF2Mathlib.GF2Poly.equivPolynomial : Hex.GF2Poly ≃+* Polynomial (ZMod 2)

The packed GF(2) polynomial representation is ring-equivalent to Mathlib polynomials over ZMod 2.

The composition of the packed-to-generic correspondence with the generic prime-field one, which is what makes the packed representation reachable from Mathlib rather than only from the rest of Hex. noncomputable because Mathlib's polynomial multiplication is; the packed side stays executable.

Equations

• HexGF2Mathlib.GF2Poly.equivPolynomial = HexGF2Mathlib.GF2Poly.equiv.trans HexPolyFpMathlib.fpPolyEquiv

theorem HexGF2Mathlib.GF2Poly.equivPolynomial_apply (q : Hex.GF2Poly) : equivPolynomial q = HexPolyFpMathlib.fpPolyEquiv (toFpPoly q)

The forward direction of equivPolynomial transports the packed value through the generic representation.

Deliberately not @[simp]: coeff_equivPolynomial below is the coefficient normal form, and a simp set containing both would rewrite past its left-hand side and leave a toZMod applied to an if.

@[simp]

theorem HexGF2Mathlib.GF2Poly.equivPolynomial_symm_apply (P : Polynomial (ZMod 2)) : equivPolynomial.symm P = ofFpPoly (HexPolyFpMathlib.polynomialToFpPoly P)

The inverse direction unpacks a Mathlib polynomial back to packed words.

@[simp]

theorem HexGF2Mathlib.GF2Poly.coeff_equivPolynomial (q : Hex.GF2Poly) (i : ℕ) : (equivPolynomial q).coeff i = if q.coeff i = true then 1 else 0

Coefficients survive the crossing: bit i of the packed representation is the i-th Mathlib coefficient, as 1 or 0 in ZMod 2.

This is the lemma a caller reaches for first, and the reason it is stated rather than left to simp: unfolding through both legs leaves a toZMod applied to an if, which needs the branchwise cast lemmas to finish.