Certificate construction for the Bareiss decomposition

certifyDecomposition constructs a proof of Echelon.Decomposition A L σ pivot from the given decomposition data. It proves that L * A_σ has the given pivots (through the product L * A_σ = U), and that L is lower triangular with nonzero diagonal entries.

The certify* functions assemble these proofs from facts about single entries, including the arithmetic equalities for the product and the non-zeroness for the diagonal entries of L and the pivots of U, which are established by the model's certifier (or the kernel).

Main definitions

• certifyDecomposition: builds the Echelon.Decomposition certificate from decomposition data.
• DecompositionCert: the internal certificate structure that includes the decomposition data, U and the product equation for downstream tactics.

Implementation notes

The elimination records its echelon form U, making the product L * A_σ = U a certificate obligation of its own.

The product is proved on the list representation which the kernel checks more cheaply.

def Mathlib.Tactic.Echelon.decideCertifier {u : Lean.Level} (α : Q(Type u)) : EntryCertifier α

The certifier that leaves each fact to the kernel's decide.

Equations

• Mathlib.Tactic.Echelon.decideCertifier α = { eq := fun (a b : Q(«$α»)) => Qq.mkDecideProofQ q(«$a» = «$b»), neZero := fun (_zα : Q(Zero «$α»)) (a : Q(«$α»)) => Qq.mkDecideProofQ q(«$a» ≠ 0) }

def Mathlib.Tactic.Echelon.certifyLowerTriangularDiagList {u : Lean.Level} {α : Q(Type u)} (certifier : EntryCertifier α) (zα : Q(Zero «$α»)) (k c : ℕ) (kQ cQ : Q(ℕ)) (rows : Q(List (List «$α»))) : Lean.MetaM Q(IsLowerTriangularDiagList «$kQ» «$cQ» «$rows»)

Construct the list-based IsLowerTriangularDiagList k c rows cert.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Echelon.certifyLowerTriangularDiagList certifier zα k 0 kQ cQ rows = pure q(⋯)

def Mathlib.Tactic.Echelon.certifyLowerTriangularDiag {u : Lean.Level} {m : ℕ} {α : Q(Type u)} (certifier : EntryCertifier α) (zα : Q(Zero «$α»)) (L : Matrix.ListMatrixLit α m m) : Lean.MetaM ((have a := L.matrix; Q(«$a».IsLowerTriangular)) × have a := L.matrix; Q(∀ (i : Fin «$m»), «$a».diag i ≠ 0))

Prove that L is lower triangular with a nonzero diagonal.

Equations

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

def Mathlib.Tactic.Echelon.certifyPivotedList {u : Lean.Level} {n : ℕ} {α : Q(Type u)} (certifier : EntryCertifier α) (zα : Q(Zero «$α»)) (cols : List ℕ) (pivots : Q(List (Fin «$n»))) (rows : Q(List (List «$α»))) : Lean.MetaM Q(IsPivotedList «$pivots» «$rows»)

Construct the list-based IsPivotedList pivots rows cert.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Echelon.certifyPivotedList certifier zα [] pivots rows = pure q(⋯)

def Mathlib.Tactic.Echelon.certifyPivotedBy {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (certifier : EntryCertifier α) (zα : Q(Zero «$α»)) (U : Matrix.ListMatrixLit α m n) (cols : List ℕ) (pivots : Q(List (Fin «$n»))) : Lean.MetaM (have a := U.matrix; Q(«$a».IsPivotedBy fun (i : Fin «$m») => pivotOfList «$pivots» ↑i))

Prove that U is pivoted by pivotOfList pivots from the rows of U, with certifier proving the pivot entries nonzero.

Equations

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

structure Mathlib.Tactic.Echelon.DecompositionCert {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (A : Q(Matrix (Fin «$m») (Fin «$n») «$α»)) : Type

An internal structure recording the Echelon.Decomposition certificate of A with its data, together with the intermediate certificates that downstream tactics reuse (the echelon form U and the product equation stated on it).

• L : Matrix.ListMatrixLit α m m

  The transformation matrix.

• swaps : Q(List (Fin «$m» × Fin «$m»))

  The row swaps.

• pivot : Q(Fin «$m» → WithTop (Fin «$n»))

  The pivot of the resulting echelon form.

• decomp : let a := self.L.matrix; Q(Echelon.Decomposition «$A» unknown_1 (Matrix.permOfSwaps unknown_2) unknown_3)

  The decomposition certificate from the theory.

• U : Matrix.ListMatrixLit α m n

  The echelon form.

• mul_eq : let a := self.U.matrix; let a_1 := self.L.matrix; Q(unknown_1 * «$A».submatrix (⇑(Matrix.permOfSwaps unknown_2)) id = unknown_3)

  The product equation.

def Mathlib.Tactic.Echelon.certifyDecomposition {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (certifier? : Option (EntryCertifier α)) (rα : Q(CommRing «$α»)) (A : Q(Matrix (Fin «$m») (Fin «$n») «$α»)) (entries : Array (Array Q(«$α»))) (data : BareissData Q(«$α»)) : Lean.MetaM (DecompositionCert rα A)

Build the DecompositionCert of A from the decomposition data and the parsed entries of A.

Equations

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