Documentation

MIPRE.Foundations.Introspection.AuxiliaryDualProgram

Executable canonical dual of a binary linear map #

The rows of a matrix span the dot-product orthogonal complement of its kernel. Canonical elimination of those rows therefore computes the exact CL.lperp, including for singular matrices and in dimension zero.

source
theorem MIPRE.Introspection.AuxiliaryDual.map_canonLin_of_le_ker {F : Type u_1} [Field F] {n : ℕ} {V : Type u_2} [AddCommGroup V] [Module F V] (S : Submodule F (Fin n → F)) (D : (Fin n → F) →ₗ[F] V) (hS : S ≤ D.ker) (x : Fin n → F) :
D ((CL.canonLin S) x) = D x

A linear map killing a subspace also kills the part removed by canonical reduction. This permits changing quotient representatives without identifying two coordinate enumerations.

source
theorem MIPRE.Introspection.AuxiliaryDual.perp_span_rows {F : Type u_1} [Field F] {m n : ℕ} (A : Matrix (Fin m) (Fin n) F) :
CL.perp (Submodule.span F (Set.range A)) = A.mulVecLin.ker

Orthogonality to all matrix rows is precisely the kernel condition.

source
theorem MIPRE.Introspection.AuxiliaryDual.span_rows_eq_perp_ker {F : Type u_1} [Field F] {m n : ℕ} (A : Matrix (Fin m) (Fin n) F) :
Submodule.span F (Set.range A) = CL.perp A.mulVecLin.ker

The matrix rows generate the kernel's dot-product orthogonal complement.

source
noncomputable def MIPRE.Introspection.AuxiliaryDual.rowSpaceCheck :
Cost.PolyTimeFun (List Cost.BitStr × Cost.BitStr) Bool

Membership in the supplied row span, tested by exact canonical reduction. The zero vector has the input vector's width, so malformed widths do not become an implicit promise about the program's termination.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.Introspection.AuxiliaryDual.rowSpaceCheck_correct {n : ℕ} (vs : List (Fin n → ZMod 2)) (v : Fin n → ZMod 2) :
    rowSpaceCheck.toFun (List.map LowDegree.BinaryLinear.vectorBits vs, LowDegree.BinaryLinear.vectorBits v) = true ↔ v ∈ Submodule.span (ZMod 2) {x : Fin n → ZMod 2 | x ∈ vs}
    source
    theorem MIPRE.Introspection.AuxiliaryDual.rowSpaceCheck_matrix {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) (v : Fin n → ZMod 2) :
    rowSpaceCheck.toFun (LowDegree.BinaryLinear.matrixBits A, LowDegree.BinaryLinear.vectorBits v) = true ↔ v ∈ CL.perp A.mulVecLin.ker

    The executable test is independent of the choice of quotient representatives: it detects the dot-product orthogonal complement of the matrix kernel.