theorem HexGF2Theory.prime_two : Hex.Nat.Prime 2

2 is prime, the characteristic fact both packed correspondences need to name the generic field over F_2. Stated once here rather than inside each namespace, since the two copies were identical.

instance HexGF2Theory.instPrimeModulusTwo : Hex.ZMod64.PrimeModulus 2

2 is a prime modulus, so Hex.ZMod64 2 is a field and the generic quotient-field construction applies to Hex.FpPoly 2.

def HexGF2Theory.GF2n.modulusFpPoly {n : ℕ} {irr : UInt64} : Hex.FpPoly 2

The packed irreducible modulus viewed inside the generic FpPoly 2 representation.

Equations

• HexGF2Theory.GF2n.modulusFpPoly = HexGF2Theory.GF2Poly.toFpPoly (Hex.GF2Poly.ofUInt64Monic irr n)

theorem HexGF2Theory.GF2n.modulusFpPoly_degree_pos {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} : 0 < modulusFpPoly.degree

The generic FpPoly 2 modulus inherits positive degree from the packed single-word modulus, whose degree is the fixed extension degree n > 0.

theorem HexGF2Theory.GF2n.modulusFpPoly_irreducible {n : ℕ} {irr : UInt64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} : modulusFpPoly.Irreducible

Packed irreducibility transports across the GF2Poly ≃+* FpPoly 2 conversion layer.

@[reducible, inline]

abbrev HexGF2Theory.GF2n.GenericFiniteField {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} : Type

The generic finite-field model corresponding to the packed single-word GF(2^n) wrapper.

Equations

• HexGF2Theory.GF2n.GenericFiniteField = Hex.GFqField.FiniteField HexGF2Theory.GF2n.modulusFpPoly ⋯ HexGF2Theory.prime_two ⋯

def HexGF2Theory.GF2n.toGeneric {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} (x : Hex.GF2n n irr hn hn64 hirr) : GenericFiniteField

Interpret a packed single-word field element inside the generic quotient field model.

Equations

• HexGF2Theory.GF2n.toGeneric x = Hex.GFqField.ofPoly HexGF2Theory.GF2n.modulusFpPoly ⋯ HexGF2Theory.prime_two ⋯ (HexGF2Theory.GF2Poly.toFpPoly (Hex.GF2n.toPolyWord x.val))

def HexGF2Theory.GF2n.ofGeneric {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} (x : GenericFiniteField) : Hex.GF2n n irr hn hn64 hirr

Repack the canonical representative of a generic quotient-field element as a single-word GF(2^n) element.

Equations

• HexGF2Theory.GF2n.ofGeneric x = Hex.GF2n.reduce ((HexGF2Theory.GF2Poly.ofFpPoly (Hex.GFqField.repr x)).toWords.getD 0 0)

@[simp]

theorem HexGF2Theory.GF2n.ofGeneric_toGeneric {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} (x : Hex.GF2n n irr hn hn64 hirr) : ofGeneric (toGeneric x) = x

Embedding a single-word element in the generic model and repacking recovers it: the packed val is already the canonical representative.

@[simp]

theorem HexGF2Theory.GF2n.toGeneric_ofGeneric {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} (x : GenericFiniteField) : toGeneric (ofGeneric x) = x

Repacking a generic element and re-embedding recovers it: the round trip loses nothing because both sides store the same reduced residue.

@[simp]

theorem HexGF2Theory.GF2n.toGeneric_add {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} (x y : Hex.GF2n n irr hn hn64 hirr) : toGeneric (x + y) = toGeneric x + toGeneric y

The single-word embedding is additive: packed XOR-then-reduce agrees with addition in the generic quotient field.

@[simp]

theorem HexGF2Theory.GF2n.toGeneric_mul {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} (x y : Hex.GF2n n irr hn hn64 hirr) : toGeneric (x * y) = toGeneric x * toGeneric y

The single-word embedding is multiplicative: the packed carry-less multiply-then-reduce agrees with multiplication in the generic quotient field.

def HexGF2Theory.GF2n.equiv {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} : Hex.GF2n n irr hn hn64 hirr ≃+* GenericFiniteField

The packed single-word field wrapper is ring-equivalent to the generic finite-field construction over the transported modulus.

Equations

• HexGF2Theory.GF2n.equiv = { toFun := HexGF2Theory.GF2n.toGeneric, invFun := HexGF2Theory.GF2n.ofGeneric, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

def HexGF2Theory.GF2n.finEquiv {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} : Hex.GF2n n irr hn hn64 hirr ≃ Fin (2 ^ n)

Single-word packed field elements are indexed by their bounded canonical word representatives.

Equations

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

@[instance_reducible]

noncomputable instance HexGF2Theory.GF2n.instFintype {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} : Fintype (Hex.GF2n n irr hn hn64 hirr)

Equations

• HexGF2Theory.GF2n.instFintype = Fintype.ofEquiv (Fin (2 ^ n)) HexGF2Theory.GF2n.finEquiv.symm

theorem HexGF2Theory.GF2n.fintype_card {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} : Fintype.card (Hex.GF2n n irr hn hn64 hirr) = 2 ^ n

A single-word GF(2^n) has 2 ^ n elements, read off the val bound rather than transported across the ring equivalence.

@[reducible, inline]

abbrev HexGF2Theory.GF2nPoly.ReducedPackedRep (f : Hex.GF2Poly) : Type

Reduced packed representatives modulo f, isolated from the field wrapper so Mathlib-side finite support can be transported before the final public GF2nPoly cardinality statements are proved.

Equations

• HexGF2Theory.GF2nPoly.ReducedPackedRep f = { p : Hex.GF2Poly // p.IsZero ∨ p.natDegree < f.natDegree }

def HexGF2Theory.GF2nPoly.reducedPackedRepEquiv {f : Hex.GF2Poly} {hirr : f.Irreducible} : Hex.GF2nPoly f hirr ≃ ReducedPackedRep f

The executable packed quotient wrapper is exactly the reduced-representative subtype used for finite support.

Equations

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

def HexGF2Theory.GF2nPoly.reducedPackedRepIndex {f : Hex.GF2Poly} (x : ReducedPackedRep f) : Fin (2 ^ f.natDegree)

Encode a reduced packed representative as a bounded binary index.

Equations

• HexGF2Theory.GF2nPoly.reducedPackedRepIndex x = ⟨HexGF2Theory.GF2Poly.toNat ↑x, ⋯⟩

def HexGF2Theory.GF2nPoly.reducedPackedRepOfIndex {f : Hex.GF2Poly} (i : Fin (2 ^ f.natDegree)) : ReducedPackedRep f

Decode a bounded binary index into the corresponding reduced packed representative.

Equations

• HexGF2Theory.GF2nPoly.reducedPackedRepOfIndex i = ⟨HexGF2Theory.GF2Poly.ofNatBelowDegree f.natDegree ↑i, ⋯⟩

@[simp]

theorem HexGF2Theory.GF2nPoly.reducedPackedRepIndex_ofIndex {f : Hex.GF2Poly} (i : Fin (2 ^ f.natDegree)) : reducedPackedRepIndex (reducedPackedRepOfIndex i) = i

Decoding a bounded index and re-encoding it returns the index.

@[simp]

theorem HexGF2Theory.GF2nPoly.reducedPackedRepOfIndex_index {f : Hex.GF2Poly} (x : ReducedPackedRep f) : reducedPackedRepOfIndex (reducedPackedRepIndex x) = x

Encoding a reduced representative and decoding it returns the representative.

def HexGF2Theory.GF2nPoly.reducedPackedRepFinEquiv {f : Hex.GF2Poly} : ReducedPackedRep f ≃ Fin (2 ^ f.natDegree)

Reduced packed representatives are equivalent to the finite binary index space determined by the modulus degree.

Equations

• HexGF2Theory.GF2nPoly.reducedPackedRepFinEquiv = { toFun := HexGF2Theory.GF2nPoly.reducedPackedRepIndex, invFun := HexGF2Theory.GF2nPoly.reducedPackedRepOfIndex, left_inv := ⋯, right_inv := ⋯ }

def HexGF2Theory.GF2nPoly.modulusFpPoly {f : Hex.GF2Poly} : Hex.FpPoly 2

The packed irreducible modulus viewed inside the generic FpPoly 2 representation.

Equations

• HexGF2Theory.GF2nPoly.modulusFpPoly = HexGF2Theory.GF2Poly.toFpPoly f

theorem HexGF2Theory.GF2nPoly.modulusFpPoly_degree_pos {f : Hex.GF2Poly} {hdeg : 0 < f.natDegree} : 0 < modulusFpPoly.degree

The generic FpPoly 2 modulus inherits positive degree from the packed modulus, which carries it as the explicit hypothesis hdeg : 0 < f.natDegree.

This positivity is not derivable from hirr alone: Hex.GF2Poly.Irreducible (HexGF2/Euclid.lean:57) is f ≠ 0 ∧ ∀ a b, a * b = f → a.natDegree = 0 ∨ b.natDegree = 0, which admits the unit f = 1 (its only factorisations 1 = 1 * 1 have both factors of degree 0), and toFpPoly 1 = 1 has degree 0. Throughout HexGF2, positive degree is taken from a separate hypothesis, never from irreducibility. So the arbitrary-degree wrapper requires 0 < f.natDegree exactly as the single-word GF2n wrapper requires hn : 0 < n above; the toFpPoly transport preserves it via degree?_toFpPoly.

theorem HexGF2Theory.GF2nPoly.modulusFpPoly_irreducible {f : Hex.GF2Poly} {hirr : f.Irreducible} : modulusFpPoly.Irreducible

Packed irreducibility transports across the GF2Poly ≃+* FpPoly 2 conversion layer.

@[reducible, inline]

abbrev HexGF2Theory.GF2nPoly.GenericFiniteField {f : Hex.GF2Poly} {hirr : f.Irreducible} {hdeg : 0 < f.natDegree} : Type

The generic finite-field model corresponding to the packed arbitrary-degree GF(2^n) wrapper.

Equations

• HexGF2Theory.GF2nPoly.GenericFiniteField = Hex.GFqField.FiniteField HexGF2Theory.GF2nPoly.modulusFpPoly ⋯ HexGF2Theory.prime_two ⋯

def HexGF2Theory.GF2nPoly.toGeneric {f : Hex.GF2Poly} {hirr : f.Irreducible} {hdeg : 0 < f.natDegree} (x : Hex.GF2nPoly f hirr) : GenericFiniteField

Interpret a packed quotient-field element inside the generic quotient field model.

Equations

• HexGF2Theory.GF2nPoly.toGeneric x = Hex.GFqField.ofPoly HexGF2Theory.GF2nPoly.modulusFpPoly ⋯ HexGF2Theory.prime_two ⋯ (HexGF2Theory.GF2Poly.toFpPoly x.val)

def HexGF2Theory.GF2nPoly.ofGeneric {f : Hex.GF2Poly} {hirr : f.Irreducible} {hdeg : 0 < f.natDegree} (x : GenericFiniteField) : Hex.GF2nPoly f hirr

Repack the canonical representative of a generic quotient-field element as a packed GF(2^n) residue.

Equations

• HexGF2Theory.GF2nPoly.ofGeneric x = Hex.GF2nPoly.reducePoly (HexGF2Theory.GF2Poly.ofFpPoly (Hex.GFqField.repr x))

theorem HexGF2Theory.GF2nPoly.natDegree_toFpPoly (q : Hex.GF2Poly) : (GF2Poly.toFpPoly q).degree = q.natDegree

FpPoly.degree of a transported packed polynomial equals its packed degree.

theorem HexGF2Theory.GF2nPoly.toFpPoly_reduceMod (p g : Hex.GF2Poly) (hgdeg : 0 < g.natDegree) : GF2Poly.toFpPoly (p % g) = Hex.GFqRing.reduceMod (GF2Poly.toFpPoly g) (GF2Poly.toFpPoly p)

Reduction-compatibility bridge. Packed remainder reduction modulo f transports across the GF2Poly ≃+* FpPoly 2 conversion layer to the generic quotient-ring reduction GFqRing.reduceMod. This is the missing transport that lets the GF2nPoly quotient round-trip / add / mul obligations follow from the already-proved packed-level ring equivalence.

theorem HexGF2Theory.GF2nPoly.eq_of_repr_eq {f : Hex.GF2Poly} {hirr : f.Irreducible} {hdeg : 0 < f.natDegree} {x y : GenericFiniteField} (h : Hex.GFqField.repr x = Hex.GFqField.repr y) : x = y

Equality of generic finite-field elements from equality of canonical representatives.

theorem HexGF2Theory.GF2nPoly.repr_toGeneric {f : Hex.GF2Poly} {hirr : f.Irreducible} {hdeg : 0 < f.natDegree} (x : Hex.GF2nPoly f hirr) : Hex.GFqField.repr (toGeneric x) = GF2Poly.toFpPoly x.val

The canonical representative of a packed element embedded into the generic model is simply its packed value, transported to FpPoly 2.

@[simp]

theorem HexGF2Theory.GF2nPoly.ofGeneric_toGeneric {f : Hex.GF2Poly} {hirr : f.Irreducible} {hdeg : 0 < f.natDegree} (x : Hex.GF2nPoly f hirr) : ofGeneric (toGeneric x) = x

Embedding a packed residue in the generic model and repacking recovers it: the packed value is already reduced modulo f.

@[simp]

theorem HexGF2Theory.GF2nPoly.toGeneric_ofGeneric {f : Hex.GF2Poly} {hirr : f.Irreducible} {hdeg : 0 < f.natDegree} (x : GenericFiniteField) : toGeneric (ofGeneric x) = x

Repacking a generic element and re-embedding recovers it.

@[simp]

theorem HexGF2Theory.GF2nPoly.toGeneric_add {f : Hex.GF2Poly} {hirr : f.Irreducible} {hdeg : 0 < f.natDegree} (x y : Hex.GF2nPoly f hirr) : toGeneric (x + y) = toGeneric x + toGeneric y

The packed-quotient embedding is additive.

@[simp]

theorem HexGF2Theory.GF2nPoly.toGeneric_mul {f : Hex.GF2Poly} {hirr : f.Irreducible} {hdeg : 0 < f.natDegree} (x y : Hex.GF2nPoly f hirr) : toGeneric (x * y) = toGeneric x * toGeneric y

The packed-quotient embedding is multiplicative.

def HexGF2Theory.GF2nPoly.equiv {f : Hex.GF2Poly} {hirr : f.Irreducible} {hdeg : 0 < f.natDegree} : Hex.GF2nPoly f hirr ≃+* GenericFiniteField

The packed arbitrary-degree field wrapper is ring-equivalent to the generic finite-field construction over the transported modulus.

Equations

• HexGF2Theory.GF2nPoly.equiv = { toFun := HexGF2Theory.GF2nPoly.toGeneric, invFun := HexGF2Theory.GF2nPoly.ofGeneric, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

def HexGF2Theory.GF2nPoly.finEquiv {f : Hex.GF2Poly} {hirr : f.Irreducible} : Hex.GF2nPoly f hirr ≃ Fin (2 ^ f.natDegree)

Packed arbitrary-degree field elements are indexed by reduced packed representatives below the modulus degree.

Equations

• HexGF2Theory.GF2nPoly.finEquiv = HexGF2Theory.GF2nPoly.reducedPackedRepEquiv.trans HexGF2Theory.GF2nPoly.reducedPackedRepFinEquiv

@[instance_reducible]

noncomputable instance HexGF2Theory.GF2nPoly.instFintype {f : Hex.GF2Poly} {hirr : f.Irreducible} : Fintype (Hex.GF2nPoly f hirr)

Equations

• HexGF2Theory.GF2nPoly.instFintype = Fintype.ofEquiv (Fin (2 ^ f.natDegree)) HexGF2Theory.GF2nPoly.finEquiv.symm

theorem HexGF2Theory.GF2nPoly.fintype_card {f : Hex.GF2Poly} {hirr : f.Irreducible} : Fintype.card (Hex.GF2nPoly f hirr) = 2 ^ f.natDegree

The packed quotient by f has 2 ^ deg f elements, counted through its reduced-representative subtype.