def Hex.Matrix.IsRowReduced.pivotLift {F : Type u} [Lean.Grind.Field F] {n m : Nat} (D : RowEchelonData F n m) : Matrix F m n

Place the pivot-row coordinates in their pivot columns, with zero free coordinates. Columns beyond the rank are zero.

Equations

• Hex.Matrix.IsRowReduced.pivotLift D = Hex.Matrix.ofFn fun (i : Fin m) (j : Fin n) => if h : ↑j < D.rank then if D.pivotCols.get ⟨↑j, h⟩ = i then 1 else 0 else 0

@[reducible, inline]

abbrev Hex.Matrix.SolveData {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) : Type u

A particular solution and the canonical nullspace matrix, sized by the computed rank of the coefficient matrix.

Equations

• A.SolveData = (Vector F m × Hex.Matrix F m (m - A.rowReduce_rank))

def Hex.Matrix.solveFrom {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} {A : Matrix F n m} {D : RowEchelonData F n m} (E : A.IsRowReduced D) (b : Vector F n) : Except (Vector F n) (Vector F m × Matrix F m (m - D.rank))

Solve using retained reduced-row-echelon data, preserving its basis dimension.

Equations

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

def Hex.Matrix.solve {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) (b : Vector F n) : Except (Vector F n) A.SolveData

Solve a field system completely. An error carries the first separating row of the RREF transform; success includes the canonical nullspace basis.

Equations

• A.solve b = Hex.Matrix.solveFrom ⋯ b

def Hex.Matrix.solve? {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) (b : Vector F n) : Option A.SolveData

The option view of solve, forgetting only the inconsistency witness.

Equations

• A.solve? b = (A.solve b).toOption

theorem Hex.Matrix.solve_error {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) (b y : Vector F n) : A.solve b = Except.error y → vecMul y A = 0 ∧ y.dotProduct b ≠ 0

Failure returns a left-kernel separator with nonzero pairing against the RHS.

theorem Hex.Matrix.solve?_isSome {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) (b : Vector F n) : (A.solve? b).isSome = true ↔ ∃ (x : Vector F m), A * x = b

Success is equivalent to mathematical consistency, with no resource-failure case.

theorem Hex.Matrix.solve?_eq_none {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) (b : Vector F n) : A.solve? b = none ↔ ¬∃ (x : Vector F m), A * x = b

The option API fails exactly on inconsistent systems.

theorem Hex.Matrix.solve?_none_witness {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) (b : Vector F n) : A.solve? b = none ↔ ∃ (y : Vector F n), vecMul y A = 0 ∧ y.dotProduct b ≠ 0

Inconsistency is equivalent to existence of a separating row functional.

theorem Hex.Matrix.solve?_spec {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) (b : Vector F n) (s : A.SolveData) : A.solve? b = some s → A * s.fst = b ∧ s.snd = A.nullspaceBasisMatrix ∧ ∀ (x : Vector F m), A * x = b ↔ ∃ (c : Vector F (m - A.rowReduce_rank)), x = s.fst + s.snd * c

Every solution is the particular solution plus a combination of the returned nullspace columns, and every such combination is a solution.

theorem Hex.Matrix.solve?_unique {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) (b : Vector F n) (s : A.SolveData) (c₁ c₂ : Vector F (m - A.rowReduce_rank)) : A.solve? b = some s → s.snd * c₁ = s.snd * c₂ → c₁ = c₂

The canonical free coordinates make nullspace coefficients unique.

theorem Hex.Matrix.solve?_free {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) (b : Vector F n) (s : A.SolveData) (h : A.solve? b = some s) (k : Fin (m - A.rowReduce_rank)) : s.fst[⋯.freeCols.get k] = 0

The particular solution sets every canonical free coordinate to zero.

theorem Hex.Matrix.solve?_noCols {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n : Nat} (A : Matrix F n 0) (b : Vector F n) : (A.solve? b).isSome = true ↔ b = 0

A system with no unknowns is consistent exactly for a zero RHS.

theorem Hex.Matrix.solve?_noRows {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {m : Nat} (A : Matrix F 0 m) (b : Vector F 0) : (A.solve? b).isSome = true

With no equations, every RHS is empty and solve always succeeds.