Polynomial products with coefficients in an explicit binary quotient

def MIPRE.LowDegree.BinaryQuotient.coeffPolynomial {R : Type u_1} [CommRing R] (z : R) : List Cost.BitStr → Polynomial R

Interpret a list of binary coefficient vectors as a polynomial.

Equations

• MIPRE.LowDegree.BinaryQuotient.coeffPolynomial z [] = 0
• MIPRE.LowDegree.BinaryQuotient.coeffPolynomial z (c :: cs) = Polynomial.C (MIPRE.LowDegree.BinaryPolynomial.evalBits z c) + Polynomial.X * MIPRE.LowDegree.BinaryQuotient.coeffPolynomial z cs

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_nil {R : Type u_1} [CommRing R] (z : R) : coeffPolynomial z [] = 0

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_cons {R : Type u_1} [CommRing R] (z : R) (c : Cost.BitStr) (cs : List Cost.BitStr) : coeffPolynomial z (c :: cs) = Polynomial.C (BinaryPolynomial.evalBits z c) + Polynomial.X * coeffPolynomial z cs

def MIPRE.LowDegree.BinaryQuotient.linearMulCarry (p a carry : Cost.BitStr) (cs : List Cost.BitStr) : List Cost.BitStr

Multiply by a linear factor, with an extra constant coefficient carried in.

Equations

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

def MIPRE.LowDegree.BinaryQuotient.linearMulBits (p a : Cost.BitStr) (cs : List Cost.BitStr) : List Cost.BitStr

Multiplication by X + a on encoded coefficient lists.

Equations

• MIPRE.LowDegree.BinaryQuotient.linearMulBits p a cs = MIPRE.LowDegree.BinaryQuotient.linearMulCarry p a (MIPRE.LowDegree.BinaryPolynomial.zeroBits p) cs

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.length_linearMulCarry (p a carry : Cost.BitStr) (cs : List Cost.BitStr) : (linearMulCarry p a carry cs).length = cs.length + 1

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.length_linearMulBits (p a : Cost.BitStr) (cs : List Cost.BitStr) : (linearMulBits p a cs).length = cs.length + 1

theorem MIPRE.LowDegree.BinaryQuotient.linearMulCarry_width (p a carry : Cost.BitStr) (cs : List Cost.BitStr) (ha : List.length a = List.length p) (hc : List.length carry = List.length p) (hs : ∀ c ∈ cs, List.length c = List.length p) (c : Cost.BitStr) : c ∈ linearMulCarry p a carry cs → List.length c = List.length p

The carried linear multiplication preserves correct coefficient widths.

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_linearMulCarry {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a carry : Cost.BitStr) (cs : List Cost.BitStr) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : List.length a = List.length p) (hc : List.length carry = List.length p) (hs : ∀ c ∈ cs, List.length c = List.length p) : coeffPolynomial z (linearMulCarry p a carry cs) = Polynomial.C (BinaryPolynomial.evalBits z carry) + (Polynomial.X + Polynomial.C (BinaryPolynomial.evalBits z a)) * coeffPolynomial z cs

Linear multiplication has exactly the expected polynomial semantics.

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_linearMulBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a : Cost.BitStr) (cs : List Cost.BitStr) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : List.length a = List.length p) (hs : ∀ c ∈ cs, List.length c = List.length p) : coeffPolynomial z (linearMulBits p a cs) = (Polynomial.X + Polynomial.C (BinaryPolynomial.evalBits z a)) * coeffPolynomial z cs

Multiplication by a linear factor is correct in any represented binary algebra.

noncomputable def MIPRE.LowDegree.BinaryQuotient.scaleCoeffProg : Cost.PolyTimeFun (List Cost.BitStr × Cost.BitStr × Cost.BitStr) (List Cost.BitStr)

Scalar multiplication of all coefficient vectors by a supplied quotient element.

Equations

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

noncomputable def MIPRE.LowDegree.BinaryQuotient.linearMulCarryProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

A uniform linear-factor multiplication program on arbitrary nested lists.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.linearMulCarryProg_apply (p a carry : Cost.BitStr) (cs : List Cost.BitStr) : linearMulCarryProg.toFun (p, a, carry, cs) = linearMulCarry p a carry cs

noncomputable def MIPRE.LowDegree.BinaryQuotient.linearMulBitsProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

Polynomial-time multiplication by one encoded monic linear factor.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.linearMulBitsProg_apply (p a : Cost.BitStr) (cs : List Cost.BitStr) : linearMulBitsProg.toFun (p, a, cs) = linearMulBits p a cs

theorem MIPRE.LowDegree.BinaryQuotient.linearMulCarry_width_le (p a carry : Cost.BitStr) (cs : List Cost.BitStr) (N : ℕ) (hc : List.length carry ≤ N) (hs : ∀ c ∈ cs, List.length c ≤ N) (c : Cost.BitStr) : c ∈ linearMulCarry p a carry cs → List.length c ≤ N

Malformed coefficient arithmetic cannot increase a retained coefficient width.

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryQuotient.ProductState : Type

Modulus and accumulated coefficient list for a product of linear factors.

Equations

• MIPRE.LowDegree.BinaryQuotient.ProductState = (MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryQuotient.productStep (s : ProductState) (a : Cost.BitStr) : ProductState

Multiply the accumulated polynomial by the next supplied linear factor.

Equations

• MIPRE.LowDegree.BinaryQuotient.productStep s a = (s.1, MIPRE.LowDegree.BinaryQuotient.linearMulBits s.1 a s.2)

theorem MIPRE.LowDegree.BinaryQuotient.fold_productStep_shape (bs : List Cost.BitStr) (s : ProductState) : (List.foldl productStep s bs).1 = s.1 ∧ (List.foldl productStep s bs).2.length = s.2.length + bs.length

The product loop retains its modulus and adds one coefficient per iteration.

theorem MIPRE.LowDegree.BinaryQuotient.fold_productStep_width (bs : List Cost.BitStr) (p : Cost.BitStr) (cs : List Cost.BitStr) (N : ℕ) (hp : List.length p ≤ N) (hs : ∀ c ∈ cs, List.length c ≤ N) (c : Cost.BitStr) : c ∈ (List.foldl productStep (p, cs) bs).2 → List.length c ≤ N

Every coefficient width remains bounded independently of the number of factors.

theorem MIPRE.LowDegree.BinaryQuotient.fold_productStep_width_eq (bs : List Cost.BitStr) (p : Cost.BitStr) (cs : List Cost.BitStr) (hb : ∀ a ∈ bs, List.length a = List.length p) (hs : ∀ c ∈ cs, List.length c = List.length p) (c : Cost.BitStr) : c ∈ (List.foldl productStep (p, cs) bs).2 → List.length c = List.length p

Valid fixed-width coefficients remain valid through the product loop.

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_fold_productStep {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (bs cs : List Cost.BitStr) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (hb : ∀ a ∈ bs, List.length a = List.length p) (hs : ∀ c ∈ cs, List.length c = List.length p) : coeffPolynomial z (List.foldl productStep (p, cs) bs).2 = (List.map (fun (a : Cost.BitStr) => Polynomial.X + Polynomial.C (BinaryPolynomial.evalBits z a)) bs).prod * coeffPolynomial z cs

The accumulated coefficient polynomial is the product of all supplied factors.

def MIPRE.LowDegree.BinaryQuotient.linearProductBits (p : Cost.BitStr) (bs : List Cost.BitStr) : List Cost.BitStr

Product of the monic linear factors with the supplied roots.

Equations

• MIPRE.LowDegree.BinaryQuotient.linearProductBits p bs = (List.foldl MIPRE.LowDegree.BinaryQuotient.productStep (p, [MIPRE.LowDegree.BinaryPolynomial.oneBits p]) bs).2

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_linearProductBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (bs : List Cost.BitStr) (hp : p ≠ []) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (hb : ∀ a ∈ bs, List.length a = List.length p) : coeffPolynomial z (linearProductBits p bs) = (List.map (fun (a : Cost.BitStr) => Polynomial.X + Polynomial.C (BinaryPolynomial.evalBits z a)) bs).prod

The encoded product has the expected polynomial semantics.

noncomputable def MIPRE.LowDegree.BinaryQuotient.productStepProg : Cost.PolyTimeFun (ProductState × Cost.BitStr) ProductState

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.esize_coefficients_le (cs : List Cost.BitStr) (N : ℕ) (hs : ∀ c ∈ cs, List.length c ≤ N) : Cost.esize cs ≤ cs.length * (4 * N + 2) + 1

Nested coefficient-list encoded size is polynomial in count and width.

theorem MIPRE.LowDegree.BinaryQuotient.productStep_bounded : productStepProg.FoldBounded (10 * Polynomial.X ^ 2 + 10 * Polynomial.X + 10)

noncomputable def MIPRE.LowDegree.BinaryQuotient.linearProductBitsProg : Cost.PolyTimeFun (Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

One globally polynomial-time program for a product of encoded linear factors.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.linearProductBitsProg_apply (p : Cost.BitStr) (bs : List Cost.BitStr) : linearProductBitsProg.toFun (p, bs) = linearProductBits p bs

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryQuotient.SquareState : Type

State for successive Frobenius powers, retaining the modulus.

Equations

• MIPRE.LowDegree.BinaryQuotient.SquareState = (MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryQuotient.squareStep (s : SquareState) : SquareState

One repeated-squaring step in a supplied binary quotient.

Equations

• MIPRE.LowDegree.BinaryQuotient.squareStep s = (s.1, MIPRE.LowDegree.BinaryPolynomial.mulReduce s.1 s.2 s.2)

theorem MIPRE.LowDegree.BinaryQuotient.iterate_squareStep_shape (n : ℕ) (s : SquareState) : (squareStep^[n] s).1 = s.1 ∧ List.length (squareStep^[n] s).2 ≤ List.length s.2

Squaring cannot increase the width even on malformed inputs.

theorem MIPRE.LowDegree.BinaryQuotient.iterate_squareStep_width (n : ℕ) (p a : Cost.BitStr) (ha : List.length a = List.length p) : List.length (squareStep^[n] (p, a)).2 = List.length p

Repeated squaring preserves the fixed-width representation.

theorem MIPRE.LowDegree.BinaryQuotient.evalBits_iterate_squareStep {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (n : ℕ) (p a : Cost.BitStr) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : List.length a = List.length p) : BinaryPolynomial.evalBits z (squareStep^[n] (p, a)).2 = BinaryPolynomial.evalBits z a ^ 2 ^ n

Repeated squaring computes the corresponding Frobenius power.

noncomputable def MIPRE.LowDegree.BinaryQuotient.squareStepProg : Cost.PolyTimeFun SquareState SquareState

Equations

• MIPRE.LowDegree.BinaryQuotient.squareStepProg = MIPRE.Cost.PolyTimeFun.fst.pair MIPRE.LowDegree.BinaryQuotient.squareProg

theorem MIPRE.LowDegree.BinaryQuotient.squareStep_bounded (n : ℕ) (s : SquareState) : Cost.esize (squareStepProg.toFun^[n] s) ≤ Polynomial.eval (Cost.esize s) (5 * Polynomial.X + 5)

def MIPRE.LowDegree.BinaryQuotient.orbitBits (u : Cost.Unary) (p a : Cost.BitStr) : List Cost.BitStr

The first Frobenius powers of a supplied represented element.

Equations

• MIPRE.LowDegree.BinaryQuotient.orbitBits u p a = List.map Prod.snd (MIPRE.Cost.recordIterates MIPRE.LowDegree.BinaryQuotient.squareStep u (p, a))

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.length_orbitBits (u : Cost.Unary) (p a : Cost.BitStr) : (orbitBits u p a).length = List.length u

The orbit list has exactly its unary budget of elements.

theorem MIPRE.LowDegree.BinaryQuotient.orbitBits_width (u : Cost.Unary) (p a : Cost.BitStr) (ha : List.length a = List.length p) (b : Cost.BitStr) : b ∈ orbitBits u p a → List.length b = List.length p

Every orbit element has the supplied modulus width.

theorem MIPRE.LowDegree.BinaryQuotient.map_evalBits_orbitBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (u : Cost.Unary) (p a : Cost.BitStr) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : List.length a = List.length p) : List.map (BinaryPolynomial.evalBits z) (orbitBits u p a) = List.ofFn fun (i : Fin (List.length u)) => BinaryPolynomial.evalBits z a ^ 2 ^ ↑i

The orbit encodes exactly the specified list of Frobenius powers.

noncomputable def MIPRE.LowDegree.BinaryQuotient.orbitBitsProg : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr × Cost.BitStr) (List Cost.BitStr)

A polynomial-time orbit printer, valid on every raw input.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.orbitBitsProg_apply (u : Cost.Unary) (p a : Cost.BitStr) : orbitBitsProg.toFun (u, p, a) = orbitBits u p a

def MIPRE.LowDegree.BinaryQuotient.orbitProductBits (u : Cost.Unary) (p a : Cost.BitStr) : List Cost.BitStr

Multiply the monic linear factors for a specified Frobenius orbit.

Equations

• MIPRE.LowDegree.BinaryQuotient.orbitProductBits u p a = MIPRE.LowDegree.BinaryQuotient.linearProductBits p (MIPRE.LowDegree.BinaryQuotient.orbitBits u p a)

noncomputable def MIPRE.LowDegree.BinaryQuotient.orbitProductBitsProg : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr × Cost.BitStr) (List Cost.BitStr)

A uniform polynomial-time Frobenius-orbit product program.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.orbitProductBitsProg_apply (u : Cost.Unary) (p a : Cost.BitStr) : orbitProductBitsProg.toFun (u, p, a) = orbitProductBits u p a

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_orbitProductBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (u : Cost.Unary) (p a : Cost.BitStr) (hp : p ≠ []) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : List.length a = List.length p) : coeffPolynomial z (orbitProductBits u p a) = (List.ofFn fun (i : Fin (List.length u)) => Polynomial.X + Polynomial.C (BinaryPolynomial.evalBits z a ^ 2 ^ ↑i)).prod

The printed product equals the product of the Frobenius conjugate linear factors.

theorem MIPRE.LowDegree.BinaryQuotient.orbitProductBits_width (u : Cost.Unary) (p a : Cost.BitStr) (ha : List.length a = List.length p) (c : Cost.BitStr) : c ∈ orbitProductBits u p a → List.length c = List.length p

Every printed coefficient has the prescribed quotient width.

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.length_orbitProductBits (u : Cost.Unary) (p a : Cost.BitStr) : (orbitProductBits u p a).length = List.length u + 1

The orbit product has exactly one more coefficient than its orbit length.