Core determinant correspondence between executable Hex.Matrix and Mathlib.

This module proves the central bridge lemma det_eq: the executable Leibniz determinant Hex.Matrix.det equals Matrix.det of the corresponding Mathlib matrix matrixEquiv M. It first matches Hex permutation vectors to Mathlib Equiv.Perm (PermutationVector.toPerm, equivs) and the inversion-count sign to Equiv.Perm.sign (detSign_eq_permSign). Building on det_eq, it translates matrixEquiv of leading prefixes, bordered minors, deleted rows/columns, and row updates, and ports the Desnanot-Jacobi and adjugate row-replacement identities (desnanot_jacobi_deleteRowCol_endpoints, det_mul_det_setRow_setRow_eq_cofactorRowPairing_mul_sub) into the Hex API, plus the ordered nMatrix/skipIndex2 row-transport helpers used downstream.

theorem HexMatrixMathlib.PermutationVector.get_injective_of_nodup {n : ℕ} {perm : Vector (Fin n) n} (hnodup : perm.toList.Nodup) : Function.Injective fun (i : Fin n) => perm[i]

noncomputable def HexMatrixMathlib.PermutationVector.toPerm {n : ℕ} (perm : Vector (Fin n) n) (hnodup : perm.toList.Nodup) : Equiv.Perm (Fin n)

Convert a Hex permutation vector into the corresponding Mathlib permutation.

Equations

• HexMatrixMathlib.PermutationVector.toPerm perm hnodup = Equiv.ofBijective (fun (i : Fin n) => perm[i]) ⋯

@[simp]

theorem HexMatrixMathlib.PermutationVector.toPerm_apply {n : ℕ} (perm : Vector (Fin n) n) (hnodup : perm.toList.Nodup) (i : Fin n) : (toPerm perm hnodup) i = perm[i]

theorem HexMatrixMathlib.PermutationVector.toPerm_injective {n : ℕ} : Function.Injective fun (p : { perm : Vector (Fin n) n // perm.toList.Nodup }) => toPerm ↑p ⋯

theorem HexMatrixMathlib.PermutationVector.vectorOfPerm_nodup {n : ℕ} (σ : Equiv.Perm (Fin n)) : (Vector.ofFn fun (i : Fin n) => σ i).toList.Nodup

theorem HexMatrixMathlib.PermutationVector.toPerm_vectorOfPerm {n : ℕ} (σ : Equiv.Perm (Fin n)) : toPerm (Vector.ofFn fun (i : Fin n) => σ i) ⋯ = σ

noncomputable def HexMatrixMathlib.PermutationVector.equivs (n : ℕ) : List (Equiv.Perm (Fin n))

Hex permutation vectors converted to Mathlib permutations, with proofs attached.

Equations

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

theorem HexMatrixMathlib.PermutationVector.equivs_complete {n : ℕ} (σ : Equiv.Perm (Fin n)) : σ ∈ equivs n

theorem HexMatrixMathlib.PermutationVector.equivs_nodup (n : ℕ) : (equivs n).Nodup

theorem HexMatrixMathlib.PermutationVector.detSign_vectorOfPerm_eq_permSign {R : Type u} {n : ℕ} [CommRing R] (σ : Equiv.Perm (Fin n)) : Hex.Matrix.detSign (Vector.ofFn fun (i : Fin n) => σ i) = ↑↑(Equiv.Perm.sign σ)

Hex's inversion-count determinant sign agrees with Mathlib's permutation sign.

theorem HexMatrixMathlib.PermutationVector.detSign_eq_permSign {R : Type u} {n : ℕ} [CommRing R] (perm : Vector (Fin n) n) (hnodup : perm.toList.Nodup) : Hex.Matrix.detSign perm = ↑↑(Equiv.Perm.sign (toPerm perm hnodup))

Hex's inversion-count determinant sign agrees with Mathlib's permutation sign.

@[simp]

theorem HexMatrixMathlib.detProduct_eq_matrixEquiv {R : Type u} {n : ℕ} [Lean.Grind.Ring R] (M : Hex.Matrix R n n) (perm : Vector (Fin n) n) : M.detProduct perm = List.foldl (fun (acc : R) (i : Fin n) => acc * matrixEquiv M i perm[i]) 1 (List.finRange n)

@[simp]

theorem HexMatrixMathlib.detTerm_eq_matrixEquiv {R : Type u} {n : ℕ} [Lean.Grind.Ring R] (M : Hex.Matrix R n n) (perm : Vector (Fin n) n) : M.detTerm perm = Hex.Matrix.detSign perm * List.foldl (fun (acc : R) (i : Fin n) => acc * matrixEquiv M i perm[i]) 1 (List.finRange n)

theorem HexMatrixMathlib.det_eq {R : Type u} {n : ℕ} [CommRing R] (M : Hex.Matrix R n n) : M.det = (matrixEquiv M).det

The executable Leibniz determinant Hex.Matrix.det agrees with Mathlib's Matrix.det of the corresponding Mathlib matrix matrixEquiv M. This is the bridge that lets a fact about Matrix.det be discharged by running the executable determinant, or the executable determinant be reasoned about with Mathlib's determinant theory.

theorem HexMatrixMathlib.matrixEquiv_borderedMinor {R : Type u} {n : ℕ} (M : Hex.Matrix R n n) (k : ℕ) (hk : k < n) (i j : Fin n) : matrixEquiv (M.borderedMinor k hk i j) = (matrixEquiv M).submatrix (fun (r : Fin (k + 1)) => if hr : ↑r < k then ⟨↑r, ⋯⟩ else i) fun (c : Fin (k + 1)) => if hc : ↑c < k then ⟨↑c, ⋯⟩ else j

matrixEquiv sends Hex bordered Bareiss minors to Mathlib submatrices.

theorem HexMatrixMathlib.det_principalSubmatrix_eq_submatrix_det {R : Type u} {n : ℕ} [CommRing R] (M : Hex.Matrix R n n) (k : ℕ) (hk : k ≤ n) : (M.principalSubmatrix k hk).det = ((matrixEquiv M).submatrix (fun (r : Fin k) => ⟨↑r, ⋯⟩) fun (c : Fin k) => ⟨↑c, ⋯⟩).det

Determinant form of matrixEquiv_principalSubmatrix.

theorem HexMatrixMathlib.det_borderedMinor_eq_submatrix_det {R : Type u} {n : ℕ} [CommRing R] (M : Hex.Matrix R n n) (k : ℕ) (hk : k < n) (i j : Fin n) : (M.borderedMinor k hk i j).det = ((matrixEquiv M).submatrix (fun (r : Fin (k + 1)) => if hr : ↑r < k then ⟨↑r, ⋯⟩ else i) fun (c : Fin (k + 1)) => if hc : ↑c < k then ⟨↑c, ⋯⟩ else j).det

Determinant form of matrixEquiv_borderedMinor.

theorem HexMatrixMathlib.matrixEquiv_deleteRowCol {R : Type u} {n : ℕ} (M : Hex.Matrix R (n + 1) (n + 1)) (row col : Fin (n + 1)) : matrixEquiv (M.deleteRowCol row col) = (matrixEquiv M).submatrix (Hex.Matrix.skipIndex row) (Hex.Matrix.skipIndex col)

Deleting a row and column in the Hex matrix representation is the same as submatrixing the Mathlib representation by the corresponding skip maps.

theorem HexMatrixMathlib.desnanot_jacobi_deleteRowCol_endpoints {R : Type u} {n : ℕ} [CommRing R] (M : Hex.Matrix R (n + 2) (n + 2)) : M.det * ((M.deleteRowCol 0 0).deleteRowCol (Fin.last n) (Fin.last n)).det = (M.deleteRowCol 0 0).det * (M.deleteRowCol (Fin.last (n + 1)) (Fin.last (n + 1))).det - (M.deleteRowCol 0 (Fin.last (n + 1))).det * (M.deleteRowCol (Fin.last (n + 1)) 0).det

Endpoint Hex-minor form of Desnanot-Jacobi. Reindex rows and columns first to use it for an arbitrary two-row/two-column choice.

theorem HexMatrixMathlib.desnanot_jacobi_matrixEquiv_reindex {R : Type u} {n : ℕ} [CommRing R] (M : Hex.Matrix R (n + 2) (n + 2)) (row col : Fin (n + 2) ≃ Fin (n + 2)) : have A := (matrixEquiv M).submatrix ⇑row ⇑col; A.det * (A.submatrix (Fin.succAbove 0 ∘ (Fin.last n).succAbove) (Fin.succAbove 0 ∘ (Fin.last n).succAbove)).det = (A.submatrix (Fin.succAbove 0) (Fin.succAbove 0)).det * (A.submatrix (Fin.last (n + 1)).succAbove (Fin.last (n + 1)).succAbove).det - (A.submatrix (Fin.succAbove 0) (Fin.last (n + 1)).succAbove).det * (A.submatrix (Fin.last (n + 1)).succAbove (Fin.succAbove 0)).det

Desnanot-Jacobi for an arbitrary pair of rows and columns, expressed as a row/column reindexing of a Hex matrix and proved in the Mathlib bridge layer.

Consumers choose row and col so that their two distinguished rows and columns are sent to 0 and Fin.last; the four one-row minors and the two-row/two-column interior minor are then the displayed submatrices of the reindexed matrix.

theorem HexMatrixMathlib.det_mul_cofactor_setRow_eq_cofactorRowPairing_mul_sub {R : Type u} {n : ℕ} [CommRing R] (M : Hex.Matrix R (n + 1) (n + 1)) (r s c : Fin (n + 1)) (rowVec : Vector R (n + 1)) (hrs : s ≠ r) : M.det * (M.setRow r rowVec).cofactor s c = M.cofactorRowPairing r rowVec * M.cofactor s c - M.cofactorRowPairing s rowVec * M.cofactor r c

One-row replacement cofactor identity in the Hex matrix API.

Replacing row r by u and then taking a cofactor along a distinct row s is controlled by the two cofactor-row pairings of u against the original matrix. This bridge-layer theorem is the row-replacement form of the Desnanot-Jacobi/adjugate relation needed by the two-row replacement Plucker transport.

theorem HexMatrixMathlib.det_mul_det_setRow_setRow_eq_cofactorRowPairing_mul_sub {R : Type u} {n : ℕ} [CommRing R] (M : Hex.Matrix R (n + 1) (n + 1)) (r s : Fin (n + 1)) (u v : Vector R (n + 1)) (hrs : s ≠ r) : M.det * ((M.setRow r u).setRow s v).det = M.cofactorRowPairing r u * M.cofactorRowPairing s v - M.cofactorRowPairing s u * M.cofactorRowPairing r v

Two-row replacement determinant identity in the Hex matrix API.

Replacing distinct rows r and s by u and v satisfies the adjugate two-row determinant relation, stated entirely in terms of Hex determinants and cofactor-row pairings.

Ordered nMatrix row transport helpers

theorem HexMatrixMathlib.skipIndex2_ordered_four_row_p2 {n : ℕ} (p1 p2 p3 q : Fin (n + 2)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : Hex.Matrix.skipIndex2 p1 q ⋯ ⟨↑p2 - 1, ⋯⟩ = p2

theorem HexMatrixMathlib.skipIndex2_ordered_four_row_p3 {n : ℕ} (p1 p2 p3 q : Fin (n + 2)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : Hex.Matrix.skipIndex2 p1 q ⋯ ⟨↑p3 - 1, ⋯⟩ = p3

theorem HexMatrixMathlib.nMatrix_ordered_four_row_p2 {R : Type u} {n : ℕ} (B : Hex.Matrix R (n + 2) n) (p1 p2 p3 q : Fin (n + 2)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : (B.nMatrix p1 q ⋯)[⟨↑p2 - 1, ⋯⟩] = B[p2]

theorem HexMatrixMathlib.nMatrix_ordered_four_row_p3 {R : Type u} {n : ℕ} (B : Hex.Matrix R (n + 2) n) (p1 p2 p3 q : Fin (n + 2)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : (B.nMatrix p1 q ⋯)[⟨↑p3 - 1, ⋯⟩] = B[p3]

theorem HexMatrixMathlib.skipIndex2_ordered_four_p1_p2_row_q {n : ℕ} (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : Hex.Matrix.skipIndex2 p1 p2 h12 ⟨↑q - 2, ⋯⟩ = q

theorem HexMatrixMathlib.skipIndex2_ordered_four_p1_p3_row_q {n : ℕ} (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : Hex.Matrix.skipIndex2 p1 p3 ⋯ ⟨↑q - 2, ⋯⟩ = q

theorem HexMatrixMathlib.nMatrix_ordered_four_p1_p2_row_q {R : Type u} {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : (B.nMatrix p1 p2 h12)[⟨↑q - 2, ⋯⟩] = B[q]

theorem HexMatrixMathlib.nMatrix_ordered_four_p1_p3_row_q {R : Type u} {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : (B.nMatrix p1 p3 ⋯)[⟨↑q - 2, ⋯⟩] = B[q]

theorem HexMatrixMathlib.ordered_four_row_p2_ne_p3 {n : ℕ} (p1 p2 p3 q : Fin (n + 2)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : ⟨↑p3 - 1, ⋯⟩ ≠ ⟨↑p2 - 1, ⋯⟩

theorem HexMatrixMathlib.nMatrix_ordered_four_setRow_p2_row_p3 {R : Type u} {n : ℕ} (B : Hex.Matrix R (n + 2) n) (p1 p2 p3 q : Fin (n + 2)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) (u : Vector R n) : ((B.nMatrix p1 q ⋯).setRow ⟨↑p2 - 1, ⋯⟩ u)[⟨↑p3 - 1, ⋯⟩] = B[p3]

theorem HexMatrixMathlib.nMatrix_ordered_four_setRow_p3_row_p2 {R : Type u} {n : ℕ} (B : Hex.Matrix R (n + 2) n) (p1 p2 p3 q : Fin (n + 2)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) (v : Vector R n) : ((B.nMatrix p1 q ⋯).setRow ⟨↑p3 - 1, ⋯⟩ v)[⟨↑p2 - 1, ⋯⟩] = B[p2]

theorem HexMatrixMathlib.ordered_four_cofactorRowPairing_p2_p1_eq_det_setRow {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have M := B.nMatrix p1 q ⋯; have r2 := ⟨↑p2 - 1, ⋯⟩; M.cofactorRowPairing r2 B[p1] = (M.setRow r2 B[p1]).det

theorem HexMatrixMathlib.ordered_four_cofactorRowPairing_p3_p1_eq_det_setRow {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have M := B.nMatrix p1 q ⋯; have r3 := ⟨↑p3 - 1, ⋯⟩; M.cofactorRowPairing r3 B[p1] = (M.setRow r3 B[p1]).det

theorem HexMatrixMathlib.ordered_four_cofactorRowPairing_p2_q_eq_det_setRow {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have M := B.nMatrix p1 q ⋯; have r2 := ⟨↑p2 - 1, ⋯⟩; M.cofactorRowPairing r2 B[q] = (M.setRow r2 B[q]).det

theorem HexMatrixMathlib.ordered_four_cofactorRowPairing_p3_q_eq_det_setRow {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have M := B.nMatrix p1 q ⋯; have r3 := ⟨↑p3 - 1, ⋯⟩; M.cofactorRowPairing r3 B[q] = (M.setRow r3 B[q]).det

Cyclic shift permutation for ordered four-row B[p1] transports

These helpers package the row permutation that moves B[p1] from position p1.val past the intermediate rows up to position p_t.val - 1. Together with Matrix.det_permute, they give signed nDet transports for the cofactorRowPairing M r? B[p1] pairings used by the ordered four-row Plucker assembly.

theorem HexMatrixMathlib.ordered_four_cofactorRowPairing_p2_p1_eq_pow_mul_nDet {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have M := B.nMatrix p1 q ⋯; have r2 := ⟨↑p2 - 1, ⋯⟩; have h2q := ⋯; M.cofactorRowPairing r2 B[p1] = (-1) ^ (↑p2 - ↑p1 - 1) * B.nDet p2 q h2q

Bridge-layer transport for the ordered four-row Plucker setup.

For p1 < p2 < p3 < q, the cofactor-row pairing cofactorRowPairing M r2 B[p1] of the ordered base matrix M = nMatrix B p1 q against B[p1] at row r2 := p2.val - 1 equals the signed nDet B p2 q minor with sign (-1)^(p2.val - p1.val - 1).

theorem HexMatrixMathlib.ordered_four_cofactorRowPairing_p3_p1_eq_pow_mul_nDet {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have M := B.nMatrix p1 q ⋯; have r3 := ⟨↑p3 - 1, ⋯⟩; have h3qq := h3q; M.cofactorRowPairing r3 B[p1] = (-1) ^ (↑p3 - ↑p1 - 1) * B.nDet p3 q h3qq

Bridge-layer transport for the ordered four-row Plucker setup.

For p1 < p2 < p3 < q, the cofactor-row pairing cofactorRowPairing M r3 B[p1] of the ordered base matrix M = nMatrix B p1 q against B[p1] at row r3 := p3.val - 1 equals the signed nDet B p3 q minor with sign (-1)^(p3.val - p1.val - 1).

theorem HexMatrixMathlib.ordered_four_cofactorRowPairing_p2_q_eq_pow_mul_nDet {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have M := B.nMatrix p1 q ⋯; have r2 := ⟨↑p2 - 1, ⋯⟩; M.cofactorRowPairing r2 B[q] = (-1) ^ (↑q - ↑p2 - 1) * B.nDet p1 p2 h12

Bridge-layer transport for the ordered four-row Plucker setup.

For p1 < p2 < p3 < q, the cofactor-row pairing cofactorRowPairing M r2 B[q] of the ordered base matrix M = nMatrix B p1 q against B[q] at row r2 := p2.val - 1 equals the signed nDet B p1 p2 minor with sign (-1)^(q.val - p2.val - 1).

theorem HexMatrixMathlib.ordered_four_cofactorRowPairing_p3_q_eq_pow_mul_nDet {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have M := B.nMatrix p1 q ⋯; have r3 := ⟨↑p3 - 1, ⋯⟩; M.cofactorRowPairing r3 B[q] = (-1) ^ (↑q - ↑p3 - 1) * B.nDet p1 p3 ⋯

Bridge-layer transport for the ordered four-row Plucker setup.

For p1 < p2 < p3 < q, the cofactor-row pairing cofactorRowPairing M r3 B[q] of the ordered base matrix M = nMatrix B p1 q against B[q] at row r3 := p3.val - 1 equals the signed nDet B p1 p3 minor with sign (-1)^(q.val - p3.val - 1).