inductive HexMatrixTheory.InverseResult {F : Type u} [Field F] {n : ℕ} (A : Matrix (Fin n) (Fin n) F) : Type u

A certified inverse or a certified nonzero right-kernel vector.

• invertible {F : Type u} [Field F] {n : ℕ} {A : Matrix (Fin n) (Fin n) F} (value : Matrix (Fin n) (Fin n) F) (right_inv : A * value = 1) (left_inv : value * A = 1) (inv_eq : A⁻¹ = value) : InverseResult A
• singular {F : Type u} [Field F] {n : ℕ} {A : Matrix (Fin n) (Fin n) F} (kernel : Fin n → F) (nonzero : kernel ≠ 0) (annihilates : A.mulVec kernel = 0) (det_eq : A.det = 0) (inv_eq : A⁻¹ = 0) : InverseResult A

inductive HexMatrixTheory.SolveResult {F : Type u} [Field F] {n m : ℕ} (A : Matrix (Fin n) (Fin m) F) (b : Fin n → F) : Type u

The complete affine solution space or a certified separating row.

• consistent {F : Type u} [Field F] {n m : ℕ} {A : Matrix (Fin n) (Fin m) F} {b : Fin n → F} (value : Fin m → F) (nullity : ℕ) (basis : Matrix (Fin m) (Fin nullity) F) (solution : A.mulVec value = b) (complete : ∀ (x : Fin m → F), A.mulVec x = b ↔ ∃! c : Fin nullity → F, x = value + basis.mulVec c) : SolveResult A b
• inconsistent {F : Type u} [Field F] {n m : ℕ} {A : Matrix (Fin n) (Fin m) F} {b : Fin n → F} (separator : Fin n → F) (annihilates : Matrix.vecMul separator A = 0) (separates : separator ⬝ᵥ b ≠ 0) (impossible : ¬∃ (x : Fin m → F), A.mulVec x = b) : SolveResult A b

def HexMatrixTheory.SolveResult.statement {F : Type u} [Field F] {n m : ℕ} {A : Matrix (Fin n) (Fin m) F} {b : Fin n → F} : SolveResult A b → Prop

The full mathematical statement certified by either solve outcome.

Equations

• (HexMatrixTheory.SolveResult.consistent value nullity basis solution complete).statement = ∀ (x : Fin m → F), A.mulVec x = b ↔ ∃! c : Fin nullity → F, x = value + basis.mulVec c
• (HexMatrixTheory.SolveResult.inconsistent separator annihilates separates impossible).statement = ¬∃ (x : Fin m → F), A.mulVec x = b

theorem HexMatrixTheory.SolveResult.spec {F : Type u} [Field F] {n m : ℕ} {A : Matrix (Fin n) (Fin m) F} {b : Fin n → F} (r : SolveResult A b) : r.statement

Extract completeness or impossibility while retaining the literal result data.

def HexMatrixTheory.FieldCertificate.matrix (n m : ℕ) (a : Hex.Matrix.Lists.ScaledRows) : Matrix (Fin n) (Fin m) ℚ

Decoding belongs to soundness, outside the arithmetic reduction path.

Equations

• HexMatrixTheory.FieldCertificate.matrix n m a = HexMatrixTheory.ofLists n m (HexMatrixTheory.decodeRows a)

def HexMatrixTheory.FieldCertificate.vector (n : ℕ) (a : Hex.Matrix.Lists.Scaled) : Fin n → ℚ

Equations

• HexMatrixTheory.FieldCertificate.vector n a = HexMatrixTheory.vecOfList n (HexMatrixTheory.decodeList a)

theorem HexMatrixTheory.FieldCertificate.matrix_apply (n m : ℕ) (a : Hex.Matrix.Lists.ScaledRows) (i : Fin n) (j : Fin m) : matrix n m a i j = ↑(Hex.Matrix.Lists.get a.nums ↑i ↑j) / ↑a.denom

theorem HexMatrixTheory.FieldCertificate.vector_apply (n : ℕ) (a : Hex.Matrix.Lists.Scaled) (i : Fin n) : vector n a i = ↑(Hex.Matrix.Lists.entry 0 a.nums ↑i) / ↑a.denom

theorem HexMatrixTheory.FieldCertificate.matrix_valid {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} (h : Hex.Matrix.FieldLists.matrix n m a = true) : 0 < a.denom ∧ Hex.Matrix.Lists.shape n m a.nums = true

theorem HexMatrixTheory.FieldCertificate.vector_valid {n : ℕ} {a : Hex.Matrix.Lists.Scaled} (h : Hex.Matrix.FieldLists.vector n a = true) : 0 < a.denom ∧ a.nums.length = n

theorem HexMatrixTheory.FieldCertificate.mul_apply {n k m : ℕ} {a b : Hex.Matrix.Lists.ScaledRows} (ha : Hex.Matrix.Lists.shape n k a.nums = true) (i : Fin n) (j : Fin m) : (matrix n k a * matrix k m b) i j = ↑(Hex.Matrix.Lists.dot (Hex.Matrix.Lists.entry [] a.nums ↑i) (Hex.Matrix.Lists.column (↑j) b.nums)) / (↑a.denom * ↑b.denom)

theorem HexMatrixTheory.FieldCertificate.product {n k m : ℕ} {a b c : Hex.Matrix.Lists.ScaledRows} (ha : Hex.Matrix.FieldLists.matrix n k a = true) (hb : Hex.Matrix.FieldLists.matrix k m b = true) (hc : Hex.Matrix.FieldLists.matrix n m c = true) (h : Hex.Matrix.FieldLists.product n m a b c = true) : matrix n k a * matrix k m b = matrix n m c

Arbitrary accepted scaled products transport to Mathlib multiplication.

theorem HexMatrixTheory.FieldCertificate.inverse {n : ℕ} {a b : Hex.Matrix.Lists.ScaledRows} (ha : Hex.Matrix.FieldLists.matrix n n a = true) (hb : Hex.Matrix.FieldLists.matrix n n b = true) (h : Hex.Matrix.FieldLists.inverse n a b = true) : matrix n n a * matrix n n b = 1

The scaled identity check supplies the matrix inverse equation.

theorem HexMatrixTheory.FieldCertificate.inv_eq {F : Type u} [Field F] {n : ℕ} {A B : Matrix (Fin n) (Fin n) F} (hr : A * B = 1) (hl : B * A = 1) : A⁻¹ = B

A two-sided inverse determines Mathlib's nonsingular inverse.

theorem HexMatrixTheory.FieldCertificate.mulVec_apply {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} {v : Hex.Matrix.Lists.Scaled} (ha : Hex.Matrix.Lists.shape n m a.nums = true) (i : Fin n) : (matrix n m a).mulVec (vector m v) i = ↑(Hex.Matrix.Lists.dot (Hex.Matrix.Lists.entry [] a.nums ↑i) v.nums) / (↑a.denom * ↑v.denom)

theorem HexMatrixTheory.FieldCertificate.kernel {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} {v : Hex.Matrix.Lists.Scaled} (ha : Hex.Matrix.FieldLists.matrix n m a = true) (h : Hex.Matrix.FieldLists.kernel n a v = true) : (matrix n m a).mulVec (vector m v) = 0

theorem HexMatrixTheory.FieldCertificate.nonzero {n k : ℕ} {v : Hex.Matrix.Lists.Scaled} (hv : Hex.Matrix.FieldLists.vector n v = true) (hk : k < n) (h : Hex.Matrix.Lists.entry 0 v.nums k ≠ 0) : vector n v ≠ 0

theorem HexMatrixTheory.FieldCertificate.singular {F : Type u} [Field F] {n : ℕ} {A : Matrix (Fin n) (Fin n) F} {v : Fin n → F} (hv : v ≠ 0) (ha : A.mulVec v = 0) : A.det = 0 ∧ A⁻¹ = 0

A nonzero kernel vector certifies determinant zero, including the empty boundary.

theorem HexMatrixTheory.FieldCertificate.column_valid {n : ℕ} {v : Hex.Matrix.Lists.Scaled} (h : Hex.Matrix.FieldLists.vector n v = true) : Hex.Matrix.FieldLists.matrix n 1 (Hex.Matrix.FieldLists.columnBlock v) = true

theorem HexMatrixTheory.FieldCertificate.column_apply (n : ℕ) (v : Hex.Matrix.Lists.Scaled) (i : Fin n) : matrix n 1 (Hex.Matrix.FieldLists.columnBlock v) i 0 = vector n v i

theorem HexMatrixTheory.FieldCertificate.residual {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} {b x : Hex.Matrix.Lists.Scaled} (ha : Hex.Matrix.FieldLists.matrix n m a = true) (hb : Hex.Matrix.FieldLists.vector n b = true) (hx : Hex.Matrix.FieldLists.vector m x = true) (h : Hex.Matrix.FieldLists.product n 1 a (Hex.Matrix.FieldLists.columnBlock x) (Hex.Matrix.FieldLists.columnBlock b) = true) : (matrix n m a).mulVec (vector m x) = vector n b

A residual identity accepts every solution, regardless of the producer's choice.

theorem HexMatrixTheory.FieldCertificate.dot_apply {n : ℕ} {a b : Hex.Matrix.Lists.Scaled} (ha : a.nums.length = n) : vector n a ⬝ᵥ vector n b = ↑(Hex.Matrix.Lists.dot a.nums b.nums) / (↑a.denom * ↑b.denom)

theorem HexMatrixTheory.FieldCertificate.vecMul_apply {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} {y : Hex.Matrix.Lists.Scaled} (hy : y.nums.length = n) (j : Fin m) : Matrix.vecMul (vector n y) (matrix n m a) j = ↑(Hex.Matrix.Lists.dot y.nums (Hex.Matrix.Lists.column (↑j) a.nums)) / (↑y.denom * ↑a.denom)

theorem HexMatrixTheory.FieldCertificate.impossible {F : Type u} [Field F] {n m : ℕ} {A : Matrix (Fin n) (Fin m) F} {b y : Fin n → F} (hy : Matrix.vecMul y A = 0) (hb : y ⬝ᵥ b ≠ 0) : ¬∃ (x : Fin m → F), A.mulVec x = b

A separating row rules out every solution by associativity.

theorem HexMatrixTheory.FieldCertificate.separator {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} {b y : Hex.Matrix.Lists.Scaled} (hb : Hex.Matrix.FieldLists.vector n b = true) (hy : Hex.Matrix.FieldLists.vector n y = true) (h : Hex.Matrix.FieldLists.separator m a b y = true) : Matrix.vecMul (vector n y) (matrix n m a) = 0 ∧ vector n y ⬝ᵥ vector n b ≠ 0

Transport the two independently checked separator conditions.

structure HexMatrixTheory.FieldCertificate.EchelonChecks (n m : ℕ) (d : Hex.Matrix.SolveBasis) : Prop

The proof-facing reduced-row-echelon conditions extracted from a list check.

• rows : d.rank ≤ n
• cols : d.rank ≤ m
• length : d.pivots.length = d.rank
• bounds (i : Fin d.rank) : Hex.Matrix.Lists.entry m d.pivots ↑i < m
• sorted (i j : Fin d.rank) : i < j → Hex.Matrix.Lists.entry m d.pivots ↑i < Hex.Matrix.Lists.entry m d.pivots ↑j
• pivot (i : Fin d.rank) (j : Fin n) : Hex.Matrix.Lists.get d.reduced.nums (↑j) (Hex.Matrix.Lists.entry m d.pivots ↑i) = if ↑i = ↑j then ↑d.reduced.denom else 0
• trailing (i : Fin n) (j : Fin m) : d.rank ≤ ↑i → Hex.Matrix.Lists.get d.reduced.nums ↑i ↑j = 0

theorem HexMatrixTheory.FieldCertificate.echelon_spec {n m : ℕ} {d : Hex.Matrix.SolveBasis} (h : Hex.Matrix.FieldLists.echelon n m d = true) : EchelonChecks n m d

@[reducible, inline]

noncomputable abbrev HexMatrixTheory.FieldCertificate.echelonData {n m : ℕ} (d : Hex.Matrix.SolveBasis) (h : EchelonChecks n m d) : Hex.Matrix.RowEchelonData ℚ n m

Reconstruct executable data only in the soundness layer.

Equations

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

theorem HexMatrixTheory.FieldCertificate.echelonData_pivot {n m : ℕ} (d : Hex.Matrix.SolveBasis) (h : EchelonChecks n m d) (i : Fin d.rank) : ↑((echelonData d h).pivotCols.get i) = Hex.Matrix.Lists.entry m d.pivots ↑i

theorem HexMatrixTheory.FieldCertificate.rowReduced {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} {d : Hex.Matrix.SolveBasis} (ha : Hex.Matrix.FieldLists.matrix n m a = true) (hr : Hex.Matrix.FieldLists.matrix n m d.reduced = true) (hu : Hex.Matrix.FieldLists.matrix n n d.transform = true) (hw : Hex.Matrix.FieldLists.matrix n n d.inverse = true) (hprod : Hex.Matrix.FieldLists.product n m d.transform a d.reduced = true) (hinv : Hex.Matrix.FieldLists.inverse n d.transform d.inverse = true) (h : EchelonChecks n m d) : (matrixEquiv.symm (matrix n m a)).IsRowReduced (echelonData d h)

Checked row operations and canonical columns give an arbitrary IsRowReduced witness.

theorem HexMatrixTheory.FieldCertificate.pivots_list {n m : ℕ} {d : Hex.Matrix.SolveBasis} (h : EchelonChecks n m d) : List.map Fin.val (echelonData d h).pivotCols.toList = d.pivots

theorem HexMatrixTheory.FieldCertificate.free_list {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} {d : Hex.Matrix.SolveBasis} (h : EchelonChecks n m d) (E : (matrixEquiv.symm (matrix n m a)).IsRowReduced (echelonData d h)) : List.map Fin.val ⋯.freeColsList = List.filter (fun (j : ℕ) => !d.pivots.contains j) (List.range m)

theorem HexMatrixTheory.FieldCertificate.free_entry {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} {d : Hex.Matrix.SolveBasis} (h : EchelonChecks n m d) (E : (matrixEquiv.symm (matrix n m a)).IsRowReduced (echelonData d h)) (hf : d.free = List.filter (fun (j : ℕ) => !d.pivots.contains j) (List.range m)) (k : Fin (m - d.rank)) : ↑(⋯.freeCols.get k) = Hex.Matrix.Lists.entry m d.free ↑k

theorem HexMatrixTheory.FieldCertificate.basis_eq {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} {d : Hex.Matrix.SolveBasis} (h : EchelonChecks n m d) (E : (matrixEquiv.symm (matrix n m a)).IsRowReduced (echelonData d h)) (hr : Hex.Matrix.FieldLists.matrix n m d.reduced = true) (hb : Hex.Matrix.FieldLists.matrix m d.nullity d.basis = true) (hf : Hex.Matrix.FieldLists.freeData m d = true) : matrix m (m - d.rank) d.basis = matrixEquiv E.nullspaceMatrix

The checked basis is exactly the computed free-column basis of the reconstructed RREF.

theorem HexMatrixTheory.FieldCertificate.affine {F : Type u} [Field F] {n m : ℕ} {M : Hex.Matrix F n m} {D : Hex.Matrix.RowEchelonData F n m} (E : M.IsRowReduced D) {b : Fin n → F} {value : Fin m → F} (hvalue : (matrixEquiv M).mulVec value = b) (x : Fin m → F) : (matrixEquiv M).mulVec x = b ↔ ∃! c : Fin (m - D.rank) → F, x = value + (matrixEquiv E.nullspaceMatrix).mulVec c

Span completeness and independence give unique affine coordinates.

theorem HexMatrixTheory.FieldCertificate.complete {n m : ℕ} {a : Hex.Matrix.Lists.ScaledRows} {b : Hex.Matrix.Lists.Scaled} {d : Hex.Matrix.SolveBasis} (ha : Hex.Matrix.FieldLists.matrix n m a = true) (hb : Hex.Matrix.FieldLists.vector n b = true) (hr : Hex.Matrix.FieldLists.matrix n m d.reduced = true) (hu : Hex.Matrix.FieldLists.matrix n n d.transform = true) (hw : Hex.Matrix.FieldLists.matrix n n d.inverse = true) (hv : Hex.Matrix.FieldLists.vector m d.value = true) (hk : Hex.Matrix.FieldLists.matrix m d.nullity d.basis = true) (hprod : Hex.Matrix.FieldLists.product n m d.transform a d.reduced = true) (hinv : Hex.Matrix.FieldLists.inverse n d.transform d.inverse = true) (he : Hex.Matrix.FieldLists.echelon n m d = true) (hsol : Hex.Matrix.FieldLists.product n 1 a (Hex.Matrix.FieldLists.columnBlock d.value) (Hex.Matrix.FieldLists.columnBlock b) = true) (hfree : Hex.Matrix.FieldLists.freeData m d = true) : (matrix n m a).mulVec (vector m d.value) = vector n b ∧ ∀ (x : Fin m → ℚ), (matrix n m a).mulVec x = vector n b ↔ ∃! c : Fin d.nullity → ℚ, x = vector m d.value + (matrix m d.nullity d.basis).mulVec c

The complete check transports the quoted particular solution and full affine basis.

def HexMatrixTheory.InverseFacts {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) : Hex.Matrix.InverseWitness → Prop

All proof fields for one inverse outcome, bundled for a single kernel check.

Equations

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

def HexMatrixTheory.SolveFacts {n m : ℕ} (A : Matrix (Fin n) (Fin m) ℚ) (b : Fin n → ℚ) : Hex.Matrix.SolveWitness → Prop

All proof fields for one solve outcome.

Equations

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

theorem HexMatrixTheory.inverse_facts {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) (rows : List (List ℚ)) (c : Hex.Matrix.InverseWitness) (hA : A = ofLists n n rows) (hc : Hex.Matrix.checkInverseList n rows c = true) : InverseFacts A c

Soundness for both inverse certificate alternatives.

noncomputable def HexMatrixTheory.inverse_of_checkList {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) (rows : List (List ℚ)) (c : Hex.Matrix.InverseWitness) (hA : A = ofLists n n rows) (hc : Hex.Matrix.checkInverseList n rows c = true) : InverseResult A

Accepted inverse-product and kernel certificates produce either certified outcome.

Equations

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

theorem HexMatrixTheory.solve_of_checkList {n m : ℕ} (A : Matrix (Fin n) (Fin m) ℚ) (b : Fin n → ℚ) (x : Fin m → ℚ) (rows : List (List ℚ)) (rhs candidate : List ℚ) (hA : A = ofLists n m rows) (hb : b = vecOfList n rhs) (hx : x = vecOfList m candidate) (hc : Hex.Matrix.checkSolutionList n m rows rhs candidate = true) : A.mulVec x = b

Direct residual soundness for literal matrices and vectors.

theorem HexMatrixTheory.solve_facts {n m : ℕ} (A : Matrix (Fin n) (Fin m) ℚ) (b : Fin n → ℚ) (rows : List (List ℚ)) (rhs : List ℚ) (c : Hex.Matrix.SolveWitness) (hA : A = ofLists n m rows) (hb : b = vecOfList n rhs) (hc : Hex.Matrix.checkSolveList n m rows rhs c = true) : SolveFacts A b c

Soundness for both complete solve certificate alternatives.

noncomputable def HexMatrixTheory.solveResult_of_checkList {n m : ℕ} (A : Matrix (Fin n) (Fin m) ℚ) (b : Fin n → ℚ) (rows : List (List ℚ)) (rhs : List ℚ) (c : Hex.Matrix.SolveWitness) (hA : A = ofLists n m rows) (hb : b = vecOfList n rhs) (hc : Hex.Matrix.checkSolveList n m rows rhs c = true) : SolveResult A b

Complete positive and negative outcomes from arbitrary accepted list data.

Equations

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

def HexMatrixTheory.InverseResult.value? {F : Type u} [Field F] {n : ℕ} {A : Matrix (Fin n) (Fin n) F} : InverseResult A → Option (Matrix (Fin n) (Fin n) F)

The inverse matrix, when present.

Equations

• (HexMatrixTheory.InverseResult.invertible value right_inv left_inv inv_eq).value? = some value
• (HexMatrixTheory.InverseResult.singular kernel nonzero annihilates det_eq inv_eq).value? = none

def HexMatrixTheory.InverseResult.kernel? {F : Type u} [Field F] {n : ℕ} {A : Matrix (Fin n) (Fin n) F} : InverseResult A → Option (Fin n → F)

The nonzero kernel witness in the singular branch.

Equations

• (HexMatrixTheory.InverseResult.invertible value right_inv left_inv inv_eq).kernel? = none
• (HexMatrixTheory.InverseResult.singular kernel nonzero annihilates det_eq inv_eq).kernel? = some kernel

def HexMatrixTheory.SolveResult.data? {F : Type u} [Field F] {n m : ℕ} {A : Matrix (Fin n) (Fin m) F} {b : Fin n → F} : SolveResult A b → Option ((k : ℕ) × (Fin m → F) × Matrix (Fin m) (Fin k) F)

Literal nullity, particular solution and basis, when the system is consistent.

Equations

• (HexMatrixTheory.SolveResult.consistent value nullity basis solution complete).data? = some ⟨nullity, (value, basis)⟩
• (HexMatrixTheory.SolveResult.inconsistent separator annihilates separates impossible).data? = none

def HexMatrixTheory.SolveResult.separator? {F : Type u} [Field F] {n m : ℕ} {A : Matrix (Fin n) (Fin m) F} {b : Fin n → F} : SolveResult A b → Option (Fin n → F)

The separating row in the inconsistent branch.

Equations

• (HexMatrixTheory.SolveResult.consistent value nullity basis solution complete).separator? = none
• (HexMatrixTheory.SolveResult.inconsistent separator annihilates separates impossible).separator? = some separator

theorem HexMatrixTheory.inverse_value {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) (rows : List (List ℚ)) (a value : Hex.Matrix.Lists.ScaledRows) (hA : A = ofLists n n rows) (hc : Hex.Matrix.checkInverseList n rows (Hex.Matrix.InverseWitness.invertible a value) = true) : (inverse_of_checkList A rows (Hex.Matrix.InverseWitness.invertible a value) hA hc).value? = some (FieldCertificate.matrix n n value)

theorem HexMatrixTheory.inverse_kernel {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) (rows : List (List ℚ)) (a : Hex.Matrix.Lists.ScaledRows) (v : Hex.Matrix.Lists.Scaled) (k : ℕ) (hA : A = ofLists n n rows) (hc : Hex.Matrix.checkInverseList n rows (Hex.Matrix.InverseWitness.singular a v k) = true) : (inverse_of_checkList A rows (Hex.Matrix.InverseWitness.singular a v k) hA hc).kernel? = some (FieldCertificate.vector n v)

theorem HexMatrixTheory.solve_data {n m : ℕ} (A : Matrix (Fin n) (Fin m) ℚ) (b : Fin n → ℚ) (rows : List (List ℚ)) (rhs : List ℚ) (a : Hex.Matrix.Lists.ScaledRows) (v : Hex.Matrix.Lists.Scaled) (d : Hex.Matrix.SolveBasis) (hA : A = ofLists n m rows) (hb : b = vecOfList n rhs) (hc : Hex.Matrix.checkSolveList n m rows rhs (Hex.Matrix.SolveWitness.consistent a v d) = true) : (solveResult_of_checkList A b rows rhs (Hex.Matrix.SolveWitness.consistent a v d) hA hb hc).data? = some ⟨d.nullity, (FieldCertificate.vector m d.value, FieldCertificate.matrix m d.nullity d.basis)⟩

theorem HexMatrixTheory.solve_separator {n m : ℕ} (A : Matrix (Fin n) (Fin m) ℚ) (b : Fin n → ℚ) (rows : List (List ℚ)) (rhs : List ℚ) (a : Hex.Matrix.Lists.ScaledRows) (v y : Hex.Matrix.Lists.Scaled) (hA : A = ofLists n m rows) (hb : b = vecOfList n rhs) (hc : Hex.Matrix.checkSolveList n m rows rhs (Hex.Matrix.SolveWitness.inconsistent a v y) = true) : (solveResult_of_checkList A b rows rhs (Hex.Matrix.SolveWitness.inconsistent a v y) hA hb hc).separator? = some (FieldCertificate.vector n y)

theorem HexMatrixTheory.FieldCertificate.identify_matrix {n m : ℕ} (A : Matrix (Fin n) (Fin m) ℚ) (rows : List (List ℚ)) (s : Hex.Matrix.Lists.ScaledRows) (hA : A = ofLists n m rows) (hd : 0 < s.denom) (hs : Hex.Matrix.Lists.scaleRows s.denom rows s.nums = true) : A = matrix n m s

A literal matrix is identified with its scaled encoding by cross products.

theorem HexMatrixTheory.FieldCertificate.identify_vector {n : ℕ} (v : Fin n → ℚ) (xs : List ℚ) (s : Hex.Matrix.Lists.Scaled) (hv : v = vecOfList n xs) (hd : 0 < s.denom) (hs : Hex.Matrix.Lists.scaleRow s.denom xs s.nums = true) : v = vector n s

A literal vector is identified without normalizing decoded fractions.

theorem HexMatrixTheory.FieldCertificate.inverse_literal {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℚ} {a s : Hex.Matrix.Lists.ScaledRows} (h : InverseFacts A (Hex.Matrix.InverseWitness.invertible a s)) (hB : B = matrix n n s) : A * B = 1 ∧ B * A = 1 ∧ A⁻¹ = B

theorem HexMatrixTheory.FieldCertificate.singular_literal {n : ℕ} {A : Matrix (Fin n) (Fin n) ℚ} {v : Fin n → ℚ} {a : Hex.Matrix.Lists.ScaledRows} {s : Hex.Matrix.Lists.Scaled} {k : ℕ} (h : InverseFacts A (Hex.Matrix.InverseWitness.singular a s k)) (hv : v = vector n s) : v ≠ 0 ∧ A.mulVec v = 0 ∧ A.det = 0 ∧ A⁻¹ = 0

theorem HexMatrixTheory.FieldCertificate.solve_literal {n m : ℕ} {A : Matrix (Fin n) (Fin m) ℚ} {b : Fin n → ℚ} {a : Hex.Matrix.Lists.ScaledRows} {rhs : Hex.Matrix.Lists.Scaled} {d : Hex.Matrix.SolveBasis} {v : Fin m → ℚ} {B : Matrix (Fin m) (Fin d.nullity) ℚ} (h : SolveFacts A b (Hex.Matrix.SolveWitness.consistent a rhs d)) (hv : v = vector m d.value) (hB : B = matrix m d.nullity d.basis) : A.mulVec v = b ∧ ∀ (x : Fin m → ℚ), A.mulVec x = b ↔ ∃! c : Fin d.nullity → ℚ, x = v + B.mulVec c

theorem HexMatrixTheory.FieldCertificate.separator_literal {n m : ℕ} {A : Matrix (Fin n) (Fin m) ℚ} {b y : Fin n → ℚ} {a : Hex.Matrix.Lists.ScaledRows} {rhs s : Hex.Matrix.Lists.Scaled} (h : SolveFacts A b (Hex.Matrix.SolveWitness.inconsistent a rhs s)) (hy : y = vector n s) : Matrix.vecMul y A = 0 ∧ y ⬝ᵥ b ≠ 0 ∧ ¬∃ (x : Fin m → ℚ), A.mulVec x = b

theorem HexMatrixTheory.FieldCertificate.zero_matrix (n m : ℕ) : matrix n m { denom := 1, nums := List.replicate n (List.replicate m 0) } = 0