def Hex.GF2Poly.xPowSubX (k : Nat) : GF2Poly

The absolute polynomial X^(2^k) - X in characteristic two.

Packed GF(2) subtraction is addition, so this is represented as X^(2^k) + X.

Equations

• Hex.GF2Poly.xPowSubX k = Hex.GF2Poly.monomial (2 ^ k) + Hex.GF2Poly.monomial 1

theorem Hex.GF2Poly.dvd_xPowSubX_iff_frobeniusDiffMod_isZero (f : GF2Poly) (k : Nat) : f ∣ xPowSubX k ↔ (f.frobeniusDiffMod k).isZero = true

The executable Frobenius remainder vanishes exactly when f divides the absolute Rabin polynomial X^(2^k) - X.

This is the GF2 counterpart of the absolute-to-modular identity used by the generic Berlekamp Rabin soundness proof.

theorem Hex.GF2Poly.xpow2kMod_eq_modX_at_degree {g : GF2Poly} (hg_irr : g.Irreducible) (hg_pos : 0 < g.natDegree) : g.xpow2kMod g.natDegree = monomial 1 % g

Backward Rabin algebraic content packaged at the executable level.

For an irreducible packed polynomial g of positive degree d, the iterated-squaring chain xpow2kMod g d returns to the residue class of X. Equivalently, the residue field element X mod g is fixed by the d-fold Frobenius endomorphism α ↦ α^(2^d) — the standard Fermat–Euler statement for the residue field F_2[X]/(g) (which has 2^d elements when g is irreducible).

This is the deepest finite-field ingredient of Rabin's test: once it is available, irreducible_dvd_xPowSubX_degree follows by char-2 cancellation.

theorem Hex.GF2Poly.irreducible_dvd_xPowSubX_degree {g : GF2Poly} (hg_irr : g.Irreducible) (hg_pos : 0 < g.natDegree) : g ∣ xPowSubX g.natDegree

Backward Rabin degree theorem for packed GF2 polynomials.

An irreducible g of degree d > 0 divides X^(2^d) - X. The proof combines char-2 cancellation with xpow2kMod_eq_modX_at_degree, which carries the residue-field Fermat–Euler argument.

theorem Hex.GF2Poly.xPowSubX_dvd_of_dvd {d m : Nat} (hdvd : d ∣ m) : xPowSubX d ∣ xPowSubX m

Divisibility chain on Rabin polynomials: if d ∣ m, then X^(2^d) - X divides X^(2^m) - X.

theorem Hex.GF2Poly.exists_maximalProperDivisor_dvd {n d : Nat} (hd_pos : 0 < d) (hd_dvd : d ∣ n) (hd_lt : d < n) : ∃ (m : Nat), m ∈ maximalProperDivisors n ∧ d ∣ m

Every positive proper divisor of n is contained in a maximal proper divisor of n.

This routes an irreducible factor degree to one of the gcd legs checked by rabinTest.

theorem Hex.GF2Poly.dvd_frobeniusDiffMod_of_dvd_dvd {f g : GF2Poly} (hg_dvd_f : g ∣ f) {k : Nat} (hg_dvd_pow : g ∣ xPowSubX k) : g ∣ f.frobeniusDiffMod k

A common divisor of f and the absolute Rabin polynomial also divides the modular Frobenius remainder used by the executable test.

theorem Hex.GF2Poly.isUnitPolynomial_of_dvd_isUnitPolynomial {g h : GF2Poly} (hgh : g ∣ h) (hh : h.isUnitPolynomial = true) : g.isUnitPolynomial = true

A divisor of a unit polynomial is a unit polynomial.

For packed GF2 this is a degree argument over the executable divisibility relation.

theorem Hex.GF2Poly.ne_zero_of_pos_degree {f : GF2Poly} (hpos : 0 < f.natDegree) : f ≠ 0

A polynomial of positive degree is nonzero.

theorem Hex.GF2Poly.dvd_xPowSubX_iff_quotient_X_frobeniusIter_eq_X {g : GF2Poly} (hg_irr : g.Irreducible) (hg_pos : 0 < g.natDegree) (k : Nat) : g ∣ xPowSubX k ↔ GF2nPoly.X.frobeniusIter k = GF2nPoly.X

Rabin divisibility is equivalent to the quotient class of X being fixed by k iterated Frobenius squarings in GF2nPoly g hg_irr.

This is the packed quotient identity used by the finite-field part of Rabin soundness: absolute divisibility by X^(2^k) - X is the same as X^(2^k) = X in the quotient by g.

theorem Hex.GF2Poly.quotient_X_frobenius_fixed_iff_degree_dvd {g : GF2Poly} (hg_irr : g.Irreducible) (hg_pos : 0 < g.natDegree) {n : Nat} (hfixed : GF2nPoly.X.frobeniusIter n = GF2nPoly.X) : g.natDegree ∣ n

If the quotient class of X is fixed by the n-fold Frobenius squaring in GF2[x]/(g), then the irreducible modulus degree divides n.

This is the quotient-facing period statement used by the Rabin soundness orchestration layer; the divisibility/equality translation stays centralized in dvd_xPowSubX_iff_quotient_X_frobeniusIter_eq_X.

theorem Hex.GF2Poly.natDegree_dvd_of_irreducible_dvd_xPowSubX {g : GF2Poly} (hg_irr : g.Irreducible) (hg_pos : 0 < g.natDegree) {n : Nat} (hg_dvd : g ∣ xPowSubX n) : g.natDegree ∣ n

Forward Rabin degree theorem for packed GF2 polynomials.

If an irreducible g of positive degree divides X^(2^n) - X, then deg g divides n.

theorem Hex.GF2Poly.factor_ne_zero_of_ne_zero {f a b : GF2Poly} (hab : a * b = f) (hf_ne_zero : f ≠ 0) : a ≠ 0

The left factor in a factorization of a nonzero polynomial is nonzero.

theorem Hex.GF2Poly.pos_degree_of_ne_zero_of_not_degree_zero {a : GF2Poly} (_ha_ne_zero : a ≠ 0) (ha_not_unit : a.natDegree ≠ 0) : 0 < a.natDegree

A nonzero polynomial whose degree is not zero has positive degree.

theorem Hex.GF2Poly.factor_degree_lt {f a b : GF2Poly} (hab : a * b = f) (ha_ne_zero : a ≠ 0) (hb_pos : 0 < b.natDegree) : a.natDegree < f.natDegree

The degree of a factor a is strictly less than the degree of f whenever the cofactor b has positive degree.

theorem Hex.GF2Poly.isUnitPolynomial_eq_false_of_pos_degree {g : GF2Poly} (hpos : 0 < g.natDegree) : g.isUnitPolynomial = false

A positive-degree polynomial is not a unit polynomial.

theorem Hex.GF2Poly.rabinCoprimeTest_of_mem_maximalProperDivisors (f : GF2Poly) (hwitnesses : f.rabinWitnesses.all Prod.snd = true) {m : Nat} (hm : m ∈ maximalProperDivisors f.natDegree) : f.rabinCoprimeTest m = true

The m-th maximal-proper-divisor witness of rabinTest: if the test passes, the gcd leg holds at every maximal proper divisor.

theorem Hex.GF2Poly.isUnitPolynomial_of_dvd_gcd_isUnit {f q g : GF2Poly} (hgf : g ∣ f) (hgq : g ∣ q) (hgcd : (f.gcd q).isUnitPolynomial = true) : g.isUnitPolynomial = true

If gcd(f, q) is a unit polynomial and g divides both f and q, then g is itself a unit polynomial.

theorem Hex.GF2Poly.exists_irreducible_factor_of_factor {f a b : GF2Poly} (_hab : a * b = f) (ha_pos : 0 < a.natDegree) : ∃ (g : GF2Poly), g.Irreducible ∧ g ∣ a ∧ 0 < g.natDegree ∧ g.natDegree ≤ a.natDegree

Every nonconstant factor of a packed GF2 polynomial has an irreducible factor.

The proof is the usual descent on degree, specialized to the project-side GF2Poly.Irreducible predicate and the packed divisibility relation. The hypothesis a * b = f is irrelevant to the construction; descent operates purely on a via strong induction on a.natDegree.

theorem Hex.GF2Poly.rabinTest_imp_irreducible (f : GF2Poly) (hrabin : f.rabinTest = true) : f.Irreducible

Soundness of the executable Rabin test against Hex.GF2Poly.Irreducible.

The proof decomposes the Boolean test, picks an irreducible factor of any nontrivial factorization, routes its degree through a maximal proper divisor, and contradicts the corresponding gcd leg.

theorem Hex.GF2Poly.checkIrreducibilityCertificate_imp_irreducible (f : GF2Poly) (cert : IrreducibilityCertificate) (hcheck : f.checkIrreducibilityCertificate cert = true) : f.Irreducible

Accepted executable irreducibility certificates imply project-side GF2Poly.Irreducible, composing checker soundness with Rabin soundness.

theorem Hex.GF2Poly.checkIrreducibilityCertificateLinear_imp_irreducible (f : GF2Poly) (cert : IrreducibilityCertificate) (hcheck : f.checkIrreducibilityCertificateLinear cert = true) : f.Irreducible

The linear-time variant of the certificate checker also implies project-side GF2Poly.Irreducible, composing the linear soundness theorem with Rabin soundness.