Dense Homogeneous-Kernel Correctness

Correctness contracts for executable dense homogeneous-kernel witnesses.

theorem CompPoly.DenseMatrix.homogeneousWitness_eq_none_iff {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) : M.homogeneousWitness = none ↔ M.homogeneousKernelBasis.size = 0

theorem CompPoly.DenseMatrix.homogeneousWitness_exists_of_rows_lt_cols {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : DenseMatrix F) (h : M.rows < M.cols) : ∃ (v : Array F), M.homogeneousWitness = some v

A matrix with more columns than rows has an executable homogeneous witness.

theorem CompPoly.DenseMatrix.homogeneousWitness_width {F : Type u_1} [Field F] [BEq F] {M : DenseMatrix F} {v : Array F} (h : M.homogeneousWitness = some v) : M.VectorWidth v

Any homogeneous witness returned by the executable kernel search has matrix-column width.

theorem CompPoly.DenseMatrix.homogeneousWitness_nonzero {F : Type u_1} [Field F] [BEq F] {M : DenseMatrix F} {v : Array F} (h : M.homogeneousWitness = some v) : NonzeroVector v

Any homogeneous witness returned by the executable kernel search is nonzero.

theorem CompPoly.DenseMatrix.homogeneousWitness_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} (hM : M.WellFormed) {v : Array F} (h : M.homogeneousWitness = some v) : M.VectorWidth v ∧ M.IsHomogeneousSolution v ∧ NonzeroVector v

Soundness of the homogeneous witness returned by Gaussian elimination.

theorem CompPoly.DenseMatrix.homogeneousWitness_none_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : DenseMatrix F} (hM : M.WellFormed) (h : M.homogeneousWitness = none) (v : Array F) : M.VectorWidth v → M.IsHomogeneousSolution v → ¬NonzeroVector v

If no homogeneous witness is returned, the homogeneous kernel is trivial.