No-pivot Bareiss loop invariant for hex-matrix-mathlib.

This module proves the recursive bordered-minor invariant of the no-pivot Bareiss recurrence: after k regular Bareiss steps, the trailing entries of the working matrix agree with the corresponding bordered-minor determinants of the source matrix, and the previous pivot agrees with the determinant of the leading prefix of size k. As an immediate corollary, when all leading-prefix determinants are nonzero (NonzeroBareissPivots), the loop never takes the singular branch.

The invariant proof composes the bordered-minor stepMatrix update lemma (Hex.Matrix.stepMatrix_borderedMinor_update) with the bordered-minor specialization of Desnanot-Jacobi (desnanot_jacobi_borderedMinor in the parent module) and the exact-division equation (bareissExactDiv_borderedMinor_of_mul_eq).

theorem HexMatrixMathlib.borderedMinor_corner_eq_principalSubmatrix {n : ℕ} {R : Type u} [Lean.Grind.Ring R] (M : Hex.Matrix R n n) (k : ℕ) (hk : k < n) : M.borderedMinor k hk ⟨k, hk⟩ ⟨k, hk⟩ = M.principalSubmatrix (k + 1) ⋯

The k-bordered minor of M at the corner row/column ⟨k, hk⟩ is exactly the (k + 1)-leading prefix of M. This identifies the trailing-corner entry under the no-pivot Bareiss invariant with a leading-prefix determinant.

def HexMatrixMathlib.NonzeroBareissPivots {n : ℕ} (M : Hex.Matrix ℤ n n) : Prop

Hypothesis used by the no-pivot Bareiss soundness proof: every leading prefix determinant up to size n is nonzero.

Equations

• HexMatrixMathlib.NonzeroBareissPivots M = ∀ (k : Fin n), (M.principalSubmatrix (↑k + 1) ⋯).det ≠ 0

structure HexMatrixMathlib.BareissNoPivotInvariant {n : ℕ} (source : Hex.Matrix ℤ n n) (state : Hex.Matrix.BareissState n) : Prop

Bordered-minor invariant of the no-pivot Bareiss recurrence:

• singularStep is none (no pivot has been zero yet);
• the previous pivot equals the determinant of the leading prefix of size state.step (which is 1 for state.step = 0);
• the previous pivot is nonzero (so the next step's exact division is valid);
• every trailing entry (i, j) with state.step ≤ i.val and state.step ≤ j.val agrees with the determinant of the state.step-bordered minor with trailing row i and column j.

The implication on diagonal entries (state.matrix[k][k] agrees with the leading-prefix determinant of size k + 1) follows from trailing_eq taken at i = j = ⟨k, _⟩ together with borderedMinor_corner_eq_principalSubmatrix.

• singular_none : state.singularStep = none
• step_le : state.step ≤ n
• prevPivot_eq : state.prevPivot = (source.principalSubmatrix state.step ⋯).det
• prevPivot_ne : state.prevPivot ≠ 0
• trailing_eq (h : state.step < n) (i j : Fin n) : state.step ≤ ↑i → state.step ≤ ↑j → state.matrix[i][j] = (source.borderedMinor state.step h i j).det

theorem HexMatrixMathlib.bareissNoPivotInvariant_initial {n : ℕ} (M : Hex.Matrix ℤ n n) : BareissNoPivotInvariant M M.noPivotInitialState

The initial Bareiss no-pivot state satisfies the bordered-minor invariant: the matrix is the source itself, and the previous-pivot convention is det (principalSubmatrix _ 0 _) = 1.

theorem HexMatrixMathlib.bareissPivotInvariant_regular_no_swap {n : ℕ} (source : Hex.Matrix ℤ n n) (state : Hex.Matrix.BareissState n) (hinv : BareissNoPivotInvariant source state) (hDone : state.step + 1 < n) (hp : state.matrix[state.step][state.step] ≠ 0) : BareissNoPivotInvariant source { step := state.step + 1, matrix := state.matrix.stepMatrix state.step state.matrix[state.step][state.step] state.prevPivot, prevPivot := state.matrix[state.step][state.step], rowSwaps := state.rowSwaps, singularStep := none }

Public regular no-swap step surface for the row-pivoted Bareiss proof. When the current diagonal pivot is already nonzero, the row-pivoted loop takes the same regular step as the no-pivot loop, so the bordered-minor invariant is preserved by the existing no-pivot step proof.

theorem HexMatrixMathlib.bareissPivotNoPivot_column_eq_zero {n : ℕ} (state : Hex.Matrix.BareissState n) (hDone : state.step + 1 < n) (hp0 : state.matrix[state.step][state.step] = 0) (hfind : state.matrix.findPivot? ⟨state.step, ⋯⟩ (state.step + 1) = none) (i : Fin n) : state.step ≤ ↑i → state.matrix[i][⟨state.step, ⋯⟩] = 0

In the pivot-search failure branch, the current pivot column is zero at and below the current step.

theorem HexMatrixMathlib.bareissPivotNoPivot_principalSubmatrix_det_eq_zero {n : ℕ} (source : Hex.Matrix ℤ n n) (state : Hex.Matrix.BareissState n) (hinv : BareissNoPivotInvariant source state) (hDone : state.step + 1 < n) (hp0 : state.matrix[state.step][state.step] = 0) (hfind : state.matrix.findPivot? ⟨state.step, ⋯⟩ (state.step + 1) = none) : (source.principalSubmatrix (state.step + 1) ⋯).det = 0

In the pivot-search failure branch, the bordered-minor invariant identifies the zero current pivot with the next leading-prefix determinant.

theorem HexMatrixMathlib.borderedMinor_zero_column_succ_det_eq_zero_of_entries {n : ℕ} (source : Hex.Matrix ℤ n n) (k : ℕ) (hk : k < n) (hnext : k + 1 < n) (hprev : (source.principalSubmatrix k ⋯).det ≠ 0) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) (hcorner : (source.borderedMinor k hk ⟨k, ⋯⟩ ⟨k, ⋯⟩).det = 0) (hleft : (source.borderedMinor k hk i ⟨k, ⋯⟩).det = 0) : (source.borderedMinor (k + 1) hnext i j).det = 0

One-step zero propagation for the singular row-pivoted Bareiss branch.

If the current k-bordered trailing pivot column is zero at every row at or below k, then every (k + 1)-bordered minor one step deeper is zero. The proof is the Desnanot-Jacobi recurrence: both numerator terms contain a zero minor from the failed pivot column, and the previous leading-prefix pivot is nonzero, so the next determinant must vanish.

theorem HexMatrixMathlib.borderedMinor_zero_column_succ_det_eq_zero {n : ℕ} (source : Hex.Matrix ℤ n n) (k : ℕ) (hk : k < n) (hnext : k + 1 < n) (hprev : (source.principalSubmatrix k ⋯).det ≠ 0) (hcol : ∀ (i : Fin n), k ≤ ↑i → (source.borderedMinor k hk i ⟨k, hk⟩).det = 0) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) : (source.borderedMinor (k + 1) hnext i j).det = 0

Column-shaped form of borderedMinor_zero_column_succ_det_eq_zero_of_entries. This is the API used by the singular row-pivoted Bareiss branch: failed pivot search supplies a zero current pivot column, and the bordered-minor invariant transports that to this determinant column hypothesis.

theorem HexMatrixMathlib.bareissPivotRegularSwap_det {n : ℕ} (state : Hex.Matrix.BareissState n) (hDone : state.step + 1 < n) {pivot : Fin n} (hfind : state.matrix.findPivot? ⟨state.step, ⋯⟩ (state.step + 1) = some pivot) : (state.matrix.rowSwap ⟨state.step, ⋯⟩ pivot).det = -state.matrix.det

In the row-swap regular branch, the Hex determinant of the working matrix flips sign. This is the determinant-side row-swap fact needed by the row-pivoted Bareiss invariant.

theorem HexMatrixMathlib.bareissPivotInvariant_regular_swap {n : ℕ} (source : Hex.Matrix ℤ n n) (state : Hex.Matrix.BareissState n) (hinv : BareissNoPivotInvariant source state) (hDone : state.step + 1 < n) {pivot : Fin n} (hfind : state.matrix.findPivot? ⟨state.step, ⋯⟩ (state.step + 1) = some pivot) : BareissNoPivotInvariant (source.rowSwap ⟨state.step, ⋯⟩ pivot) { step := state.step, matrix := state.matrix.rowSwap ⟨state.step, ⋯⟩ pivot, prevPivot := state.prevPivot, rowSwaps := state.rowSwaps + 1, singularStep := state.singularStep }

Public regular swap-only step surface for the row-pivoted Bareiss proof. When the current diagonal pivot is zero and findPivot? returns a later row, the row-pivoted loop swaps source rows state.step and pivot before applying the stepMatrix update. Under that source rewrite, the bordered-minor invariant transports across the source row swap: the working matrix is rowSwap'd to match, the row-swap counter increments, and state.step is unchanged.

The subsequent stepMatrix update is then handled by bareissPivotInvariant_regular_no_swap applied to the swapped source.

theorem HexMatrixMathlib.bareissData_sign_succ {n : ℕ} (data : Hex.Matrix.BareissData n) : { matrix := data.matrix, rowSwaps := data.rowSwaps + 1, singularStep := data.singularStep }.sign = -data.sign

Incrementing the row-swap counter flips the Bareiss sign.

def HexMatrixMathlib.bareissStateSign {n : ℕ} (state : Hex.Matrix.BareissState n) : ℤ

Equations

• HexMatrixMathlib.bareissStateSign state = if state.rowSwaps % 2 = 0 then 1 else -1

def HexMatrixMathlib.BareissPivotInvariant {n : ℕ} (source : Hex.Matrix ℤ n n) (state : Hex.Matrix.BareissState n) : Prop

Row-pivoted Bareiss invariant. The current working state is interpreted as a no-pivot Bareiss state for a logical source obtained from the original source by the row swaps already performed; the sign field records the determinant relation back to the original source.

Equations

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

theorem HexMatrixMathlib.bareissPivotInvariant_initial {n : ℕ} (M : Hex.Matrix ℤ n n) : BareissPivotInvariant M M.noPivotInitialState

The initial row-pivoted Bareiss state satisfies the pivoted invariant with the original matrix as its logical source.

theorem HexMatrixMathlib.bareissPivotInvariant_regular_no_swap_step {n : ℕ} (source : Hex.Matrix ℤ n n) (state : Hex.Matrix.BareissState n) (hinv : BareissPivotInvariant source state) (hDone : state.step + 1 < n) (hp : state.matrix[state.step][state.step] ≠ 0) : BareissPivotInvariant source { step := state.step + 1, matrix := state.matrix.stepMatrix state.step state.matrix[state.step][state.step] state.prevPivot, prevPivot := state.matrix[state.step][state.step], rowSwaps := state.rowSwaps, singularStep := none }

A regular row-pivoted Bareiss step that does not swap rows preserves the pivoted invariant.

theorem HexMatrixMathlib.bareissPivotInvariant_regular_swap_step {n : ℕ} (source : Hex.Matrix ℤ n n) (state : Hex.Matrix.BareissState n) (hinv : BareissPivotInvariant source state) (hDone : state.step + 1 < n) {pivot : Fin n} (hfind : state.matrix.findPivot? ⟨state.step, ⋯⟩ (state.step + 1) = some pivot) : BareissPivotInvariant source { step := state.step + 1, matrix := (state.matrix.rowSwap ⟨state.step, ⋯⟩ pivot).stepMatrix state.step (state.matrix.rowSwap ⟨state.step, ⋯⟩ pivot)[state.step][state.step] state.prevPivot, prevPivot := (state.matrix.rowSwap ⟨state.step, ⋯⟩ pivot)[state.step][state.step], rowSwaps := state.rowSwaps + 1, singularStep := none }

A regular row-pivoted Bareiss step that swaps rows preserves the pivoted invariant.

theorem HexMatrixMathlib.pivotLoop_invariant_of_singularStep_eq_none {n : ℕ} (source : Hex.Matrix ℤ n n) (fuel : ℕ) (state : Hex.Matrix.BareissState n) (hinv : BareissPivotInvariant source state) (hregular : (Hex.Matrix.pivotLoop fuel state).singularStep = none) : BareissPivotInvariant source (Hex.Matrix.pivotLoop fuel state)

Recursive row-pivoted Bareiss invariant. If a pivotLoop run finishes with no singular step, then the final state still satisfies the pivoted invariant.

theorem HexMatrixMathlib.noPivotLoop_invariant {n : ℕ} (source : Hex.Matrix ℤ n n) (fuel : ℕ) (state : Hex.Matrix.BareissState n) (hinv : BareissNoPivotInvariant source state) (hpivots : ∀ (k : Fin n), state.step ≤ ↑k → (source.principalSubmatrix (↑k + 1) ⋯).det ≠ 0) : BareissNoPivotInvariant source (Hex.Matrix.noPivotLoop fuel state)

The recursive no-pivot Bareiss invariant: starting from any state that satisfies BareissNoPivotInvariant, if every future leading-prefix determinant (from state.step up to n) is nonzero, then the invariant continues to hold after running noPivotLoop for any amount of fuel.

theorem HexMatrixMathlib.bareissNoPivotInvariant_holds {n : ℕ} (M : Hex.Matrix ℤ n n) (h : NonzeroBareissPivots M) : BareissNoPivotInvariant M (Hex.Matrix.noPivotLoop n M.noPivotInitialState)

Under NonzeroBareissPivots, the no-pivot Bareiss recurrence run from the initial state satisfies the bordered-minor invariant.

theorem HexMatrixMathlib.noPivotLoop_singularStep_eq_none {n : ℕ} (M : Hex.Matrix ℤ n n) (h : NonzeroBareissPivots M) : (Hex.Matrix.noPivotLoop n M.noPivotInitialState).singularStep = none

Immediate consequence of the bordered-minor invariant: under NonzeroBareissPivots, the no-pivot Bareiss recurrence never takes the singular branch.

theorem HexMatrixMathlib.bareissNoPivotData_singularStep_eq_none {n : ℕ} (M : Hex.Matrix ℤ n n) (h : NonzeroBareissPivots M) : M.bareissNoPivotData.singularStep = none

Public corollary: under NonzeroBareissPivots, the executable no-pivot Bareiss data records no singular step.

theorem HexMatrixMathlib.noPivotLoop_invariant_of_singularStep_eq_none {n : ℕ} (source : Hex.Matrix ℤ n n) (fuel : ℕ) (state : Hex.Matrix.BareissState n) (hinv : BareissNoPivotInvariant source state) (hregular : (Hex.Matrix.noPivotLoop fuel state).singularStep = none) : BareissNoPivotInvariant source (Hex.Matrix.noPivotLoop fuel state)

Outcome-driven companion of noPivotLoop_invariant: if the no-pivot Bareiss loop run from a valid invariant state does NOT record a singular step during its fuel iterations, the invariant continues to hold afterward. The non-singular outcome guarantees every visited pivot was nonzero, which is the hypothesis the inductive step needs.

This is the no-pivot analog of pivotLoop_invariant_of_singularStep_eq_none.

theorem HexMatrixMathlib.bareissNoPivot_eq_det {n : ℕ} (M : Hex.Matrix ℤ n n) (h : NonzeroBareissPivots M) : M.bareissNoPivot = (matrixEquiv M).det

Capstone: under NonzeroBareissPivots, the no-pivot Bareiss recurrence computes the Mathlib determinant of the source matrix.

Failed Bareiss column dependence

Helper for the row-pivoted singular Bareiss branch: if the pivot search at level k fails (the entire k-bordered trailing column is zero) and the preceding leading-prefix determinant is nonzero, then there is an explicit linear combination of the columns of source — with coefficients given by the signed k × k cofactors of the leading prefix augmented with column k — that vanishes at every row. The coefficient on column k is Hex.Matrix.det (Hex.Matrix.principalSubmatrix source k _), which is nonzero by hypothesis. The follow-up issue closes the determinant via Matrix.det_updateCol_sum and the duplicate-column determinant identity.

def HexMatrixMathlib.failedBareissTopBlock {n : ℕ} (source : Hex.Matrix ℤ n n) (k : ℕ) (hk : k < n) : Matrix (Fin k) (Fin (k + 1)) ℤ

The k × (k+1) top block used to define the failed-pivot column dependence: leading k rows of source, restricted to columns 0..k-1 followed by column k.

Equations

• HexMatrixMathlib.failedBareissTopBlock source k hk s c = if hc : ↑c < k then HexMatrixMathlib.matrixEquiv source ⟨↑s, ⋯⟩ ⟨↑c, ⋯⟩ else HexMatrixMathlib.matrixEquiv source ⟨↑s, ⋯⟩ ⟨k, hk⟩

noncomputable def HexMatrixMathlib.failedBareissColumn {n : ℕ} (source : Hex.Matrix ℤ n n) (k : ℕ) (hk : k < n) : Fin n → ℤ

Coefficient function for the failed-pivot column dependence. The value at c is (-1)^(k + c.val) * det(failedBareissTopBlock with column c removed) for c.val ≤ k and 0 otherwise. The coefficient on column k is det (principalSubmatrix source k _); see failedBareissColumn_at_pivot.

Equations

• HexMatrixMathlib.failedBareissColumn source k hk c = if hc : ↑c ≤ k then (-1) ^ (k + ↑c) * ((HexMatrixMathlib.failedBareissTopBlock source k hk).submatrix id ⟨↑c, ⋯⟩.succAbove).det else 0

theorem HexMatrixMathlib.failedBareissColumn_above_pivot {n : ℕ} (source : Hex.Matrix ℤ n n) (k : ℕ) (hk : k < n) (c : Fin n) (hc : k < ↑c) : failedBareissColumn source k hk c = 0

theorem HexMatrixMathlib.failedBareissColumn_at_pivot {n : ℕ} (source : Hex.Matrix ℤ n n) (k : ℕ) (hk : k < n) : failedBareissColumn source k hk ⟨k, hk⟩ = (source.principalSubmatrix k ⋯).det

theorem HexMatrixMathlib.failed_bareiss_column_dependence {n : ℕ} (source : Hex.Matrix ℤ n n) (k : ℕ) (hk : k < n) (hprev : (source.principalSubmatrix k ⋯).det ≠ 0) (hcol : ∀ (i : Fin n), k ≤ ↑i → (source.borderedMinor k hk i ⟨k, hk⟩).det = 0) : ∃ (α : Fin n → ℤ), α ⟨k, hk⟩ ≠ 0 ∧ (∀ (c : Fin n), k < ↑c → α c = 0) ∧ (matrixEquiv source).mulVec α = 0

Failed Bareiss column dependence.

If the leading-prefix determinant of source at size k is nonzero, and the k-bordered minors with trailing column ⟨k, _⟩ all vanish for trailing rows at or beyond k, then there is an explicit linear combination of the columns of source — vanishing in every row — whose coefficient on column k equals the leading-prefix determinant (and is therefore nonzero). The coefficients on columns past k are zero.

The construction is the standard cofactor/adjugate trick: cofactor expansion along the last row of the (k+1)-bordered minors yields the coefficient function failedBareissColumn.

theorem HexMatrixMathlib.det_eq_zero_of_bareiss_failed_column {n : ℕ} (source : Hex.Matrix ℤ n n) (k : ℕ) (hk : k < n) (hprev : (source.principalSubmatrix k ⋯).det ≠ 0) (hcol : ∀ (i : Fin n), k ≤ ↑i → (source.borderedMinor k hk i ⟨k, hk⟩).det = 0) : source.det = 0

Failed Bareiss column ⟹ source determinant is zero.

If the leading-prefix determinant of source at size k is nonzero but every k-bordered minor with trailing column ⟨k, _⟩ and trailing row at or below k vanishes, then Hex.Matrix.det source = 0.

This is the Mathlib-side theorem consumed by the row-pivoted singular Bareiss packaging: failed pivot search at level k produces a zero pivot column, which the bordered-minor invariant transports to the determinant column hypothesis here. The proof obtains a nonzero kernel vector for matrixEquiv source from failed_bareiss_column_dependence, then closes the determinant via Matrix.exists_mulVec_eq_zero_iff.

theorem HexMatrixMathlib.bareissPivotInvariant_singular_no_pivot_det_eq_zero {n : ℕ} (source : Hex.Matrix ℤ n n) (state : Hex.Matrix.BareissState n) (hinv : BareissPivotInvariant source state) (hDone : state.step + 1 < n) (hp0 : state.matrix[state.step][state.step] = 0) (hfind : state.matrix.findPivot? ⟨state.step, ⋯⟩ (state.step + 1) = none) : source.det = 0

If row-pivoted Bareiss pivot search fails in a state satisfying the pivoted invariant, then the original source determinant is zero.

theorem HexMatrixMathlib.pivotLoop_singularStep_ne_none_det_eq_zero {n : ℕ} (source : Hex.Matrix ℤ n n) (fuel : ℕ) (state : Hex.Matrix.BareissState n) (hinv : BareissPivotInvariant source state) (hsing : (Hex.Matrix.pivotLoop fuel state).singularStep ≠ none) : source.det = 0

If a row-pivoted Bareiss loop reaches any singular step from a state satisfying the pivoted invariant, then the original source determinant is zero.

theorem HexMatrixMathlib.pivotLoop_singularStep_eq_some_det_eq_zero {n : ℕ} (source : Hex.Matrix ℤ n n) (fuel : ℕ) (state : Hex.Matrix.BareissState n) (hinv : BareissPivotInvariant source state) {k : ℕ} (hsing : (Hex.Matrix.pivotLoop fuel state).singularStep = some k) : source.det = 0

Some specific singular step recorded by pivotLoop forces the source determinant to be zero.

theorem HexMatrixMathlib.pivotLoop_initial_singularStep_ne_none_det_eq_zero {n : ℕ} (M : Hex.Matrix ℤ n n) (hsing : (Hex.Matrix.pivotLoop n M.noPivotInitialState).singularStep ≠ none) : M.det = 0

The public row-pivoted Bareiss loop, started from the initial state, records a singular step only when the input determinant is zero.

theorem HexMatrixMathlib.bareissData_singularStep_ne_none_det_eq_zero {n : ℕ} (M : Hex.Matrix ℤ n n) (hsing : M.bareissData.singularStep ≠ none) : M.det = 0

Data-facing singular branch theorem for the final row-pivoted Bareiss capstone.

theorem HexMatrixMathlib.bareissData_eq_mathlib_det {n : ℕ} (M : Hex.Matrix ℤ n n) : M.bareissData.det = (matrixEquiv M).det

Mathlib-side correctness theorem for the packaged row-pivoted Bareiss data: its .det field equals Mathlib's determinant of the corresponding matrix. Proven directly here by combining the row-pivot invariant with the singular-branch determinant-zero theorem above.

theorem HexMatrixMathlib.bareiss_eq_mathlib_det {n : ℕ} (M : Hex.Matrix ℤ n n) : M.bareiss = (matrixEquiv M).det

Row-pivoted Bareiss determinant soundness, exposed against Mathlib's determinant for downstream Mathlib-side callers.

theorem HexMatrixMathlib.noPivotLoop_full_eq_borderedMinor_det {n : ℕ} (M : Hex.Matrix ℤ n n) (k : ℕ) (hk : k + 1 < n) (a c : Fin n) (hak : k + 1 ≤ ↑a) (hck : k + 1 ≤ ↑c) (h_no_sing : (Hex.Matrix.noPivotLoop (k + 1) M.noPivotInitialState).singularStep = none) : (Hex.Matrix.noPivotLoop (k + 1) M.noPivotInitialState).matrix[a][c] = (M.borderedMinor (k + 1) hk a c).det

Off-step generalisation of the no-pivot Bareiss bordered-minor identification. After k + 1 no-pivot Bareiss iterations on M, every entry at (a, c) with k + 1 ≤ a.val, c.val equals the determinant of the (k + 2) × (k + 2) bordered minor of M with trailing row a and column c, provided the partial loop records no singular step.

Composes noPivotLoop_invariant_of_singularStep_eq_none (the invariant propagates through a non-singular partial pass), BareissNoPivotInvariant (the trailing-block entries equal bordered-minor determinants), and noPivotLoop_step_eq_add_of_singularStep_none (the partial pass advances step by exactly the fuel consumed).