Computable arithmetic for monic quotient presentations

ExtensionParams F stores the degree, lower modulus coefficients and an explicit inverse-exponent parameter q. Ext P is one nominal carrier with coefficient vectors in ascending degree order. Its coordinate maps require no algebraic structure; arithmetic uses a ring of coefficients. The presentation index separates parameter values for a fixed coefficient algebra. Operations and their theorems are relative to the supplied ring or field structure on F; the raw carrier does not separate alternative algebra structures on that same type. Distinct coefficient presentations should use nominal coefficient types and explicit ring maps. The polynomial quotient interpretation uses commutative coefficients; the raw formulas are defined for any ring.

Multiplication reduces monomials with shiftReduce. The executable reduction-table implementation mulTbl is connected to mul by mul_eq_mulTbl. Power uses binary exponentiation, and the canonical inverse candidate uses the literal exponent q^d - 2.

This module supplies no cardinality or irreducibility certificate. Polynomial specifications and quotient correspondence belong to Extension/Defs.lean and Extension/Bridge.lean; certified field laws belong to Extension/Field.lean. Raw parameters with an incorrect q still admit arithmetic but do not thereby acquire field laws. The binomial conversion describes the modulus X^d - W.

structure CompPoly.Extension.ExtensionParams (F : Type u_2) : Type u_2

The data defining an extension F[X] / f by a monic modulus f of degree d.

The modulus is stored by its d lower coefficients: f = X^d + ∑_{i < d} lower[i] · X^i. The leading coefficient is an implicit 1, so f is monic by construction.

Irreducibility is not part of these parameters: the quotient is a commutative ring for every monic modulus over a commutative ring. Field laws additionally require finite-cardinality and irreducibility certificates.

• d : ℕ

  The degree of the extension.

• two_le : 2 ≤ self.d

  Degree at least two; a degree-one "extension" is just F.

• lower : Vector F self.d

  The lower coefficients of the monic modulus, little-endian: lower[i] is the coefficient of X^i in poly, for i < d. The coefficient of X^d is an implicit 1.

• q : ℕ

  The proposed base cardinality, stored explicitly for the inverse exponent.

  Raw arithmetic does not certify this value. Field laws require a separate proof that Nat.card F = q, together with finiteness and irreducibility.

@[inline]

def CompPoly.Extension.ExtensionParams.lowerCoeff {F : Type u_1} (P : ExtensionParams F) (i : Fin P.d) : F

The coefficient of X^i in the lower part of the modulus.

def CompPoly.Extension.ExtensionParams.lowerCoeffNat {F : Type u_1} [Ring F] (P : ExtensionParams F) (k : ℕ) : F

The lower modulus coefficient at index k, or zero when P.d ≤ k.

@[simp]

theorem CompPoly.Extension.ExtensionParams.lowerCoeffNat_coe {F : Type u_1} [Ring F] (P : ExtensionParams F) (i : Fin P.d) : P.lowerCoeffNat ↑i = P.lowerCoeff i

theorem CompPoly.Extension.ExtensionParams.lowerCoeffNat_of_ge {F : Type u_1} [Ring F] (P : ExtensionParams F) {k : ℕ} (h : P.d ≤ k) : P.lowerCoeffNat k = 0

theorem CompPoly.Extension.ExtensionParams.d_pos {F : Type u_1} (P : ExtensionParams F) : 0 < P.d

structure CompPoly.Extension.Ext {F : Type u_2} (P : ExtensionParams F) : Type u_2

The carrier of the quotient by the monic modulus in P, with coefficients in ascending order of powers. The parameter remains part of the type even when two moduli have equal degree.

• coeffs : Vector F P.d

  The coefficient of X^i is stored at index i.

@[inline]

def CompPoly.Extension.Ext.ofVector {F : Type u_1} {P : ExtensionParams F} (v : Vector F P.d) : Ext P

Build an element from coefficients in ascending order of powers.

@[simp]

theorem CompPoly.Extension.Ext.coeffs_ofVector {F : Type u_1} {P : ExtensionParams F} (v : Vector F P.d) : (ofVector v).coeffs = v

Extracting the coefficients of a constructed element returns the input vector.

@[simp]

theorem CompPoly.Extension.Ext.ofVector_coeffs {F : Type u_1} {P : ExtensionParams F} (x : Ext P) : ofVector x.coeffs = x

Reconstructing an element from its coefficient vector returns that element.

theorem CompPoly.Extension.Ext.coeffs_injective {F : Type u_1} {P : ExtensionParams F} : Function.Injective coeffs

The coefficient vector uniquely determines an element.

@[inline]

def CompPoly.Extension.Ext.ofFn {F : Type u_1} {P : ExtensionParams F} (g : Fin P.d → F) : Ext P

Build an element from a coefficient function.

@[inline]

def CompPoly.Extension.Ext.coeff {F : Type u_1} {P : ExtensionParams F} (x : Ext P) (i : Fin P.d) : F

The coefficient of X^i.

@[simp]

theorem CompPoly.Extension.Ext.coeff_ofFn {F : Type u_1} {P : ExtensionParams F} (g : Fin P.d → F) (i : Fin P.d) : (ofFn g).coeff i = g i

theorem CompPoly.Extension.Ext.ext {F : Type u_1} {P : ExtensionParams F} {x y : Ext P} (h : ∀ (i : Fin P.d), x.coeff i = y.coeff i) : x = y

Two elements with the same coefficients are equal.

theorem CompPoly.Extension.Ext.ext_iff {F : Type u_1} {P : ExtensionParams F} {x y : Ext P} : x = y ↔ ∀ (i : Fin P.d), x.coeff i = y.coeff i

theorem CompPoly.Extension.Ext.ofFn_coeff {F : Type u_1} {P : ExtensionParams F} (x : Ext P) : ofFn x.coeff = x

def CompPoly.Extension.Ext.equivFn {F : Type u_1} (P : ExtensionParams F) : Ext P ≃ (Fin P.d → F)

Coefficient vectors are exactly functions out of Fin d.

def CompPoly.Extension.Ext.coeffNat {F : Type u_1} [Ring F] {P : ExtensionParams F} (x : Ext P) (i : ℕ) : F

The coefficient at index i, or zero when P.d ≤ i.

@[simp]

theorem CompPoly.Extension.Ext.coeffNat_coe {F : Type u_1} [Ring F] {P : ExtensionParams F} (x : Ext P) (i : Fin P.d) : x.coeffNat ↑i = x.coeff i

theorem CompPoly.Extension.Ext.coeffNat_of_lt {F : Type u_1} [Ring F] {P : ExtensionParams F} (x : Ext P) {i : ℕ} (h : i < P.d) : x.coeffNat i = x.coeff ⟨i, h⟩

theorem CompPoly.Extension.Ext.coeffNat_of_ge {F : Type u_1} [Ring F] {P : ExtensionParams F} (x : Ext P) {i : ℕ} (h : P.d ≤ i) : x.coeffNat i = 0

Distinguished elements

ofBase places a coefficient-ring element in the constant coordinate, and gen has the coordinates of X. The quotient bridge over a field promotes the constant embedding to an Algebra structure and identifies the reduced power gen ^ d with monomialMod d.

@[inline]

def CompPoly.Extension.Ext.ofBase {F : Type u_1} [Ring F] {P : ExtensionParams F} (c : F) : Ext P

Place a coefficient-ring element in the constant coordinate.

def CompPoly.Extension.Ext.gen {F : Type u_1} [Ring F] {P : ExtensionParams F} : Ext P

The coordinate vector with coefficient one at X and zero elsewhere.

Operations

Multiplication is defined in terms of shiftReduce — the "multiply by X, reduce mod f" map — whose iterates monomialMod k = shiftReduce^[k] 1 are the reduced monomials X^k mod f. Everything downstream is proved from the single homomorphism law toQuot (shiftReduce e) = rt * toQuot e.

@[instance_reducible]

instance CompPoly.Extension.Ext.instZero {F : Type u_1} [Ring F] {P : ExtensionParams F} : Zero (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instOne {F : Type u_1} [Ring F] {P : ExtensionParams F} : One (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instAdd {F : Type u_1} [Ring F] {P : ExtensionParams F} : Add (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instNeg {F : Type u_1} [Ring F] {P : ExtensionParams F} : Neg (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instSub {F : Type u_1} [Ring F] {P : ExtensionParams F} : Sub (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instSMul {F : Type u_1} [Ring F] {P : ExtensionParams F} : SMul F (Ext P)

def CompPoly.Extension.Ext.shiftReduce {F : Type u_1} [Ring F] {P : ExtensionParams F} (e : Ext P) : Ext P

Multiply by X and reduce modulo f.

X · (∑ eᵢ Xⁱ) = ∑ eᵢ X^(i+1), whose top term e_{d-1} X^d wraps via X^d = -∑ lowerₘ Xᵐ. So coefficient m of the reduced result is e_{m-1} - e_{d-1} · lowerₘ, with e_{-1} = 0. This is the single linear map whose iterates build the reduction table red.

def CompPoly.Extension.Ext.monomialMod {F : Type u_1} [Ring F] {P : ExtensionParams F} (k : ℕ) : Ext P

The reduced form of X^k modulo f, obtained by iterating shiftReduce (multiply by X, reduce) k times from 1 = X^0. Its image under toQuot is rt ^ k.

@[inline, specialize #[]]

def CompPoly.Extension.Ext.mul {F : Type u_1} [Ring F] {P : ExtensionParams F} (x y : Ext P) : Ext P

The monic-reduction product formula, representing multiplication in F[X] / f when the coefficient ring is commutative.

Each product monomial Xⁱ⁺ʲ is reduced modulo f by monomialMod (i + j), so coefficient m of the product collects xᵢ · yⱼ · [X^(i+j) mod f]ₘ over all pairs (i, j).

def CompPoly.Extension.Ext.redScan {F : Type u_1} [Ring F] {P : ExtensionParams F} : ℕ → Ext P → Array (Ext P) → Array (Ext P)

Append cur, shiftReduce cur, …, n entries in all, to acc; the scan that builds red. This is the table the shiftReduce docstring above refers to.

theorem CompPoly.Extension.Ext.redScan_size {F : Type u_1} [Ring F] {P : ExtensionParams F} (n : ℕ) (cur : Ext P) (acc : Array (Ext P)) : (redScan n cur acc).size = acc.size + n

theorem CompPoly.Extension.Ext.redScan_getElem {F : Type u_1} [Ring F] {P : ExtensionParams F} (n : ℕ) (cur : Ext P) (acc : Array (Ext P)) (k : ℕ) (h : k < (redScan n cur acc).size) : (redScan n cur acc)[k] = if hlt : k < acc.size then acc[k] else shiftReduce^[k - acc.size] cur

Entry k of the scan is shiftReduce^[k - acc.size] cur past the prefix it was given.

def CompPoly.Extension.Ext.red {F : Type u_1} [Ring F] (P : ExtensionParams F) : Vector (Ext P) (2 * P.d - 1)

The reduction table: red P holds X^k mod f for every k ≤ 2d - 2, i.e. every exponent a product of two reduced elements can reach.

Built by one redScan from 1, so the whole table costs O(d^2); Vector.ofFn (monomialMod ·) would iterate shiftReduce from scratch for every entry, O(d^3) in all. It exists purely for speed: mul is the specification, and mulTbl below is the compiled implementation that consults this table.

@[simp]

theorem CompPoly.Extension.Ext.red_getElem {F : Type u_1} [Ring F] {P : ExtensionParams F} {k : ℕ} (hk : k < 2 * P.d - 1) : (red P)[k] = monomialMod k

theorem Fin.foldl_add_eq_add_sum {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin n → M) (a : M) : foldl n (fun (acc : M) (i : Fin n) => acc + f i) a = a + ∑ i : Fin n, f i

A left fold that adds f i at each step is a plus the sum; the bridge from the loops the compiler runs to the Finset.sums the specification is stated with.

@[noinline]

def CompPoly.Extension.Ext.convCoeff {F : Type u_1} {P : ExtensionParams F} [Mul F] [Add F] [Zero F] (x y : Ext P) (k : ℕ) (init : F) : F

Coefficient k of the unreduced product x · y in F[X], the convolution ∑_{i + j = k} xᵢ yⱼ, as one loop over i with j = k - i; a pair outside [0, d) contributes zero. k ranges over [0, 2d - 1), the degrees a product of two reduced elements can reach.

Deliberately a separate function over its own Mul and Add instances, @[noinline] and @[nospecialize], and likewise contractCoeff below. Written inside mulTbl, or inlined or specialised on the Ring F instance, * and + on F are re-derived from the ring dictionary on every step of the innermost loop, through projections that allocate an intermediate structure each time; the emitted C of the first loop run had instDistribOfSemiring in the loop body. Here the two operations arrive as arguments, derived once per call of mulTbl, and the loop only applies them. (nospecialize matters: instance arguments are specialised even without @[specialize] on the callee.)

@[noinline]

def CompPoly.Extension.Ext.contractCoeff {F : Type u_1} {P : ExtensionParams F} [Mul F] [Add F] (tbl : Vector (Ext P) (2 * P.d - 1)) (prod : Vector F (2 * P.d - 1)) (m : Fin P.d) (init : F) : F

Coefficient m of the reduction of the unreduced product prod against the table tbl: ∑_k prodₖ · [X^k mod f]ₘ. See convCoeff for why this is a separate function.

@[specialize #[2]]

def CompPoly.Extension.Ext.mulTbl {F : Type u_1} [Ring F] {P : ExtensionParams F} (x y : Ext P) : Ext P

Table-driven multiplication: the compiled implementation of mul.

Mathematically identical to mul, in two stages: the unreduced product x · y in F[X], 2d - 1 coefficients by convCoeff, then one contraction of those against the reduction table red by contractCoeff. That is d^2 + (2d - 1) d coefficient multiplications where mul performs d^3, and the reduced monomials come from the table instead of being re-derived by monomialMod for every output coefficient. The sums are Fin.foldl loops rather than Finset.sum, which compiles to list-building Multiset machinery.

mul remains the definition everything is proved about; mul_eq_mulTbl below swaps this in for compilation via @[csimp]. The loops live in convCoeff and contractCoeff, for the reason given there.

Specialised on P as well as on the instances: at a call site whose modulus is a constant, which is every concrete extension field, the table red P is then a closed term the compiler evaluates once, rather than being rebuilt on every multiplication.

theorem CompPoly.Extension.Ext.convCoeff_zero {F : Type u_1} [Ring F] {P : ExtensionParams F} (x y : Ext P) (k : ℕ) : x.convCoeff y k 0 = ∑ i : Fin P.d, if ↑i ≤ k ∧ k - ↑i < P.d then x.coeff i * y.coeffNat (k - ↑i) else 0

convCoeff from zero is the convolution sum, with the second index as a coeffNat.

theorem CompPoly.Extension.Ext.sum_fin_add_eq_sum_fin_ite {M : Type u_2} [AddCommMonoid M] {d : ℕ} (i : Fin d) (g : ℕ → M) : ∑ j : Fin d, g (↑i + ↑j) = ∑ k : Fin (2 * d - 1), if ↑i ≤ ↑k ∧ ↑k - ↑i < d then g ↑k else 0

The reindexing behind mul_eq_mulTbl: summing g (i + j) over j < d is summing g k over the k < 2d - 1 that i + j reaches, for a fixed i < d.

@[csimp]

theorem CompPoly.Extension.Ext.mul_eq_mulTbl : @mul = @mulTbl

@[instance_reducible]

instance CompPoly.Extension.Ext.instMul {F : Type u_1} [Ring F] {P : ExtensionParams F} : Mul (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instPowNat {F : Type u_1} [Ring F] {P : ExtensionParams F} : Pow (Ext P) ℕ

Nat-power by binary exponentiation, so x ^ n costs O(log n) multiplications.

@[instance_reducible]

instance CompPoly.Extension.Ext.instNatCast {F : Type u_1} [Ring F] {P : ExtensionParams F} : NatCast (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instIntCast {F : Type u_1} [Ring F] {P : ExtensionParams F} : IntCast (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instDecidableEq {F : Type u_1} {P : ExtensionParams F} [DecidableEq F] : DecidableEq (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instBEq {F : Type u_1} {P : ExtensionParams F} [BEq F] : BEq (Ext P)

instance CompPoly.Extension.Ext.instLawfulBEq {F : Type u_1} {P : ExtensionParams F} [BEq F] [LawfulBEq F] : LawfulBEq (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instRepr {F : Type u_1} {P : ExtensionParams F} [Repr F] : Repr (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instInhabited {F : Type u_1} [Ring F] {P : ExtensionParams F} : Inhabited (Ext P)

Coefficients of the operations

@[simp]

theorem CompPoly.Extension.Ext.coeff_zero {F : Type u_1} [Ring F] {P : ExtensionParams F} (i : Fin P.d) : coeff 0 i = 0

@[simp]

theorem CompPoly.Extension.Ext.coeff_one {F : Type u_1} [Ring F] {P : ExtensionParams F} (i : Fin P.d) : coeff 1 i = if ↑i = 0 then 1 else 0

@[simp]

theorem CompPoly.Extension.Ext.coeff_add {F : Type u_1} [Ring F] {P : ExtensionParams F} (x y : Ext P) (i : Fin P.d) : (x + y).coeff i = x.coeff i + y.coeff i

@[simp]

theorem CompPoly.Extension.Ext.coeff_neg {F : Type u_1} [Ring F] {P : ExtensionParams F} (x : Ext P) (i : Fin P.d) : (-x).coeff i = -x.coeff i

@[simp]

theorem CompPoly.Extension.Ext.coeff_sub {F : Type u_1} [Ring F] {P : ExtensionParams F} (x y : Ext P) (i : Fin P.d) : (x - y).coeff i = x.coeff i - y.coeff i

@[simp]

theorem CompPoly.Extension.Ext.coeff_smul {F : Type u_1} [Ring F] {P : ExtensionParams F} (c : F) (x : Ext P) (i : Fin P.d) : (c • x).coeff i = c * x.coeff i

@[simp]

theorem CompPoly.Extension.Ext.coeff_shiftReduce {F : Type u_1} [Ring F] {P : ExtensionParams F} (e : Ext P) (m : Fin P.d) : e.shiftReduce.coeff m = (if ↑m = 0 then 0 else e.coeffNat (↑m - 1)) - e.coeffNat (P.d - 1) * P.lowerCoeff m

@[simp]

theorem CompPoly.Extension.Ext.coeff_mul {F : Type u_1} [Ring F] {P : ExtensionParams F} (x y : Ext P) (m : Fin P.d) : (x * y).coeff m = ∑ i : Fin P.d, ∑ j : Fin P.d, x.coeff i * y.coeff j * (monomialMod (↑i + ↑j)).coeff m

@[simp]

theorem CompPoly.Extension.Ext.coeff_ofBase {F : Type u_1} [Ring F] {P : ExtensionParams F} (c : F) (i : Fin P.d) : (ofBase c).coeff i = if ↑i = 0 then c else 0

@[simp]

theorem CompPoly.Extension.Ext.coeff_gen {F : Type u_1} [Ring F] {P : ExtensionParams F} (i : Fin P.d) : gen.coeff i = if ↑i = 1 then 1 else 0

@[simp]

theorem CompPoly.Extension.Ext.ofBase_one {F : Type u_1} [Ring F] {P : ExtensionParams F} : ofBase 1 = 1

ofBase agrees with 1 on the multiplicative unit.

@[simp]

theorem CompPoly.Extension.Ext.ofBase_zero {F : Type u_1} [Ring F] {P : ExtensionParams F} : ofBase 0 = 0

ofBase agrees with 0.

@[simp]

theorem CompPoly.Extension.Ext.ofBase_natCast {F : Type u_1} [Ring F] {P : ExtensionParams F} (n : ℕ) : ofBase ↑n = ↑n

ofBase agrees with the ℕ-cast, so scalars and numerals do not diverge.

@[simp]

theorem CompPoly.Extension.Ext.ofBase_intCast {F : Type u_1} [Ring F] {P : ExtensionParams F} (n : ℤ) : ofBase ↑n = ↑n

ofBase agrees with the ℤ-cast.

@[simp]

theorem CompPoly.Extension.Ext.coeff_natCast {F : Type u_1} [Ring F] {P : ExtensionParams F} (n : ℕ) (i : Fin P.d) : (↑n).coeff i = if ↑i = 0 then ↑n else 0

@[simp]

theorem CompPoly.Extension.Ext.coeff_intCast {F : Type u_1} [Ring F] {P : ExtensionParams F} (n : ℤ) (i : Fin P.d) : (↑n).coeff i = if ↑i = 0 then ↑n else 0

theorem CompPoly.Extension.Ext.pow_def {F : Type u_1} [Ring F] {P : ExtensionParams F} (x : Ext P) (n : ℕ) : x ^ n = npowBinRec n x

def CompPoly.Extension.Ext.inv {F : Type u_1} [Ring F] {P : ExtensionParams F} (x : Ext P) : Ext P

The canonical inverse candidate x ^ (q^d - 2).

Inverse laws require finite-cardinality and irreducibility certificates. For arbitrary q, this operation need not send zero to zero.

@[instance_reducible]

instance CompPoly.Extension.Ext.instInv {F : Type u_1} [Ring F] {P : ExtensionParams F} : Inv (Ext P)

@[instance_reducible]

instance CompPoly.Extension.Ext.instDiv {F : Type u_1} [Ring F] {P : ExtensionParams F} : Div (Ext P)

theorem CompPoly.Extension.Ext.inv_def {F : Type u_1} [Ring F] {P : ExtensionParams F} (x : Ext P) : x⁻¹ = x ^ (P.q ^ P.d - 2)

theorem CompPoly.Extension.Ext.div_def {F : Type u_1} [Ring F] {P : ExtensionParams F} (x y : Ext P) : x / y = x * y⁻¹

Binomial extensions as a special case

A binomial extension F[X] / (X^d - W) is the case lower = (-W, 0, …, 0). BinomialParams keeps the W-only interface; toExtensionParams maps it into the general framework. The polynomial correspondence and binomial irreducibility criterion are proved separately.

structure CompPoly.Extension.BinomialParams (F : Type u_2) : Type u_2

Parameters for the quotient F[X] / (X^d - W): the degree, constant W, and a proposed base cardinality. The modulus has lower coefficients (-W, 0, …, 0).

• d : ℕ

  The degree of the extension.

• W : F

  The extension adjoins a d-th root of W.

• two_le : 2 ≤ self.d

  Degree at least two; a degree-one "extension" is just F.

• q : ℕ

  The proposed base cardinality used by the inverse exponent.

theorem CompPoly.Extension.BinomialParams.d_pos {F : Type u_1} (P : BinomialParams F) : 0 < P.d

def CompPoly.Extension.BinomialParams.toExtensionParams {F : Type u_1} [Ring F] (P : BinomialParams F) : ExtensionParams F

The general-framework parameters for the binomial modulus X^d - W: the lower coefficient vector is (-W, 0, …, 0).

@[simp]

theorem CompPoly.Extension.BinomialParams.toExtensionParams_d {F : Type u_1} [Ring F] (P : BinomialParams F) : P.toExtensionParams.d = P.d

@[simp]

theorem CompPoly.Extension.BinomialParams.toExtensionParams_q {F : Type u_1} [Ring F] (P : BinomialParams F) : P.toExtensionParams.q = P.q

@[simp]

theorem CompPoly.Extension.BinomialParams.toExtensionParams_lowerCoeff {F : Type u_1} [Ring F] (P : BinomialParams F) (i : Fin P.toExtensionParams.d) : P.toExtensionParams.lowerCoeff i = if ↑i = 0 then -P.W else 0