theorem HexMatrixTheory.inverse?_eq_inv {F : Type u} [Field F] [DecidableEq F] {n : ℕ} (A B : Hex.Matrix F n n) : A.inverse? = some B → matrixEquiv B = (matrixEquiv A)⁻¹

Successful field inversion agrees with Mathlib's nonsingular inverse.

theorem HexMatrixTheory.inverse?_eq_none {F : Type u} [Field F] [DecidableEq F] {n : ℕ} (A : Hex.Matrix F n n) : A.inverse? = none ↔ (matrixEquiv A).det = 0

Computational singularity is exactly determinant zero after transport.

theorem HexMatrixTheory.solve?_spec {F : Type u} [Field F] [DecidableEq F] {n m : ℕ} (A : Hex.Matrix F n m) (b : Vector F n) (s : A.SolveData) : A.solve? b = some s → (matrixEquiv A).mulVec (vectorEquiv s.1) = vectorEquiv b ∧ s.2 = A.nullspaceBasisMatrix ∧ ∀ (x : Fin m → F), (matrixEquiv A).mulVec x = vectorEquiv b ↔ x - vectorEquiv s.1 ∈ (matrixEquiv A).mulVecLin.ker

A successful answer represents the affine translate of the entire kernel.

theorem HexMatrixTheory.solve?_eq_none {F : Type u} [Field F] [DecidableEq F] {n m : ℕ} (A : Hex.Matrix F n m) (b : Vector F n) : A.solve? b = none ↔ ¬∃ (x : Fin m → F), (matrixEquiv A).mulVec x = vectorEquiv b

Failure is equivalent to absence of a Mathlib matrix-vector solution.

theorem HexMatrixTheory.solve?_span {F : Type u} [Field F] [DecidableEq F] {n m : ℕ} (A : Hex.Matrix F n m) (b : Vector F n) (s : A.SolveData) (h : A.solve? b = some s) : Submodule.span F (Set.range fun (k : Fin (m - A.rowReduce_rank)) => vectorEquiv (s.2.col k)) = (matrixEquiv A).mulVecLin.ker

The returned basis spans the kernel used in the affine solution theorem.

theorem HexMatrixTheory.solve?_parameters {F : Type u} [Field F] [DecidableEq F] {n m : ℕ} (A : Hex.Matrix F n m) (b : Vector F n) (s : A.SolveData) (h : A.solve? b = some s) (x : Fin m → F) : (matrixEquiv A).mulVec x = vectorEquiv b ↔ ∃! c : Fin (m - A.rowReduce_rank) → F, x = vectorEquiv s.1 + (matrixEquiv s.2).mulVec c

Every solution has unique coordinates in the returned affine basis.

theorem HexMatrixTheory.solve_error {F : Type u} [Field F] [DecidableEq F] {n m : ℕ} (A : Hex.Matrix F n m) (b y : Vector F n) (h : A.solve b = Except.error y) : Matrix.vecMul (vectorEquiv y) (matrixEquiv A) = 0 ∧ vectorEquiv y ⬝ᵥ vectorEquiv b ≠ 0

The actual returned transform row separates the RHS from the column space.

theorem HexMatrixTheory.solve?_none_witness {F : Type u} [Field F] [DecidableEq F] {n m : ℕ} (A : Hex.Matrix F n m) (b : Vector F n) : A.solve? b = none ↔ ∃ (y : Fin n → F), Matrix.vecMul y (matrixEquiv A) = 0 ∧ y ⬝ᵥ vectorEquiv b ≠ 0

Inconsistency is equivalent to existence of a left-kernel separator.