Bounded component separation in binary polynomial quotients

Refine the unit by a supplied family of Frobenius-fixed vectors. The component count is clipped to the quotient dimension on every iteration; the algebraic orthogonality invariant proves that clipping is inert on valid inputs.

theorem MIPRE.LowDegree.BinaryQuotient.toBits_injective (f : Polynomial (ZMod 2)) (hf : f.Monic) : Function.Injective (toBits f hf)

Canonical encoding is injective for every monic quotient.

theorem MIPRE.LowDegree.BinaryQuotient.zeroRow_toBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (x : AdjoinRoot f) : BinaryLinear.zeroRow (toBits f hf x) = toBits f hf 0

The zero row agrees with the canonical zero encoding.

theorem MIPRE.LowDegree.BinaryQuotient.nonzeroRow_toBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (x : AdjoinRoot f) : BinaryLinear.nonzeroRow (toBits f hf x) = decide (x ≠ 0)

The raw zero test faithfully recognizes quotient zero on canonical encodings.

theorem MIPRE.LowDegree.BinaryQuotient.xorBits_toBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (x y : AdjoinRoot f) : BinaryPolynomial.xorBits (toBits f hf x) (toBits f hf y) = toBits f hf (x + y)

Raw XOR agrees exactly with canonical encoding of quotient addition.

theorem MIPRE.LowDegree.BinaryQuotient.mulReduce_toBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (x y : AdjoinRoot f) : BinaryPolynomial.mulReduce p (toBits f hf x) (toBits f hf y) = toBits f hf (x * y)

Raw modular multiplication agrees with canonical quotient multiplication.

def MIPRE.LowDegree.BinaryQuotient.splitBits (p e b : Cost.BitStr) : List Cost.BitStr

One quotient split uses modular multiplication, XOR, and a zero test.

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.splitBits_width (p e b x : Cost.BitStr) : x ∈ splitBits p e b → List.length x ≤ List.length e

Splitting never increases any component's coefficient width.

theorem MIPRE.LowDegree.BinaryQuotient.splitBits_encoding (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (e b : AdjoinRoot f) : splitBits p (toBits f hf e) (toBits f hf b) = List.map (toBits f hf) (splitComponent e b)

The encoded split is exactly the abstract idempotent split.

def MIPRE.LowDegree.BinaryQuotient.splitBitsCapped (p : Cost.BitStr) (l : List Cost.BitStr) (b : Cost.BitStr) : List Cost.BitStr

Refine the component list and retain at most the quotient dimension.

Equations

• MIPRE.LowDegree.BinaryQuotient.splitBitsCapped p l b = List.take (List.length p) (List.flatMap (fun (e : MIPRE.Cost.BitStr) => MIPRE.LowDegree.BinaryQuotient.splitBits p e b) l)

theorem MIPRE.LowDegree.BinaryQuotient.finrank_eq (f : Polynomial (ZMod 2)) (hf : f.Monic) : Module.finrank (ZMod 2) (AdjoinRoot f) = f.natDegree

The quotient dimension is the degree of the monic modulus.

theorem MIPRE.LowDegree.BinaryQuotient.splitBitsCapped_encoding (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (l : List (AdjoinRoot f)) (hl : ComponentFamily l) (b : AdjoinRoot f) (hb : b * b = b) : splitBitsCapped p (List.map (toBits f hf) l) (toBits f hf b) = List.map (toBits f hf) (splitComponents l b)

The list cap is inert on a genuine family of orthogonal quotient idempotents.

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryQuotient.ComponentState : Type

Quotient modulus together with its current component list.

Equations

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

def MIPRE.LowDegree.BinaryQuotient.componentStep (s : ComponentState) (b : Cost.BitStr) : ComponentState

Refine once by the next supplied fixed-space generator.

Equations

• MIPRE.LowDegree.BinaryQuotient.componentStep s b = (s.1, MIPRE.LowDegree.BinaryQuotient.splitBitsCapped s.1 s.2 b)

theorem MIPRE.LowDegree.BinaryQuotient.fold_componentStep_modulus (bs : List Cost.BitStr) (p : Cost.BitStr) (l : List Cost.BitStr) : (List.foldl componentStep (p, l) bs).1 = p

Refinement retains the modulus.

theorem MIPRE.LowDegree.BinaryQuotient.splitBitsCapped_width (p : Cost.BitStr) (l : List Cost.BitStr) (b : Cost.BitStr) (N : ℕ) (hl : ∀ e ∈ l, List.length e ≤ N) (e : Cost.BitStr) : e ∈ splitBitsCapped p l b → List.length e ≤ N

Refined lists retain the original coefficient-width bound.

theorem MIPRE.LowDegree.BinaryQuotient.fold_componentStep_width (bs : List Cost.BitStr) (p : Cost.BitStr) (l : List Cost.BitStr) (N : ℕ) (hl : ∀ e ∈ l, List.length e ≤ N) (e : Cost.BitStr) : e ∈ (List.foldl componentStep (p, l) bs).2 → List.length e ≤ N

Every partial refinement has the original maximum component width.

theorem MIPRE.LowDegree.BinaryQuotient.fold_componentStep_length (bs : List Cost.BitStr) (p : Cost.BitStr) (l : List Cost.BitStr) (N : ℕ) (hp : List.length p ≤ N) (hl : l.length ≤ N) : (List.foldl componentStep (p, l) bs).2.length ≤ N

The cap bounds the number of components even for malformed inputs.

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

A single raw component split as a polynomial-time ambient program.

Equations

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

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

Refine a raw list with one generator and apply the dimension cap.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.splitBitsCappedProg_apply (p : Cost.BitStr) (l : List Cost.BitStr) (b : Cost.BitStr) : splitBitsCappedProg.toFun (p, l, b) = splitBitsCapped p l b

noncomputable def MIPRE.LowDegree.BinaryQuotient.componentStepProg : Cost.PolyTimeFun (ComponentState × Cost.BitStr) ComponentState

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.componentStep_bounded : componentStepProg.FoldBounded (5 * Polynomial.X ^ 2 + 5 * Polynomial.X + 5)

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

Refine the unit by the supplied fixed-space generator list.

Equations

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

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

Uniform polynomial-time quotient component separation.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.componentsBitsProg_apply (p : Cost.BitStr) (bs : List Cost.BitStr) : componentsBitsProg.toFun (p, bs) = componentsBits p bs

theorem MIPRE.LowDegree.BinaryQuotient.fold_componentStep_encoding (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (bs l : List (AdjoinRoot f)) (hl : ComponentFamily l) (hb : ∀ b ∈ bs, b * b = b) : List.foldl componentStep (p, List.map (toBits f hf) l) (List.map (toBits f hf) bs) = (p, List.map (toBits f hf) (splitAllComponents l bs))

The complete encoded refinement agrees with abstract component refinement.

noncomputable def MIPRE.LowDegree.BinaryQuotient.fixedFamily (f : Polynomial (ZMod 2)) (hf : f.Monic) : List (AdjoinRoot f)

The Frobenius-fixed family in the program's specified deterministic order.

Equations

• MIPRE.LowDegree.BinaryQuotient.fixedFamily f hf = List.ofFn (MIPRE.LowDegree.BinaryQuotient.fixedGenerator f hf)

noncomputable def MIPRE.LowDegree.BinaryQuotient.components (f : Polynomial (ZMod 2)) (hf : f.Monic) : List (AdjoinRoot f)

The abstract component family produced by separating all fixed-space generators.

Equations

• MIPRE.LowDegree.BinaryQuotient.components f hf = MIPRE.LowDegree.splitAllComponents [1] (MIPRE.LowDegree.BinaryQuotient.fixedFamily f hf)

theorem MIPRE.LowDegree.BinaryQuotient.fixedFamily_idempotent (f : Polynomial (ZMod 2)) (hf : f.Monic) (b : AdjoinRoot f) : b ∈ fixedFamily f hf → b * b = b

Every generator in the computed fixed-space family is idempotent.

theorem MIPRE.LowDegree.BinaryQuotient.fixedFamily_spans (f : Polynomial (ZMod 2)) (hf : f.Monic) (z : AdjoinRoot f) (hz : z * z = z) : z ∈ Submodule.span (ZMod 2) {b : AdjoinRoot f | b ∈ fixedFamily f hf}

All quotient idempotents lie in the span of the computed family.

theorem MIPRE.LowDegree.BinaryQuotient.components_family (f : Polynomial (ZMod 2)) (hf : f.Monic) [Nontrivial (AdjoinRoot f)] : ComponentFamily (components f hf)

The computed abstract components are complete nonzero orthogonal idempotents.

theorem MIPRE.LowDegree.BinaryQuotient.components_primitive (f : Polynomial (ZMod 2)) (hf : f.Monic) [Nontrivial (AdjoinRoot f)] (e : AdjoinRoot f) : e ∈ components f hf → PrimitiveBinaryComponent e

Separation of the complete fixed space makes every returned component primitive.

theorem MIPRE.LowDegree.BinaryQuotient.oneBits_toBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hp0 : p ≠ []) : BinaryPolynomial.oneBits p = toBits f hf 1

Fixed-width one is the canonical encoding of the quotient unit.

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

Compute the primitive component encodings from the monic modulus alone.

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.quotientComponentsProg_correct (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (hp0 : p ≠ []) : quotientComponentsProg.toFun p = List.map (toBits f hf) (components f hf)

The uniform program computes precisely the abstract primitive components.