The last-row determinant recursion.

This module derives how the Leibniz determinant recurses on the final row and column. Inserting Fin.last n at the end of a permutation vector splits the sign and the product (detSign_insertAt_last, detProduct_insertAt_last, detTerm_insertAt_last), and the general insertion position is handled by detSign_insertAt_general / detTerm_insertAt_general. The payoff is the last-row factorisation det_eq_principalSubmatrix_mul_last: when the final row vanishes off the diagonal, the determinant is the determinant of the leading principal submatrix times the corner entry. Laplace expansion and the triangular diagonal-product formulas (HexDeterminant.Triangular) build on it. The enumeration combinatorics this recursion rides on (permutationVectors completeness and duplicate-freeness, raiseFinAbove / peelLastVector) live in HexDeterminant.Enumeration.

theorem Hex.Matrix.detSign_insertAt_last {R : Type u} [Lean.Grind.Ring R] {n : Nat} (v : Vector (Fin n) n) : detSign (insertAt (Fin.last n) (Vector.map Fin.castSucc v) (Fin.last n)) = detSign v

Appending the new largest value in the last position does not change the determinant sign, because it adds no inversions.

theorem Hex.Matrix.detSign_identity {R : Type u} [Lean.Grind.Ring R] (n : Nat) : detSign (Vector.ofFn fun (i : Fin n) => i) = 1

The identity permutation has positive determinant sign.

theorem Hex.Matrix.detProduct_insertAt_last {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (v : Vector (Fin n) n) : M.detProduct (insertAt (Fin.last n) (Vector.map Fin.castSucc v) (Fin.last n)) = (M.principalSubmatrix n ⋯).detProduct v * M[Fin.last n][Fin.last n]

Product reindexing for a permutation that fixes the final column. The Leibniz product splits into the product on the leading prefix times the final row/column entry.

theorem Hex.Matrix.detTerm_insertAt_last {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (v : Vector (Fin n) n) : M.detTerm (insertAt (Fin.last n) (Vector.map Fin.castSucc v) (Fin.last n)) = detSign v * ((M.principalSubmatrix n ⋯).detProduct v * M[Fin.last n][Fin.last n])

Leibniz-term reindexing for a permutation that fixes the final column. This packages the sign and product split used by last-row/last-column expansions.

theorem Hex.Matrix.det_eq_principalSubmatrix_mul_last {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (hrow : ∀ (j : Fin (n + 1)), ↑j < n → M[Fin.last n][j] = 0) : M.det = (M.principalSubmatrix n ⋯).det * M[Fin.last n][Fin.last n]

If the last row is zero before the diagonal entry, the determinant factors as the leading principal determinant times the bottom-right entry. This is the triangular-recursion step used by positivity and diagonal-product lemmas.