Plucker minor helpers

Encoding for the universal 3-term Plucker identity substrate.

def Hex.Matrix.skipIndex2 {n : Nat} (p q : Fin (n + 2)) (_hpq : ↑p < ↑q) (i : Fin n) : Fin (n + 2)

Embed Fin n into Fin (n + 2) while skipping two deleted indices p < q. This indexes minors with two removed rows.

The ordering proof _hpq is a phantom argument: it documents and pins the p < q precondition at call sites but is not consumed by the definition. This intentionally triggers the unusedArguments linter; the binder is kept deliberately (no @[nolint] exists in the Mathlib-free layer).

Equations

• Hex.Matrix.skipIndex2 p q _hpq i = if hi1 : ↑i < ↑p then ⟨↑i, ⋯⟩ else if hi2 : ↑i + 1 < ↑q then ⟨↑i + 1, ⋯⟩ else ⟨↑i + 2, ⋯⟩

@[simp]

theorem Hex.Matrix.skipIndex2_val_of_lt_p {n : Nat} (p q : Fin (n + 2)) (hpq : ↑p < ↑q) (i : Fin n) (h : ↑i < ↑p) : ↑(skipIndex2 p q hpq i) = ↑i

Below the first deleted index p, skipIndex2 is the identity: its value at i is i.

@[simp]

theorem Hex.Matrix.skipIndex2_val_of_between {n : Nat} (p q : Fin (n + 2)) (hpq : ↑p < ↑q) (i : Fin n) (h1 : ¬↑i < ↑p) (h2 : ↑i + 1 < ↑q) : ↑(skipIndex2 p q hpq i) = ↑i + 1

Between the two deleted indices p and q, skipIndex2 shifts up by one: its value at i is i + 1.

@[simp]

theorem Hex.Matrix.skipIndex2_val_of_ge_q {n : Nat} (p q : Fin (n + 2)) (hpq : ↑p < ↑q) (i : Fin n) (h1 : ¬↑i < ↑p) (h2 : ¬↑i + 1 < ↑q) : ↑(skipIndex2 p q hpq i) = ↑i + 2

At or beyond the second deleted index q, skipIndex2 shifts up by two: its value at i is i + 2.

theorem Hex.Matrix.skipIndex2_ne_p {n : Nat} (p q : Fin (n + 2)) (hpq : ↑p < ↑q) (i : Fin n) : skipIndex2 p q hpq i ≠ p

skipIndex2 p q hpq never lands on the first skipped index p.

theorem Hex.Matrix.skipIndex2_ne_q {n : Nat} (p q : Fin (n + 2)) (hpq : ↑p < ↑q) (i : Fin n) : skipIndex2 p q hpq i ≠ q

skipIndex2 p q hpq never lands on the second skipped index q.

def Hex.Matrix.mMatrix {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (v : Vector R (n + 2)) (p : Fin (n + 2)) : Matrix R (n + 1) (n + 1)

The (n + 1) × (n + 1) matrix obtained from [B | v] by deleting row p. Columns 0..n-1 carry the corresponding columns of B (restricted to rows other than p); the last column carries v (restricted to rows other than p).

Equations

• B.mMatrix v p = Hex.Matrix.ofFn fun (i j : Fin (n + 1)) => if hj : ↑j < n then B[(Hex.Matrix.skipIndex p i, ⟨↑j, hj⟩)] else v[Hex.Matrix.skipIndex p i]

theorem Hex.Matrix.mMatrix_entry_lt {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (v : Vector R (n + 2)) (p : Fin (n + 2)) (i j : Fin (n + 1)) (h : ↑j < n) : (B.mMatrix v p)[i][j] = B[skipIndex p i][⟨↑j, h⟩]

In a non-last column, mMatrix reads the corresponding entry of B through the row-deletion map.

theorem Hex.Matrix.mMatrix_entry_last {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (v : Vector R (n + 2)) (p : Fin (n + 2)) (i : Fin (n + 1)) : (B.mMatrix v p)[i][Fin.last n] = v[skipIndex p i]

The last column of mMatrix B v p is the vector v with row p deleted.

def Hex.Matrix.mDet {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (v : Vector R (n + 2)) (p : Fin (n + 2)) : R

The determinant of mMatrix B v p: the (n + 1)-maximal minor of [B | v] with row p deleted.

Equations

• B.mDet v p = (B.mMatrix v p).det

def Hex.Matrix.nMatrix {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (p q : Fin (n + 2)) (hpq : ↑p < ↑q) : Matrix R n n

The n × n matrix obtained from B by deleting rows p and q (in increasing-row order, with p.val < q.val).

Equations

• B.nMatrix p q hpq = Hex.Matrix.ofFn fun (i j : Fin n) => B[(Hex.Matrix.skipIndex2 p q hpq i, j)]

theorem Hex.Matrix.getElem_nMatrix {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (p q : Fin (n + 2)) (hpq : ↑p < ↑q) (i j : Fin n) : (B.nMatrix p q hpq)[i][j] = B[skipIndex2 p q hpq i][j]

Entry (i, j) of the two-row-deleted minor nMatrix B p q hpq is the source entry B[skipIndex2 p q hpq i][j].

def Hex.Matrix.nDet {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (p q : Fin (n + 2)) (hpq : ↑p < ↑q) : R

The determinant of nMatrix B p q hpq: the n × n minor of B with rows p, q deleted.

Equations

• B.nDet p q hpq = (B.nMatrix p q hpq).det

Row-move infrastructure for ordered four-row transports

These helpers transport the determinant of a matrix whose rows are an ordered nMatrix row sequence with one row displaced downward. Each "row-move" is realised as a chain of adjacent rowSwaps; the determinant picks up (-1) ^ k for a k-step move. The four row-content lemmas identify the rows of the moved matrix so consumers can pair them with getElem_nMatrix / skipIndex2 value lemmas.

One-row setRow transports to ordered nDet minors

For a < b < t in Fin (n + 2), the private helpers rowMoveUp_setRow_nMatrix_replace_first and _replace_second_eq_nMatrix identify the result of replacing the (t.val - 2)-th row of nMatrix B a b hab with B[a] (respectively B[b]) as a rowMoveUp of the ordered minor nMatrix B b t (resp. nMatrix B a t). The four ordered four-row transports det_setRow_nMatrix_r{2,3}_r{0,1}_eq_pow_mul_nDet_* combine these row equalities with det_rowMoveUp to give the signed nDet lemmas required by the ordered four-row Plucker assembly.

Double-row setRow transport to ordered nDet minors

For ordered rows r0 < r1 < r2 < r3, the double replacement setRow (setRow (nMatrix B r0 r1 h01) s2 B[r0]) s3 B[r1] (with s2 = ⟨r2.val - 2, _⟩ and s3 = ⟨r3.val - 2, _⟩) realises the row content of nMatrix B r2 r3 h23 with the inserted rows B[r0] and B[r1] displaced downward. Two rowMoveUp operations (first sliding B[r0] up to position r0.val, then B[r1] up to position r1.val - 1 of the intermediate matrix) reorder the rows back, contributing the combined sign (-1)^((r2 - r0 - 2) + (r3 - r1 - 2)). The intermediate identification uses rowMoveUp_setRow_of_gt to slide the outer setRow s3 B[r1] past the inner rowMoveUp, since s3.val > r2.val - 2 places it strictly above the inner move interval.

def Hex.Matrix.twoColMatrix {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (u v : Vector R (n + 2)) : Matrix R (n + 2) (n + 2)

The square matrix [B | u | v] formed by appending two vector columns to B : Matrix R (n + 2) n. The original B columns occupy positions 0..n-1; u occupies column n; v occupies the last column.

Equations

• B.twoColMatrix u v = Hex.Matrix.ofFn fun (i j : Fin (n + 2)) => if hj : ↑j < n then B[(i, ⟨↑j, hj⟩)] else if hju : ↑j = n then u[i] else v[i]

theorem Hex.Matrix.twoColMatrix_entry_lt {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (u v : Vector R (n + 2)) (i j : Fin (n + 2)) (h : ↑j < n) : (B.twoColMatrix u v)[i][j] = B[i][⟨↑j, h⟩]

In one of the original B columns, twoColMatrix agrees entrywise with B.

theorem Hex.Matrix.twoColMatrix_entry_penultimate {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (u v : Vector R (n + 2)) (i : Fin (n + 2)) : (B.twoColMatrix u v)[i][⟨n, ⋯⟩] = u[i]

The penultimate column of twoColMatrix B u v is u.

theorem Hex.Matrix.twoColMatrix_entry_last {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (u v : Vector R (n + 2)) (i : Fin (n + 2)) : (B.twoColMatrix u v)[i][Fin.last (n + 1)] = v[i]

The last column of twoColMatrix B u v is v.

def Hex.Matrix.twoColDet {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (u v : Vector R (n + 2)) : R

The determinant of [B | u | v].

Equations

• B.twoColDet u v = (B.twoColMatrix u v).det

theorem Hex.Matrix.deleteRowCol_twoColMatrix_last_eq_mMatrix {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (u v : Vector R (n + 2)) (p : Fin (n + 2)) : (B.twoColMatrix u v).deleteRowCol p (Fin.last (n + 1)) = B.mMatrix u p

Deleting row p and the final v column from [B | u | v] recovers the one-column augmented matrix mMatrix B u p.

theorem Hex.Matrix.twoColDet_eq_sum_mDet {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (u v : Vector R (n + 2)) : B.twoColDet u v = Fin.foldl (n + 2) (fun (acc : R) (p : Fin (n + 2)) => acc + v[p] * (cofactorSign p (Fin.last (n + 1)) * B.mDet u p)) 0

Laplace expansion of the two-column determinant along the final column, with the remaining minor identified as mDet B u p.

theorem Hex.Matrix.mMatrix_eq_setCol_last {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (v w : Vector R (n + 2)) (p : Fin (n + 2)) : B.mMatrix v p = (B.mMatrix w p).setCol (Fin.last n) fun (i : Fin (n + 1)) => v[skipIndex p i]

mMatrix B v p exposed as a setCol on its last column: the other columns come from B and are independent of v, while the last column carries fun i => v[skipIndex p i].

theorem Hex.Matrix.mDet_add_v {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (v w : Vector R (n + 2)) (p : Fin (n + 2)) : B.mDet (v + w) p = B.mDet v p + B.mDet w p

mDet is additive in the augmented vector column.

theorem Hex.Matrix.mDet_smul_v {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (c : R) (v : Vector R (n + 2)) (p : Fin (n + 2)) : B.mDet (c • v) p = c * B.mDet v p

mDet is homogeneous in the augmented vector column.

theorem Hex.Matrix.skipIndex_at_q_minus_one_eq_q_of_lt {n : Nat} (p q : Fin (n + 2)) (hpq : ↑p < ↑q) : skipIndex p ⟨↑q - 1, ⋯⟩ = q

For p < q, the unique row of Fin (n + 1) that maps to q under skipIndex p is ⟨q.val - 1, _⟩.

theorem Hex.Matrix.skipIndex_skipIndex_eq_skipIndex2_of_lt {n : Nat} (p q : Fin (n + 2)) (hpq : ↑p < ↑q) (i : Fin n) : skipIndex p (skipIndex ⟨↑q - 1, ⋯⟩ i) = skipIndex2 p q hpq i

For p < q, the chained skip skipIndex p ∘ skipIndex r_q (where r_q = q.val - 1) equals skipIndex2 p q hpq. This is the row-reindexing identity used to recover the n × n minor of B from the deleted-row-and-last-column minor of mMatrix B (Vector.unit q) p.

theorem Hex.Matrix.mDet_eq_sum_unit {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (v : Vector R (n + 2)) (p : Fin (n + 2)) : B.mDet v p = Fin.foldl (n + 2) (fun (acc : R) (q : Fin (n + 2)) => acc + v[q] * B.mDet (Vector.unit R q) p) 0

Expands the augmented vector column of mDet in the standard basis.

theorem Hex.Matrix.det_eq_signed_minor_of_col_basis {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (q c : Fin (n + 1)) (hcol : ∀ (r : Fin (n + 1)), M[r][c] = if r = q then 1 else 0) : M.det = cofactorSign q c * (M.deleteRowCol q c).det

Laplace expansion specialized to a column equal to a standard basis vector: if column c of M holds 1 at row q and 0 elsewhere, then det M equals the signed minor cofactorSign q c * det (deleteRowCol M q c).

theorem Hex.Matrix.deleteRowCol_mMatrix_at_q_minus_one_eq_nMatrix_of_lt {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (v : Vector R (n + 2)) (p q : Fin (n + 2)) (hpq : ↑p < ↑q) : (B.mMatrix v p).deleteRowCol ⟨↑q - 1, ⋯⟩ (Fin.last n) = B.nMatrix p q hpq

For p < q, deleting row r_q = q.val - 1 and the last column of mMatrix B v p recovers nMatrix B p q hpq, independent of v.

theorem Hex.Matrix.skipIndex_at_q_eq_q_of_gt {n : Nat} (p q : Fin (n + 2)) (hqp : ↑q < ↑p) : skipIndex p ⟨↑q, ⋯⟩ = q

For q < p, the unique row of Fin (n + 1) that maps to q under skipIndex p is ⟨q.val, _⟩.

theorem Hex.Matrix.skipIndex_skipIndex_eq_skipIndex2_of_gt {n : Nat} (p q : Fin (n + 2)) (hqp : ↑q < ↑p) (i : Fin n) : skipIndex p (skipIndex ⟨↑q, ⋯⟩ i) = skipIndex2 q p hqp i

For q < p, the chained skip skipIndex p ∘ skipIndex r_q (where r_q = ⟨q.val, _⟩) equals skipIndex2 q p hqp.

theorem Hex.Matrix.deleteRowCol_mMatrix_at_q_eq_nMatrix_of_gt {R : Type u} {n : Nat} (B : Matrix R (n + 2) n) (v : Vector R (n + 2)) (p q : Fin (n + 2)) (hqp : ↑q < ↑p) : (B.mMatrix v p).deleteRowCol ⟨↑q, ⋯⟩ (Fin.last n) = B.nMatrix q p hqp

For q < p, deleting row r_q = q.val and the last column of mMatrix B v p recovers nMatrix B q p hqp, independent of v.

theorem Hex.Matrix.mDet_unit_eq_signed_nDet_of_gt {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (p q : Fin (n + 2)) (hqp : ↑q < ↑p) : B.mDet (Vector.unit R q) p = cofactorSign ⟨↑q, ⋯⟩ (Fin.last n) * B.nDet q p hqp

Basis-vector evaluation of mDet when q < p: the basis vector e_q becomes the standard basis vector e_{q.val} in the last column of mMatrix B (Vector.unit q) p, so Laplace along that column recovers a signed n × n minor of B.

theorem Hex.Matrix.mDet_unit_eq_signed_nDet_of_lt {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (p q : Fin (n + 2)) (hpq : ↑p < ↑q) : B.mDet (Vector.unit R q) p = cofactorSign ⟨↑q - 1, ⋯⟩ (Fin.last n) * B.nDet p q hpq

Basis-vector evaluation of mDet when q > p: the basis vector e_q becomes the standard basis vector e_{q.val - 1} in the last column of mMatrix B (Vector.unit q) p, so Laplace along that column recovers a signed n × n minor of B.

theorem Hex.Matrix.mDet_unit_eq_zero_of_eq {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (p : Fin (n + 2)) : B.mDet (Vector.unit R p) p = 0

mDet B (Vector.unit p) p = 0: the basis vector e_p becomes the zero column inside mMatrix B (Vector.unit p) p after row p is deleted, so the determinant vanishes.

theorem Hex.Matrix.twoColDet_unit_unit_of_lt {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (a b : Fin (n + 2)) (hab : ↑a < ↑b) : B.twoColDet (Vector.unit R a) (Vector.unit R b) = cofactorSign b (Fin.last (n + 1)) * (cofactorSign ⟨↑a, ⋯⟩ (Fin.last n) * B.nDet a b hab)

Ordered basis-pair evaluation for twoColDet: if a < b, the only surviving ordered pair is the deleted-row pair (a, b).

theorem Hex.Matrix.twoColDet_unit_unit_of_gt {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (a b : Fin (n + 2)) (hba : ↑b < ↑a) : B.twoColDet (Vector.unit R a) (Vector.unit R b) = cofactorSign b (Fin.last (n + 1)) * (cofactorSign ⟨↑a - 1, ⋯⟩ (Fin.last n) * B.nDet b a hba)

Reverse ordered basis-pair evaluation for twoColDet: if b < a, the determinant recovers the same deleted-row pair with the reversed coefficient order.

theorem Hex.Matrix.twoColDet_unit_unit_of_eq {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (a : Fin (n + 2)) : B.twoColDet (Vector.unit R a) (Vector.unit R a) = 0

A repeated basis vector in the two appended columns makes twoColDet vanish.

theorem Hex.Matrix.twoColDet_unit_right {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (u : Vector R (n + 2)) (b : Fin (n + 2)) : B.twoColDet u (Vector.unit R b) = cofactorSign b (Fin.last (n + 1)) * B.mDet u b

Evaluation of twoColDet when the final appended column is a basis vector. This is the one-column Laplace expansion with the remaining mDet minor exposed directly.

theorem Hex.Matrix.twoColDet_eq_sum_unit_pairs {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (B : Matrix R (n + 2) n) (u v : Vector R (n + 2)) : B.twoColDet u v = Fin.foldl (n + 2) (fun (acc : R) (b : Fin (n + 2)) => acc + v[b] * Fin.foldl (n + 2) (fun (acc : R) (a : Fin (n + 2)) => acc + u[a] * B.twoColDet (Vector.unit R a) (Vector.unit R b)) 0) 0

Bilinear basis expansion of twoColDet over the two appended columns. The basis-pair terms are reduced by twoColDet_unit_unit_of_lt, twoColDet_unit_unit_of_gt, and twoColDet_unit_unit_of_eq.

theorem Hex.Matrix.det_plucker_three_term_consecutive_top {R : Type u} [Lean.Grind.CommRing R] {k : Nat} (B : Matrix R (k + 2) k) (v : Vector R (k + 2)) (alpha : Fin (k + 2)) (halpha : ↑alpha < k) : let pk := ⟨k, ⋯⟩; let plast := Fin.last (k + 1); B.mDet v alpha * B.nDet pk plast ⋯ - B.mDet v pk * B.nDet alpha plast ⋯ + B.mDet v plast * B.nDet alpha pk ⋯ = 0

Consecutive-top vector-column Plücker identity.

This is the Mathlib-free specialization used by the Gram/Bareiss trajectory: the three distinguished rows are alpha, k, and k+1 inside Fin (k + 2), so the top row is the last possible row and there is no q > p3 basis-vector case.