def Hex.GF2PolyNormalized (words : Array UInt64) : Prop

Packed-word normalization for GF2Poly: either the polynomial is zero, or its highest stored word is nonzero.

Equations

• Hex.GF2PolyNormalized words = (words.size = 0 ∨ words.back? ≠ some 0)

structure Hex.GF2Poly : Type

Polynomials over F_2, packed into 64-bit words. Bit j of words[i] stores the coefficient of x^(64 * i + j).

• words : Array UInt64

  The packed coefficient words: bit j of words[i] is the coefficient of x^(64 * i + j).

• normalized : GF2PolyNormalized self.words

theorem Hex.GF2Poly.ext_words {p q : GF2Poly} (h : p.words = q.words) : p = q

Packed polynomials are equal when their normalized word arrays are equal.

def Hex.GF2Poly.trimTrailingZeroWordsList : List UInt64 → List UInt64

Remove trailing zero words without disturbing the lower-degree prefix.

Equations

• Hex.GF2Poly.trimTrailingZeroWordsList [] = []
• Hex.GF2Poly.trimTrailingZeroWordsList (w :: ws) = if Hex.GF2Poly.trimTrailingZeroWordsList ws = [] ∧ w = 0 then [] else w :: Hex.GF2Poly.trimTrailingZeroWordsList ws

def Hex.GF2Poly.normalizeWords (words : Array UInt64) : Array UInt64

Normalize a word array by discarding trailing zero words.

Equations

• Hex.GF2Poly.normalizeWords words = (Hex.GF2Poly.trimTrailingZeroWordsList words.toList).toArray

def Hex.GF2Poly.coeffWords (words : Array UInt64) (n : Nat) : Bool

Packed-word coefficient lookup before wrapping the array as a GF2Poly.

Equations

• Hex.GF2Poly.coeffWords words n = (words[n / 64]?.getD 0 >>> (n % 64).toUInt64 &&& 1 != 0)

@[simp]

theorem Hex.GF2Poly.normalizeWords_get?_getD (words : Array UInt64) (i : Nat) : (normalizeWords words)[i]?.getD 0 = words[i]?.getD 0

Trailing-zero normalization preserves every packed coefficient word.

@[simp]

theorem Hex.GF2Poly.coeffWords_normalizeWords (words : Array UInt64) (n : Nat) : coeffWords (normalizeWords words) n = coeffWords words n

Trailing-zero normalization preserves packed coefficients.

def Hex.GF2Poly.wordBitIsSet (w : UInt64) (i : Nat) : Bool

Equations

• Hex.GF2Poly.wordBitIsSet w i = (w >>> i.toUInt64 &&& 1 != 0)

def Hex.GF2Poly.highestSetBitBelow? (fuel : Nat) (w : UInt64) : Option Nat

Equations

• Hex.GF2Poly.highestSetBitBelow? 0 w = none
• Hex.GF2Poly.highestSetBitBelow? fuel'.succ w = if Hex.GF2Poly.wordBitIsSet w fuel' = true then some fuel' else Hex.GF2Poly.highestSetBitBelow? fuel' w

def Hex.GF2Poly.highestSetBit? (w : UInt64) : Option Nat

The index of the highest set bit in a machine word, if any.

Equations

• Hex.GF2Poly.highestSetBit? w = Hex.GF2Poly.highestSetBitBelow? 64 w

theorem Hex.GF2Poly.highestSetBit?_lt {w : UInt64} {i : Nat} (h : highestSetBit? w = some i) : i < 64

A returned highest-bit index is one of the 64 word-bit positions.

theorem Hex.GF2Poly.highestSetBit?_bit {w : UInt64} {i : Nat} (h : highestSetBit? w = some i) : (w >>> i.toUInt64 &&& 1 != 0) = true

A returned highest-bit index has its bit set in the word.

theorem Hex.GF2Poly.highestSetBit?_eq_none_bit {w : UInt64} {i : Nat} (h : highestSetBit? w = none) (hi : i < 64) : (w >>> i.toUInt64 &&& 1 != 0) = false

If no highest bit exists, every queried word bit is clear.

theorem Hex.GF2Poly.highestSetBit?_above_bit {w : UInt64} {i j : Nat} (h : highestSetBit? w = some i) (hj : j < 64) (hij : i < j) : (w >>> j.toUInt64 &&& 1 != 0) = false

Bits strictly above the reported highest set bit are clear.

theorem Hex.GF2Poly.highestSetBit?_oneHot {bit : Nat} (hbit : bit < 64) : highestSetBit? (1 <<< bit.toUInt64) = some bit

The one-hot word used by monomial has its highest set bit at the requested in-word position.

theorem Hex.GF2Poly.UInt64.bne_zero_eq_toNat_bne_zero (w : UInt64) : (w != 0) = (w.toNat != 0)

A machine word is != 0 exactly when its Nat value is != 0, transporting the word-level boolean inequality to the toNat image.

theorem Hex.GF2Poly.oneHotWord_bit_self {bit : Nat} (hbit : bit < 64) : (1 <<< bit.toUInt64 >>> bit.toUInt64 &&& 1 != 0) = true

Querying the one-hot word 1 <<< bit at position bit returns the bit it encodes.

theorem Hex.GF2Poly.oneHotWord_bit_ne {hot bit : Nat} (hhot : hot < 64) (hbit : bit < 64) (hne : hot ≠ bit) : (1 <<< hot.toUInt64 >>> bit.toUInt64 &&& 1 != 0) = false

Querying the one-hot word 1 <<< hot at any position other than hot returns a clear bit.

theorem Hex.GF2Poly.oneHotWord_ne_zero {bit : Nat} (hbit : bit < 64) : 1 <<< bit.toUInt64 ≠ 0

The one-hot word 1 <<< bit is nonzero whenever bit is a valid in-word position.

def Hex.GF2Poly.ofWords (words : Array UInt64) : GF2Poly

Build a normalized packed polynomial from a raw word array.

Equations

• Hex.GF2Poly.ofWords words = { words := Hex.GF2Poly.normalizeWords words, normalized := ⋯ }

@[simp]

theorem Hex.GF2Poly.words_ofWords_empty : (ofWords #[]).words = #[]

Wrapping the empty word array gives the empty packed representation.

def Hex.GF2Poly.zero : GF2Poly

The zero polynomial.

Equations

• Hex.GF2Poly.zero = Hex.GF2Poly.ofWords #[]

@[instance_reducible]

instance Hex.GF2Poly.instZero : Zero GF2Poly

Equations

• Hex.GF2Poly.instZero = { zero := Hex.GF2Poly.zero }

@[simp]

theorem Hex.GF2Poly.ofWords_empty : ofWords #[] = 0

The empty word array represents the zero polynomial.

def Hex.GF2Poly.one : GF2Poly

The constant polynomial 1.

Equations

• Hex.GF2Poly.one = Hex.GF2Poly.ofWords #[1]

@[instance_reducible]

instance Hex.GF2Poly.instOne : One GF2Poly

Equations

• Hex.GF2Poly.instOne = { one := Hex.GF2Poly.one }

def Hex.GF2Poly.ofUInt64 (w : UInt64) : GF2Poly

Build a packed polynomial from a single machine word.

Equations

• Hex.GF2Poly.ofUInt64 w = Hex.GF2Poly.ofWords #[w]

@[simp]

theorem Hex.GF2Poly.words_ofWords_single_zero : (ofWords #[0]).words = #[]

A single zero word normalizes to the empty packed representation.

@[simp]

theorem Hex.GF2Poly.words_ofWords_pair_zero : (ofWords #[0, 0]).words = #[]

A pair of zero words normalizes to the empty packed representation.

@[simp]

theorem Hex.GF2Poly.words_ofWords_single_nonzero {w : UInt64} (hw : w ≠ 0) : (ofWords #[w]).words = #[w]

A single nonzero word is already normalized and is its own packed representation.

def Hex.GF2Poly.monomial (n : Nat) : GF2Poly

The monomial x^n.

Equations

• Hex.GF2Poly.monomial n = Hex.GF2Poly.ofWords ((Array.replicate (n / 64) 0).push (1 <<< (n % 64).toUInt64))

def Hex.GF2Poly.toWords (p : GF2Poly) : Array UInt64

The stored packed words.

Equations

• p.toWords = p.words

def Hex.GF2Poly.wordCount (p : GF2Poly) : Nat

Number of stored machine words.

Equations

• p.wordCount = p.words.size

def Hex.GF2Poly.isZero (p : GF2Poly) : Bool

true exactly when the polynomial is zero.

Equations

• p.isZero = p.words.isEmpty

def Hex.GF2Poly.IsZero (p : GF2Poly) : Prop

Proposition-level zero predicate used by the packed quotient wrappers.

Equations

• p.IsZero = (p.isZero = true)

def Hex.GF2Poly.coeff (p : GF2Poly) (n : Nat) : Bool

The coefficient of x^n.

Equations

• p.coeff n = Hex.GF2Poly.coeffWords p.words n

@[simp]

theorem Hex.GF2Poly.coeff_ofWords (words : Array UInt64) (n : Nat) : (ofWords words).coeff n = coeffWords words n

Coefficients of a raw word array are unchanged by ofWords normalization.

theorem Hex.GF2Poly.coeff_ofUInt64_eq_testBit (w : UInt64) {i : Nat} (hi : i < 64) : (ofUInt64 w).coeff i = w.toNat.testBit i

Coefficients of a single-word polynomial are the corresponding machine-word bits.

theorem Hex.GF2Poly.coeff_ofUInt64_eq_false_of_ge_64 (w : UInt64) {i : Nat} (hi : 64 ≤ i) : (ofUInt64 w).coeff i = false

Coefficients above the low machine word vanish for a single-word polynomial.

@[simp]

theorem Hex.GF2Poly.ofUInt64_zero : ofUInt64 0 = 0

Input 0 to ofUInt64 is the zero polynomial.

@[simp]

theorem Hex.GF2Poly.ofUInt64_one : ofUInt64 1 = 1

Input 1 to ofUInt64 is the unit polynomial.

theorem Hex.GF2Poly.ofUInt64_injective : Function.Injective ofUInt64

The packed single-word constructor preserves the underlying machine word.

def Hex.GF2Poly.degree? (p : GF2Poly) : Option Nat

The degree of a nonzero polynomial, if any.

Equations

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

def Hex.GF2Poly.natDegree (p : GF2Poly) : Nat

The degree, with the zero polynomial given degree 0, matching DensePoly.natDegree.

Equations

• p.natDegree = p.degree?.getD 0

theorem Hex.GF2Poly.isZero_eq_true_iff_words_eq_empty (p : GF2Poly) : p.isZero = true ↔ p.words = #[]

A normalized packed polynomial is isZero iff its stored word array is empty.

This is the representation-level characterisation. It is kept out of the simp set, where it would compete with the propositional form below for the same left-hand side, but it keeps its grind trigger: grind = registers an E-matching theorem rather than an oriented rewrite, so two triggers on one term let congruence closure learn both consequences instead of racing.

theorem Hex.GF2Poly.isZero_eq_false_iff_words_ne_empty (p : GF2Poly) : p.isZero = false ↔ p.words ≠ #[]

A normalized packed polynomial is non-isZero iff its stored word array is nonempty. The representation-level counterpart of the propositional form below: out of simp for the same reason, and a grind trigger for the same reason.

@[simp]

theorem Hex.GF2Poly.isZero_iff_eq_zero (p : GF2Poly) : p.isZero = true ↔ p = 0

isZero agrees with propositional equality to the zero polynomial.

This is the simp normal form for a successful isZero check; the representation-level Hex.GF2Poly.isZero_eq_true_iff_words_eq_empty shares its left-hand side and is deliberately not a simp lemma.

@[simp]

theorem Hex.GF2Poly.isZero_eq_false_iff_ne_zero (p : GF2Poly) : p.isZero = false ↔ p ≠ 0

A failing isZero check agrees with propositional inequality to the zero polynomial. The simp normal form for a failing check, matching Hex.GF2Poly.isZero_iff_eq_zero on the successful one.

@[simp]

theorem Hex.GF2Poly.words_eq_empty_iff (p : GF2Poly) : p.words = #[] ↔ p = 0

An empty stored word array is exactly the zero polynomial.

The simp bridge from the representation to the propositional form, so that a goal stated about words and a goal stated about isZero reach the same normal form instead of sitting either side of the representation boundary.

theorem Hex.GF2Poly.eq_zero_of_isZero {p : GF2Poly} (h : p.isZero = true) : p = 0

A polynomial that runs the isZero Boolean check is propositionally zero.

theorem Hex.GF2Poly.isZero_of_eq_zero {p : GF2Poly} (h : p = 0) : p.isZero = true

The zero polynomial passes the isZero Boolean check.

theorem Hex.GF2Poly.degree?_eq_none_of_isZero {p : GF2Poly} (h : p.isZero = true) : p.degree? = none

The degree search returns none for any polynomial passing isZero.

theorem Hex.GF2Poly.isZero_false_of_degree?_eq_some {p : GF2Poly} {d : Nat} (h : p.degree? = some d) : p.isZero = false

A successful degree search certifies the polynomial is not isZero.

theorem Hex.GF2Poly.ne_zero_of_degree?_eq_some {p : GF2Poly} {d : Nat} (h : p.degree? = some d) : p ≠ 0

A successful degree search certifies the polynomial is not equal to zero.

theorem Hex.GF2Poly.natDegree_eq_of_degree?_eq_some {p : GF2Poly} {d : Nat} (h : p.degree? = some d) : p.natDegree = d

The default-0 degree extracts the witness of a successful degree search.

Not a simp lemma: its left-hand side p.natDegree does not determine d, so simp would have to guess the witness before it could discharge the hypothesis. Apply it to an explicit degree? equation instead.

theorem Hex.GF2Poly.degree?_eq_some_highestSetBit {p : GF2Poly} {d : Nat} (h : p.degree? = some d) : ∃ (last : UInt64), ∃ (bit : Nat), p.words.back? = some last ∧ highestSetBit? last = some bit ∧ d = 64 * (p.words.size - 1) + bit

Unpack a successful degree? computation into the normalized high word and the selected bit inside that word.

theorem Hex.GF2Poly.degree?_eq_some_bit_lt {p : GF2Poly} {d bit : Nat} {last : UInt64} (hparts : p.words.back? = some last ∧ highestSetBit? last = some bit ∧ d = 64 * (p.words.size - 1) + bit) : bit < 64

The in-word bit recovered from a successful degree? computation is a valid machine-word bit index.

theorem Hex.GF2Poly.degree?_eq_some_high_bit {p : GF2Poly} {d : Nat} (h : p.degree? = some d) : ∃ (last : UInt64), ∃ (bit : Nat), p.words.back? = some last ∧ highestSetBit? last = some bit ∧ (last >>> bit.toUInt64 &&& 1 != 0) = true ∧ d = 64 * (p.words.size - 1) + bit

A successful degree? computation points at a set bit in the high word.

theorem Hex.GF2Poly.degree?_isSome_of_isZero_false {p : GF2Poly} (h : p.isZero = false) : ∃ (d : Nat), p.degree? = some d

A nonzero normalized packed polynomial has a successful degree search.

theorem Hex.GF2Poly.coeff_eq_true_of_degree?_eq_some {p : GF2Poly} {d : Nat} (h : p.degree? = some d) : p.coeff d = true

A successful degree? computation points at a set global coefficient.

theorem Hex.GF2Poly.coeff_eq_false_of_degree?_lt {p : GF2Poly} {d n : Nat} (h : p.degree? = some d) (hdn : d < n) : p.coeff n = false

Every coefficient strictly above a successful degree? computation is clear.

theorem Hex.GF2Poly.degree?_eq_some_of_coeff_eq_true_of_forall_gt_false {p : GF2Poly} {n : Nat} (hset : p.coeff n = true) (hclear : ∀ (m : Nat), n < m → p.coeff m = false) : p.degree? = some n

If a coefficient is set and every higher coefficient is clear, the packed degree search returns exactly that coefficient index.

theorem Hex.GF2Poly.coeff_eq_false_of_wordCount_le (p : GF2Poly) {n : Nat} (h : p.wordCount ≤ n / 64) : p.coeff n = false

Coefficients outside the stored word range are clear.

theorem Hex.GF2Poly.wordCount_eq_of_coeff_eq {p q : GF2Poly} (hcoeff : ∀ (n : Nat), p.coeff n = q.coeff n) : p.wordCount = q.wordCount

Coefficientwise equality of normalized packed polynomials forces equal stored word counts.

theorem Hex.GF2Poly.ext_of_wordCount_eq {p q : GF2Poly} (hsize : p.wordCount = q.wordCount) (hcoeff : ∀ (n : Nat), p.coeff n = q.coeff n) : p = q

Extensionality for normalized packed polynomials when stored word counts agree and every packed coefficient agrees.

theorem Hex.GF2Poly.ext_of_wordCount_eq_iff {p q : GF2Poly} : p = q ↔ p.wordCount = q.wordCount ∧ ∀ (n : Nat), p.coeff n = q.coeff n

theorem Hex.GF2Poly.ext_coeff {p q : GF2Poly} (hcoeff : ∀ (n : Nat), p.coeff n = q.coeff n) : p = q

Extensionality for normalized packed polynomials by their coefficient functions.

@[simp]

theorem Hex.GF2Poly.words_zero : words 0 = #[]

The zero polynomial is canonically represented by the empty word array.

@[simp]

theorem Hex.GF2Poly.wordCount_zero : wordCount 0 = 0

The zero polynomial stores no machine words.

@[simp]

theorem Hex.GF2Poly.isZero_zero : isZero 0 = true

The zero polynomial passes the isZero Boolean check.

@[simp]

theorem Hex.GF2Poly.coeff_zero (n : Nat) : coeff 0 n = false

Every coefficient of the zero polynomial is clear.

@[simp]

theorem Hex.GF2Poly.degree?_zero : degree? 0 = none

The zero polynomial has no degree witness.

@[simp]

theorem Hex.GF2Poly.natDegree_zero : natDegree 0 = 0

The default-0 degree of the zero polynomial is 0.

@[inline]

def Hex.GF2Poly.xorWordsAux (short acc : Array UInt64) : Array UInt64

The in-place worker: fold over the shorter array's indices, XOR-ing each of its words into the accumulator (the longer array). Index i is read (a[i]!) before being written, and each index is written exactly once, so position i ends up as the original acc[i] XOR short[i].

Equations

• Hex.GF2Poly.xorWordsAux short acc = List.foldl (fun (a : Array UInt64) (i : Nat) => a.setIfInBounds i (a[i]! ^^^ short[i]!)) acc (List.range short.size)

@[simp]

theorem Hex.GF2Poly.xorWordsAux_empty (acc : Array UInt64) : xorWordsAux #[] acc = acc

@[inline]

def Hex.GF2Poly.xorWords (xs ys : Array UInt64) : Array UInt64

Word-wise XOR of packed coefficient arrays: copy the longer array and XOR the shorter array's words into its matching prefix in place. This does strictly less work than rebuilding max entries (only the min-prefix is touched, in place; the longer tail is left as-is) and, unlike Array.ofFn, reduces under decide.

Equations

• Hex.GF2Poly.xorWords xs ys = if xs.size ≤ ys.size then Hex.GF2Poly.xorWordsAux xs ys else Hex.GF2Poly.xorWordsAux ys xs

theorem Hex.GF2Poly.xorWordsFold_size (short : Array UInt64) (m : Nat) (acc : Array UInt64) : (List.foldl (fun (a : Array UInt64) (i : Nat) => a.setIfInBounds i (a[i]! ^^^ short[i]!)) acc (List.range m)).size = acc.size

The XOR fold preserves the accumulator's size.

theorem Hex.GF2Poly.xorWordsFold_getElem? (short : Array UInt64) (m : Nat) (acc : Array UInt64) (j : Nat) : (List.foldl (fun (a : Array UInt64) (i : Nat) => a.setIfInBounds i (a[i]! ^^^ short[i]!)) acc (List.range m))[j]? = if j < m ∧ j < acc.size then some (acc[j]! ^^^ short[j]!) else acc[j]?

Elementwise characterization of the XOR fold over List.range m: in-range positions are XOR-updated against the original accumulator; the rest unchanged.

theorem Hex.GF2Poly.xorWords_get?_getD (xs ys : Array UInt64) (i : Nat) : (xorWords xs ys)[i]?.getD 0 = xs[i]?.getD 0 ^^^ ys[i]?.getD 0

Optional raw XOR word lookup agrees with optional lookup from the two inputs.

@[simp]

theorem Hex.GF2Poly.xorWords_size (xs ys : Array UInt64) : (xorWords xs ys).size = max xs.size ys.size

Raw XOR output has one word for every word position present in either input.

theorem Hex.GF2Poly.xorWords_getD (xs ys : Array UInt64) (i : Nat) : (xorWords xs ys).getD i 0 = xs.getD i 0 ^^^ ys.getD i 0

Raw XOR word lookup agrees with defaulted lookup from the two inputs.

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

Addition in F_2[x] is coefficientwise XOR.

Equations

• p.add q = Hex.GF2Poly.ofWords (Hex.GF2Poly.xorWords p.words q.words)

@[instance_reducible]

instance Hex.GF2Poly.instAdd : Add GF2Poly

Equations

• Hex.GF2Poly.instAdd = { add := Hex.GF2Poly.add }

theorem Hex.GF2Poly.coeff_add (p q : GF2Poly) (n : Nat) : (p + q).coeff n = coeffWords (xorWords p.words q.words) n

Addition coefficients are the normalized packed XOR of the input words.

theorem Hex.GF2Poly.coeff_add_eq_bne (p q : GF2Poly) (n : Nat) : (p + q).coeff n = (p.coeff n != q.coeff n)

Addition over packed GF(2) polynomials is coefficientwise XOR.

theorem Hex.GF2Poly.ofUInt64_xor (a b : UInt64) : ofUInt64 (a ^^^ b) = ofUInt64 a + ofUInt64 b

The single-word constructor maps machine-word XOR to polynomial addition.

@[simp]

theorem Hex.GF2Poly.ofUInt64_add (a b : UInt64) : ofUInt64 a + ofUInt64 b = ofUInt64 (a ^^^ b)

Simp-facing packed addition law for single-word constructors.

@[simp]

theorem Hex.GF2Poly.coeff_add_bne (p q : GF2Poly) (n : Nat) : (p + q).coeff n = (p.coeff n != q.coeff n)

Simp-facing form of coefficientwise addition over packed GF(2) polynomials.

theorem Hex.GF2Poly.coeff_add_of_true_true {p q : GF2Poly} {n : Nat} (hp : p.coeff n = true) (hq : q.coeff n = true) : (p + q).coeff n = false

Equal set coefficients cancel under GF(2) addition.

theorem Hex.GF2Poly.coeff_add_of_true_false {p q : GF2Poly} {n : Nat} (hp : p.coeff n = true) (hq : q.coeff n = false) : (p + q).coeff n = true

A set left coefficient and clear right coefficient remain set under GF(2) addition.

theorem Hex.GF2Poly.coeff_add_of_false_true {p q : GF2Poly} {n : Nat} (hp : p.coeff n = false) (hq : q.coeff n = true) : (p + q).coeff n = true

A clear left coefficient and set right coefficient remain set under GF(2) addition.

theorem Hex.GF2Poly.coeff_add_of_false_false {p q : GF2Poly} {n : Nat} (hp : p.coeff n = false) (hq : q.coeff n = false) : (p + q).coeff n = false

Clear coefficients remain clear under GF(2) addition.

theorem Hex.GF2Poly.xorWords_self_getD (xs : Array UInt64) (i : Nat) : (xorWords xs xs).getD i 0 = 0

Raw packed addition cancels each word against itself.

theorem Hex.GF2Poly.coeffWords_xorWords_self (xs : Array UInt64) (n : Nat) : coeffWords (xorWords xs xs) n = false

Coefficient lookup sees the raw packed sum of an array with itself as zero.

theorem Hex.GF2Poly.coeff_add_self (p : GF2Poly) (n : Nat) : (p + p).coeff n = false

Every packed coefficient of p + p is zero in characteristic two.

@[simp]

theorem Hex.GF2Poly.coeff_add_self_false (p : GF2Poly) (n : Nat) : (p + p).coeff n = false

Simp-facing coefficient form of characteristic-two self-cancellation.

theorem Hex.GF2Poly.normalizeWords_replicate_zero (n : Nat) : normalizeWords (Array.replicate n 0) = #[]

Normalization wipes an all-zero packed word array down to the canonical empty array.

theorem Hex.GF2Poly.xorWords_self (xs : Array UInt64) : xorWords xs xs = Array.replicate xs.size 0

Raw packed XOR of a word array with itself produces the all-zero array of the same size.

@[simp]

theorem Hex.GF2Poly.add_self (p : GF2Poly) : p + p = 0

Every element of F_2[x] is its own additive inverse: p + p = 0.

def Hex.GF2Poly.neg (p : GF2Poly) : GF2Poly

Negation in F_2[x] is the identity: characteristic two makes every element its own additive inverse. Present so that the additive group structure can be named, not because it computes anything.

Equations

• p.neg = p

@[instance_reducible]

instance Hex.GF2Poly.instNeg : Neg GF2Poly

Equations

• Hex.GF2Poly.instNeg = { neg := Hex.GF2Poly.neg }

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

Subtraction in F_2[x] coincides with addition.

Equations

• p.sub q = p.add q

@[instance_reducible]

instance Hex.GF2Poly.instSub : Sub GF2Poly

Equations

• Hex.GF2Poly.instSub = { sub := Hex.GF2Poly.sub }

@[simp]

theorem Hex.GF2Poly.neg_eq_self (p : GF2Poly) : -p = p

Negation is the identity.

@[simp]

theorem Hex.GF2Poly.sub_eq_add (p q : GF2Poly) : p - q = p + q

Subtraction is addition.

@[simp]

theorem Hex.GF2Poly.neg_add_cancel (p : GF2Poly) : -p + p = 0

Every element cancels against its negation, which in characteristic two is itself.

@[simp]

theorem Hex.GF2Poly.zero_add (p : GF2Poly) : 0 + p = p

Zero is the left identity for F_2[x] addition.

@[simp]

theorem Hex.GF2Poly.coeff_add_zero_left_bool (p : GF2Poly) (n : Nat) : (0 + p).coeff n = p.coeff n

Adding zero on the left leaves packed GF(2) coefficients unchanged.

@[simp]

theorem Hex.GF2Poly.coeff_add_zero_right_bool (p : GF2Poly) (n : Nat) : (p + 0).coeff n = p.coeff n

Adding zero on the right leaves packed GF(2) coefficients unchanged.

@[simp]

theorem Hex.GF2Poly.add_zero (p : GF2Poly) : p + 0 = p

Zero is the right identity for F_2[x] addition.

theorem Hex.GF2Poly.add_comm (p q : GF2Poly) : p + q = q + p

Packed F_2[x] addition is commutative.

theorem Hex.GF2Poly.add_assoc (p q r : GF2Poly) : p + q + r = p + (q + r)

Packed F_2[x] addition is associative.

@[simp]

theorem Hex.GF2Poly.add_add_cancel_left (p q : GF2Poly) : p + (p + q) = q

Adding p twice on the left cancels: p + (p + q) = q.

@[simp]

theorem Hex.GF2Poly.add_add_cancel_right (p q : GF2Poly) : p + q + q = p

Adding q twice on the right cancels: (p + q) + q = p.

def Hex.GF2Poly.shiftLeftBitsList (bitShift : Nat) (carry : UInt64) : List UInt64 → List UInt64

Shift a normalized word list left by bitShift ∈ [1, 63].

Equations

• Hex.GF2Poly.shiftLeftBitsList bitShift carry [] = if carry = 0 then [] else [carry]
• Hex.GF2Poly.shiftLeftBitsList bitShift carry (w :: ws) = (w <<< bitShift.toUInt64 ||| carry) :: Hex.GF2Poly.shiftLeftBitsList bitShift (w >>> (64 - bitShift).toUInt64) ws

theorem Hex.GF2Poly.coeffWords_shiftLeftBitsList_same_word (words : Array UInt64) {shift n : Nat} (hshiftPos : 0 < shift) (hshift : shift < 64) (hword : n / 64 < words.size) (hbit : n % 64 + shift < 64) : coeffWords (shiftLeftBitsList shift 0 words.toList).toArray (n + shift) = coeffWords words n

Sub-word shiftLeftBitsList preserves the source coefficient when the shifted bit stays inside the same machine word.

theorem Hex.GF2Poly.coeffWords_shiftLeftBitsList_carry_word (words : Array UInt64) {shift n : Nat} (hshiftPos : 0 < shift) (hshift : shift < 64) (hword : n / 64 < words.size) (hbit : 64 ≤ n % 64 + shift) : coeffWords (shiftLeftBitsList shift 0 words.toList).toArray (n + shift) = coeffWords words n

Sub-word shiftLeftBitsList preserves the source coefficient when the shifted bit crosses into the next machine word.

theorem Hex.GF2Poly.coeffWords_shiftLeftBitsList_add (words : Array UInt64) {shift n : Nat} (hshiftPos : 0 < shift) (hshift : shift < 64) (hword : n / 64 < words.size) : coeffWords (shiftLeftBitsList shift 0 words.toList).toArray (n + shift) = coeffWords words n

Sub-word shiftLeftBitsList preserves every source coefficient stored in the input words.

theorem Hex.GF2Poly.coeffWords_replicate_append_shiftLeftBitsList_add (words : Array UInt64) {k n : Nat} (hbitShift : k % 64 ≠ 0) (hword : n / 64 < words.size) : coeffWords (Array.replicate (k / 64) 0 ++ (shiftLeftBitsList (k % 64) 0 words.toList).toArray) (n + k) = coeffWords words n

The full shift-left assembly preserves the source coefficient at every in-bounds index when the bit-shift component is nonzero.

theorem Hex.GF2Poly.coeffWords_replicate_append_add_of_mod_eq_zero (words : Array UInt64) {k n : Nat} (hbitShift : k % 64 = 0) : coeffWords (Array.replicate (k / 64) 0 ++ words) (n + k) = coeffWords words n

A word-aligned shift-left assembly preserves every source coefficient (no in-word bit shift is needed).

theorem Hex.GF2Poly.coeffWords_replicate_append_shiftLeftBitsList_add_of_not_word (words : Array UInt64) {k n : Nat} (hbitShift : k % 64 ≠ 0) (hword : ¬n / 64 < words.size) : coeffWords (Array.replicate (k / 64) 0 ++ (shiftLeftBitsList (k % 64) 0 words.toList).toArray) (n + k) = false

The full shift-left assembly returns a clear coefficient at any index whose source word lies above the stored input.

theorem Hex.GF2Poly.coeffWords_replicate_append_shiftLeftBitsList_lt (words : Array UInt64) {k n : Nat} (_hbitShift : k % 64 ≠ 0) (hn : n < k) : coeffWords (Array.replicate (k / 64) 0 ++ (shiftLeftBitsList (k % 64) 0 words.toList).toArray) n = false

The full shift-left assembly returns a clear coefficient strictly below the shift amount: indices below k are zero-padded.

def Hex.GF2Poly.shiftRightBitsRevList (bitShift : Nat) (carry : UInt64) : List UInt64 → List UInt64

Shift packed words right by bitShift ∈ [1, 63], reading the input from high degree to low degree.

Equations

• Hex.GF2Poly.shiftRightBitsRevList bitShift carry [] = []
• Hex.GF2Poly.shiftRightBitsRevList bitShift carry (w :: ws) = (w >>> bitShift.toUInt64 ||| carry) :: Hex.GF2Poly.shiftRightBitsRevList bitShift (w <<< (64 - bitShift).toUInt64) ws

def Hex.GF2Poly.shiftLeft (p : GF2Poly) (k : Nat) : GF2Poly

Multiply by x^k.

Equations

• p.shiftLeft k = Hex.GF2Poly.ofWords (Array.replicate (k / 64) 0 ++ if k % 64 = 0 then p.words else (Hex.GF2Poly.shiftLeftBitsList (k % 64) 0 p.words.toList).toArray)

def Hex.GF2Poly.shiftRight (p : GF2Poly) (k : Nat) : GF2Poly

Divide by x^k, discarding the remainder.

Equations

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

def Hex.GF2Poly.mulXk (p : GF2Poly) (k : Nat) : GF2Poly

Alias for multiplication by a power of x.

Equations

• p.mulXk k = p.shiftLeft k

theorem Hex.GF2Poly.coeff_monomial (n m : Nat) : (monomial n).coeff m = coeffWords ((Array.replicate (n / 64) 0).push (1 <<< (n % 64).toUInt64)) m

Monomial coefficients reduce to the coefficient lookup on its packed word array.

@[simp]

theorem Hex.GF2Poly.coeff_monomial_self (n : Nat) : (monomial n).coeff n = true

The coefficient of the defining degree of a monomial is set.

theorem Hex.GF2Poly.words_monomial (n : Nat) : (monomial n).words = (Array.replicate (n / 64) 0).push (1 <<< (n % 64).toUInt64)

The normalized storage of a monomial is its zero prefix plus one nonzero one-hot word.

theorem Hex.GF2Poly.coeff_monomial_ne {n m : Nat} (h : m ≠ n) : (monomial n).coeff m = false

Coefficients away from the defining degree of a monomial are clear.

@[simp]

theorem Hex.GF2Poly.degree?_monomial (n : Nat) : (monomial n).degree? = some n

The packed degree search recovers the degree of a monomial.

@[simp]

theorem Hex.GF2Poly.natDegree_monomial (n : Nat) : (monomial n).natDegree = n

The default-0 degree of the monomial x^n is n.

@[simp]

theorem Hex.GF2Poly.degree?_one : degree? 1 = some 0

The unit polynomial 1 has degree witness 0. Proved through the single-word coefficient API rather than by kernel reduction, since the UInt64 bit search in degree? does not reduce definitionally under the module system.

@[simp]

theorem Hex.GF2Poly.natDegree_one : natDegree 1 = 0

The unit polynomial 1 has degree 0.

@[simp]

theorem Hex.GF2Poly.isZero_monomial_eq_false (n : Nat) : (monomial n).isZero = false

The monomial x^n is never the zero polynomial.

@[simp]

theorem Hex.GF2Poly.monomial_ne_zero (n : Nat) : monomial n ≠ 0

The monomial x^n is distinct from the zero polynomial.

@[simp]

theorem Hex.GF2Poly.coeff_shiftLeft (p : GF2Poly) (k n : Nat) : (p.shiftLeft k).coeff n = coeffWords (Array.replicate (k / 64) 0 ++ if k % 64 = 0 then p.words else (shiftLeftBitsList (k % 64) 0 p.words.toList).toArray) n

Shift-left coefficients reduce to the coefficient lookup on the shifted packed words.

theorem Hex.GF2Poly.coeff_shiftLeft_add_of_word_lt (p : GF2Poly) {k n : Nat} (hword : n / 64 < p.words.size) : (p.shiftLeft k).coeff (n + k) = p.coeff n

Shifting left by k moves every source coefficient at n to n + k when the source coefficient lies in a stored word.

@[simp]

theorem Hex.GF2Poly.coeff_mulXk (p : GF2Poly) (k n : Nat) : (p.mulXk k).coeff n = (p.shiftLeft k).coeff n

mulXk is coefficientwise the same as shiftLeft.

theorem Hex.GF2Poly.degree?_mulXk_of_degree?_eq_some {p : GF2Poly} {d k : Nat} (h : p.degree? = some d) : (p.mulXk k).degree? = some (d + k)

Multiplication by x^k shifts the degree of a nonzero packed polynomial.

theorem Hex.GF2Poly.coeff_mulXk_degree_add {p : GF2Poly} {d k : Nat} (h : p.degree? = some d) : (p.mulXk k).coeff (d + k) = true

The shifted leading coefficient of p.mulXk k is set.

theorem Hex.GF2Poly.coeff_mulXk_division_step {q : GF2Poly} {rd qd : Nat} (hq : q.degree? = some qd) (hrd : ¬rd < qd) : (q.mulXk (rd - qd)).coeff rd = true

In a long-division step, shifting the divisor by rd - qd aligns its leading coefficient with the current remainder degree.

theorem Hex.GF2Poly.coeff_division_step_cancel {rem q : GF2Poly} {rd qd : Nat} (hrem : rem.degree? = some rd) (hq : q.degree? = some qd) (hrd : ¬rd < qd) : (rem + q.mulXk (rd - qd)).coeff rd = false

The leading coefficient cancels after the characteristic-two subtraction step used by long division.

theorem Hex.GF2Poly.division_step_degree_lt {rem q : GF2Poly} {rd qd : Nat} (hrem : rem.degree? = some rd) (hq : q.degree? = some qd) (hrd : ¬rd < qd) : (rem + q.mulXk (rd - qd)).isZero = true ∨ (rem + q.mulXk (rd - qd)).natDegree < rd

A non-terminal long-division subtraction step strictly lowers the remainder degree.

def Hex.GF2Poly.divXk (p : GF2Poly) (k : Nat) : GF2Poly

Alias for exact division by a power of x when the low coefficients vanish; otherwise this drops the discarded remainder.

Equations

• p.divXk k = p.shiftRight k

theorem Hex.GF2Poly.normalizeWords_size_le (words : Array UInt64) : (normalizeWords words).size ≤ words.size

Normalization never increases the number of stored machine words.

theorem Hex.GF2Poly.wordCount_ofWords_le (words : Array UInt64) : (ofWords words).wordCount ≤ words.size

Wrapping raw words never increases the stored word count.

theorem Hex.GF2Poly.wordCount_add_le (p q : GF2Poly) : (p + q).wordCount ≤ max p.wordCount q.wordCount

Addition stores no more words than the larger input.

theorem Hex.GF2Poly.wordCount_monomial_le (n : Nat) : (monomial n).wordCount ≤ n / 64 + 1

The monomial x^n stores at most the one word containing its bit.