Executable binary vector and matrix arithmetic

def MIPRE.LowDegree.BinaryLinear.bit (x : ZMod 2) : Bool

Canonical binary scalar coordinates.

Equations

• MIPRE.LowDegree.BinaryLinear.bit x = decide (x = 1)

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.ofBool_bit (x : ZMod 2) : ofBool (bit x) = x

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.bit_ofBool (x : Bool) : bit (ofBool x) = x

theorem MIPRE.LowDegree.BinaryLinear.ofBool_injective : Function.Injective ofBool

theorem MIPRE.LowDegree.BinaryLinear.ofBool_xor (a b : Bool) : ofBool (a ^^ b) = ofBool a + ofBool b

theorem MIPRE.LowDegree.BinaryLinear.ofBool_and (a b : Bool) : ofBool (a && b) = ofBool a * ofBool b

def MIPRE.LowDegree.BinaryLinear.vectorBits {n : ℕ} (v : Fin n → ZMod 2) : Cost.BitStr

Equations

• MIPRE.LowDegree.BinaryLinear.vectorBits v = List.ofFn fun (i : Fin n) => MIPRE.LowDegree.BinaryLinear.bit (v i)

def MIPRE.LowDegree.BinaryLinear.matrixBits {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) : List Cost.BitStr

Equations

• MIPRE.LowDegree.BinaryLinear.matrixBits A = List.ofFn fun (i : Fin m) => MIPRE.LowDegree.BinaryLinear.vectorBits (A i)

def MIPRE.LowDegree.BinaryLinear.dotStep (b : Bool) (p : Bool × Bool) : Bool

Equations

• MIPRE.LowDegree.BinaryLinear.dotStep b p = (b ^^ p.1 && p.2)

def MIPRE.LowDegree.BinaryLinear.dotBits (a b : Cost.BitStr) : Bool

Equations

• MIPRE.LowDegree.BinaryLinear.dotBits a b = List.foldl MIPRE.LowDegree.BinaryLinear.dotStep false (List.zip a b)

theorem MIPRE.LowDegree.BinaryLinear.ofBool_fold_dotStep (l : List (Bool × Bool)) (b : Bool) : ofBool (List.foldl dotStep b l) = ofBool b + (List.map (fun (p : Bool × Bool) => ofBool p.1 * ofBool p.2) l).sum

theorem MIPRE.LowDegree.BinaryLinear.ofBool_dotBits (a b : Cost.BitStr) : ofBool (dotBits a b) = (List.map (fun (p : Bool × Bool) => ofBool p.1 * ofBool p.2) (List.zip a b)).sum

theorem MIPRE.LowDegree.BinaryLinear.zip_vectorBits {n : ℕ} (v w : Fin n → ZMod 2) : List.zip (vectorBits v) (vectorBits w) = List.ofFn fun (i : Fin n) => (bit (v i), bit (w i))

theorem MIPRE.LowDegree.BinaryLinear.dotBits_vectorBits {n : ℕ} (v w : Fin n → ZMod 2) : dotBits (vectorBits v) (vectorBits w) = bit (∑ i : Fin n, v i * w i)

The raw parity circuit computes the exact binary dot product.

def MIPRE.LowDegree.BinaryLinear.applyBits (A : List Cost.BitStr) (v : Cost.BitStr) : Cost.BitStr

A matrix is represented by its rows.

Equations

• MIPRE.LowDegree.BinaryLinear.applyBits A v = List.map (fun (r : MIPRE.Cost.BitStr) => MIPRE.LowDegree.BinaryLinear.dotBits r v) A

theorem MIPRE.LowDegree.BinaryLinear.applyBits_matrixBits {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) (v : Fin n → ZMod 2) : applyBits (matrixBits A) (vectorBits v) = vectorBits (A.mulVec v)

Executable matrix application agrees with the usual binary matrix-vector product.

noncomputable def MIPRE.LowDegree.BinaryLinear.dotStepProg : Cost.PolyTimeFun (Bool × Bool × Bool) Bool

Equations

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

noncomputable def MIPRE.LowDegree.BinaryLinear.dotBitsProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Bool

The parity dot product is one uniform ambient program.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.dotBitsProg_apply (a b : Cost.BitStr) : dotBitsProg.toFun (a, b) = dotBits a b

noncomputable def MIPRE.LowDegree.BinaryLinear.applyBitsProg : Cost.PolyTimeFun (List Cost.BitStr × Cost.BitStr) Cost.BitStr

Binary matrix application is polynomial-time on arbitrary raw row lists.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.applyBitsProg_apply (A : List Cost.BitStr) (v : Cost.BitStr) : applyBitsProg.toFun (A, v) = applyBits A v

theorem MIPRE.LowDegree.BinaryLinear.xorBits_vectorBits {n : ℕ} (v w : Fin n → ZMod 2) : BinaryPolynomial.xorBits (vectorBits v) (vectorBits w) = vectorBits (v + w)

Coordinatewise XOR computes binary vector addition.

def MIPRE.LowDegree.BinaryLinear.transposeBits (n : ℕ) (A : List Cost.BitStr) : List Cost.BitStr

The number of columns is explicit; short raw rows are padded with zero.

Equations

• MIPRE.LowDegree.BinaryLinear.transposeBits n A = List.map (fun (j : ℕ) => List.map (fun (r : MIPRE.Cost.BitStr) => List.getD r j false) A) (List.range n)

theorem MIPRE.LowDegree.BinaryLinear.transposeBits_matrixBits {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) : transposeBits n (matrixBits A) = matrixBits A.transpose

Raw transposition agrees with typed matrix transposition.

def MIPRE.LowDegree.BinaryLinear.mulBits (n : ℕ) (A B : List Cost.BitStr) : List Cost.BitStr

A rectangular matrix product with an explicit output width.

Equations

• MIPRE.LowDegree.BinaryLinear.mulBits n A B = List.map (fun (r : MIPRE.Cost.BitStr) => MIPRE.LowDegree.BinaryLinear.applyBits (MIPRE.LowDegree.BinaryLinear.transposeBits n B) r) A

theorem MIPRE.LowDegree.BinaryLinear.mulBits_matrixBits {m n r : ℕ} (A : Matrix (Fin m) (Fin r) (ZMod 2)) (B : Matrix (Fin r) (Fin n) (ZMod 2)) : mulBits n (matrixBits A) (matrixBits B) = matrixBits (A * B)

The executable matrix product is the ordinary product over the binary field.

noncomputable def MIPRE.LowDegree.BinaryLinear.columnProg : Cost.PolyTimeFun (ℕ × List Cost.BitStr) Cost.BitStr

Equations

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

noncomputable def MIPRE.LowDegree.BinaryLinear.transposeBitsProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr) (List Cost.BitStr)

Transposition is polynomial-time in the rows and the unary column count.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.transposeBitsProg_apply (u : Cost.Unary) (A : List Cost.BitStr) : transposeBitsProg.toFun (u, A) = transposeBits (List.length u) A

noncomputable def MIPRE.LowDegree.BinaryLinear.mulBitsProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

Matrix multiplication is globally polynomial-time in its raw inputs.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.mulBitsProg_apply (u : Cost.Unary) (A B : List Cost.BitStr) : mulBitsProg.toFun (u, A, B) = mulBits (List.length u) A B