Primitive components computed by fixed-space separation

theorem MIPRE.LowDegree.BinaryLinear.instFactPrimeOfNatNat_mIPRE_2 : Fact (Nat.Prime 2)

noncomputable def MIPRE.LowDegree.BinaryLinear.groupFixedFamily (k : ℕ) [NeZero k] : List (AddMonoidAlgebra (ZMod 2) (Fin k))

The computed generators in their fixed deterministic order.

Equations

• MIPRE.LowDegree.BinaryLinear.groupFixedFamily k = List.ofFn (MIPRE.LowDegree.BinaryLinear.groupFixedGenerator k)

noncomputable def MIPRE.LowDegree.BinaryLinear.groupComponents (k : ℕ) [NeZero k] : List (AddMonoidAlgebra (ZMod 2) (Fin k))

Separate the components directly in the cyclic algebra, starting with the unit.

Equations

• MIPRE.LowDegree.BinaryLinear.groupComponents k = MIPRE.LowDegree.splitAllComponents [1] (MIPRE.LowDegree.BinaryLinear.groupFixedFamily k)

theorem MIPRE.LowDegree.BinaryLinear.groupFixedFamily_idempotent (k : ℕ) [NeZero k] (b : AddMonoidAlgebra (ZMod 2) (Fin k)) : b ∈ groupFixedFamily k → b * b = b

theorem MIPRE.LowDegree.BinaryLinear.groupFixedFamily_spans (k : ℕ) [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) (hz : z * z = z) : z ∈ Submodule.span (ZMod 2) {b : AddMonoidAlgebra (ZMod 2) (Fin k) | b ∈ groupFixedFamily k}

theorem MIPRE.LowDegree.BinaryLinear.unitComponentFamily (k : ℕ) [NeZero k] : ComponentFamily [1]

theorem MIPRE.LowDegree.BinaryLinear.groupComponents_family (k : ℕ) [NeZero k] : ComponentFamily (groupComponents k)

theorem MIPRE.LowDegree.BinaryLinear.groupComponents_primitive (k : ℕ) [NeZero k] (e : AddMonoidAlgebra (ZMod 2) (Fin k)) : e ∈ groupComponents k → PrimitiveBinaryComponent e

theorem MIPRE.LowDegree.BinaryLinear.groupAlgebra_finrank (k : ℕ) : Module.finrank (ZMod 2) (AddMonoidAlgebra (ZMod 2) (Fin k)) = k

theorem MIPRE.LowDegree.BinaryLinear.groupComponents_length_le (k : ℕ) [NeZero k] : (groupComponents k).length ≤ k

The computation has at most k nonzero components, despite repeatedly splitting them.

def MIPRE.LowDegree.BinaryLinear.zeroRow (v : Cost.BitStr) : Cost.BitStr

Canonical zero of the same raw width.

Equations

• MIPRE.LowDegree.BinaryLinear.zeroRow v = List.map (fun (x : Bool) => false) v

theorem MIPRE.LowDegree.BinaryLinear.zeroRow_vectorBits {k : ℕ} (v : Fin k → ZMod 2) : zeroRow (vectorBits v) = vectorBits 0

theorem MIPRE.LowDegree.BinaryLinear.vectorBits_injective {k : ℕ} : Function.Injective vectorBits

def MIPRE.LowDegree.BinaryLinear.nonzeroRow (v : Cost.BitStr) : Bool

Equations

• MIPRE.LowDegree.BinaryLinear.nonzeroRow v = decide (v ≠ MIPRE.LowDegree.BinaryLinear.zeroRow v)

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.nonzeroRow_zero {k : ℕ} : nonzeroRow (vectorBits 0) = false

theorem MIPRE.LowDegree.BinaryLinear.nonzeroRow_groupBits (k : ℕ) (z : AddMonoidAlgebra (ZMod 2) (Fin k)) : nonzeroRow (vectorBits ((groupCoordinates k) z)) = decide (z ≠ 0)

noncomputable def MIPRE.LowDegree.BinaryLinear.splitBits (e b : Cost.BitStr) : List Cost.BitStr

One raw split uses cyclic multiplication and XOR, then omits zero vectors.

Equations

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

theorem MIPRE.LowDegree.BinaryLinear.splitBits_encoding {k : ℕ} [NeZero k] (e b : AddMonoidAlgebra (ZMod 2) (Fin k)) : splitBits (vectorBits ((groupCoordinates k) e)) (vectorBits ((groupCoordinates k) b)) = List.map (fun (z : AddMonoidAlgebra (ZMod 2) (Fin k)) => vectorBits ((groupCoordinates k) z)) (splitComponent e b)

theorem MIPRE.LowDegree.BinaryLinear.groupMulBitsProg_length (e b : Cost.BitStr) : List.length (groupMulBitsProg.toFun (e, b)) = List.length e

Raw convolution always has the width of its first operand, including malformed inputs.

theorem MIPRE.LowDegree.BinaryLinear.splitBits_width (e b x : Cost.BitStr) : x ∈ splitBits e b → List.length x = List.length e

noncomputable def MIPRE.LowDegree.BinaryLinear.splitBitsCapped (u : Cost.Unary) (l : List Cost.BitStr) (b : Cost.BitStr) : List Cost.BitStr

Raw refinement is clipped to the unary dimension; on valid components this clip is inert.

Equations

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

theorem MIPRE.LowDegree.BinaryLinear.splitBitsCapped_encoding {k : ℕ} [NeZero k] (l : List (AddMonoidAlgebra (ZMod 2) (Fin k))) (hl : ComponentFamily l) (b : AddMonoidAlgebra (ZMod 2) (Fin k)) (hb : b * b = b) : splitBitsCapped (Cost.unary k) (List.map (fun (z : AddMonoidAlgebra (ZMod 2) (Fin k)) => vectorBits ((groupCoordinates k) z)) l) (vectorBits ((groupCoordinates k) b)) = List.map (fun (z : AddMonoidAlgebra (ZMod 2) (Fin k)) => vectorBits ((groupCoordinates k) z)) (splitComponents l b)