Documentation

MIPRE.Foundations.LowDegree.BinaryKernel

Effective generators for a binary matrix kernel #

source
theorem MIPRE.LowDegree.BinaryLinear.typedReduceStep_eq_linear {n t : ℕ} (r : Row n t) (p : Pivot n t) :
typedReduceStep r p = r + r.1 p.1 • p.2

In characteristic two, conditional row addition is a linear map.

source
def MIPRE.LowDegree.BinaryLinear.reduceStepLinear {n t : ℕ} (p : Pivot n t) :
Row n t →ₗ[ZMod 2] Row n t
Equations
Instances For
    source
    @[simp]
    theorem MIPRE.LowDegree.BinaryLinear.reduceStepLinear_apply {n t : ℕ} (p : Pivot n t) (r : Row n t) :
    (reduceStepLinear p) r = typedReduceStep r p
    source
    def MIPRE.LowDegree.BinaryLinear.reduceLinear {n t : ℕ} :
    List (Pivot n t) → Row n t →ₗ[ZMod 2] Row n t
    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.LowDegree.BinaryLinear.reduceLinear_apply {n t : ℕ} (b : List (Pivot n t)) (r : Row n t) :
      (reduceLinear b) r = typedReduce b r
      source
      theorem MIPRE.LowDegree.BinaryLinear.typedReduce_zero_value {n t : ℕ} (b : List (Pivot n t)) (x : Fin t → ZMod 2) :
      typedReduce b (0, x) = (0, x)

      A row whose value is zero keeps its entire certificate unchanged.

      source
      def MIPRE.LowDegree.BinaryLinear.kernelMap {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) :
      (Fin n → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2

      Reduce the graph of the original matrix map and retain the certificate. This is a projection onto its kernel.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.LowDegree.BinaryLinear.kernelMap_apply {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) (x : Fin n → ZMod 2) :
        (kernelMap A) x = (typedReduce (typedBasis (columnRows A)) (A.mulVec x, x)).2
        source
        theorem MIPRE.LowDegree.BinaryLinear.kernelMap_mem_ker {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) (x : Fin n → ZMod 2) :
        (kernelMap A) x ∈ A.mulVecLin.ker

        Every output of the computed projection is in the matrix kernel.

        source
        theorem MIPRE.LowDegree.BinaryLinear.kernelMap_fixed {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) (x : Fin n → ZMod 2) (hx : x ∈ A.mulVecLin.ker) :
        (kernelMap A) x = x

        The projection fixes every vector already in the kernel.

        source
        theorem MIPRE.LowDegree.BinaryLinear.kernelMap_range {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) :
        (kernelMap A).range = A.mulVecLin.ker
        source
        theorem MIPRE.LowDegree.BinaryLinear.kernel_generators_span {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) :
        Submodule.span (ZMod 2) (Set.range fun (j : Fin n) => (kernelMap A) (Pi.single j 1)) = A.mulVecLin.ker

        The images of the standard basis generate exactly the matrix kernel.

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

        Compute at most n generators of an m-by-n binary matrix kernel. The explicit unary input is the number of columns.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPRE.LowDegree.BinaryLinear.kernelGeneratorsProg_encoding {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) :
          kernelGeneratorsProg.toFun (Cost.unary n, matrixBits A) = List.ofFn fun (j : Fin n) => vectorBits ((kernelMap A) (Pi.single j 1))

          The raw program prints canonical vectors spanning the full matrix kernel.

          source
          theorem MIPRE.LowDegree.BinaryLinear.kernelGeneratorsProg_correct {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) :
          (kernelGeneratorsProg.toFun (Cost.unary n, matrixBits A)).length = n ∧ (∀ v ∈ kernelGeneratorsProg.toFun (Cost.unary n, matrixBits A), List.length v = n ∧ vectorValue n v ∈ A.mulVecLin.ker) ∧ Submodule.span (ZMod 2) {x : Fin n → ZMod 2 | ∃ v ∈ kernelGeneratorsProg.toFun (Cost.unary n, matrixBits A), vectorValue n v = x} = A.mulVecLin.ker

          The generated family has polynomial length and every vector lies in the kernel.