Executable Bareiss determinant algorithm for hex-matrix.

This module implements fraction-free Bareiss elimination over Int in two layers: a no-pivot recurrence that follows the standard exact-division update, and a public row-pivoting wrapper that swaps in a nonzero pivot when needed and tracks the resulting determinant sign. The Mathlib-free layer exposes the executable data and state needed by later bridge proofs; it does not expose a theorem identifying the executable Bareiss determinant with the generic Leibniz determinant.

structure Hex.Matrix.BareissData (n : Nat) : Type

Output of an executable Bareiss elimination pass.

• matrix : Matrix Int n n

  Terminal matrix produced by the Bareiss pass. When singularStep = none, BareissData.det reads the last diagonal entry of this matrix, with the row-swap sign applied; for n = 0, the empty diagonal contributes 1.

• rowSwaps : Nat

  Number of row swaps performed by pivoting. Even parity contributes sign 1; odd parity contributes sign -1.

• singularStep : Option Nat

  The first elimination step that found a zero pivot and no replacement row. A value some k records that singular step and makes BareissData.det return 0; none means the run reached the terminal diagonal encoding.

def Hex.Matrix.BareissData.sign {n : Nat} (data : BareissData n) : Int

The determinant sign contributed by the recorded row swaps.

Equations

• data.sign = if data.rowSwaps % 2 = 0 then 1 else -1

def Hex.Matrix.BareissData.lastDiag? {n : Nat} (M : Matrix Int n n) : Option Int

Equations

• Hex.Matrix.BareissData.lastDiag? M_2 = none
• Hex.Matrix.BareissData.lastDiag? M_2 = some M_2[(⟨k, ⋯⟩, ⟨k, ⋯⟩)]

def Hex.Matrix.BareissData.det {n : Nat} (data : BareissData n) : Int

The determinant encoded by a Bareiss elimination result.

Equations

• data.det = match data.singularStep with | some val => 0 | none => match Hex.Matrix.BareissData.lastDiag? data.matrix with | some d => data.sign * d | none => data.sign

theorem Hex.Matrix.BareissData.det_eq_zero_of_singularStep {n : Nat} {data : BareissData n} {k : Nat} (h : data.singularStep = some k) : data.det = 0

A recorded singular step encodes determinant zero.

theorem Hex.Matrix.BareissData.det_succ_eq {k : Nat} (data : BareissData (k + 1)) (h : data.singularStep = none) : data.det = data.sign * data.matrix[⟨k, ⋯⟩][⟨k, ⋯⟩]

For a non-singular Bareiss elimination of a positive-size matrix, the encoded determinant is sign * (last diagonal entry).

theorem Hex.Matrix.BareissData.det_zero_eq (data : BareissData 0) (h : data.singularStep = none) : data.det = data.sign

For a non-singular Bareiss elimination of an empty matrix, the encoded determinant is the sign.

structure Hex.Matrix.BareissState (n : Nat) : Type

Internal state of the no-pivot Bareiss recurrence, exposed read-only for the Mathlib-side determinant proof.

• step : Nat

  Current elimination step. The next update, if any, uses this row and column as the pivot position.

• matrix : Matrix Int n n

  Current matrix carried by the Bareiss recurrence. Its terminal value is copied into BareissData.matrix by finish.

• prevPivot : Int

  Previous nonzero pivot used as the exact-division denominator; initially 1.

• rowSwaps : Nat

  Number of row swaps already performed by the pivoting wrapper. Even parity contributes determinant sign 1; odd parity contributes sign -1.

• singularStep : Option Nat

  First step at which the recurrence found a zero pivot and could not continue. A value some k is terminal evidence for the determinant-zero encoding; none means no singular step has been recorded.

@[extern lean_int_div_exact]

def Hex.Matrix.exactDiv (num denom : Int) : Int

Exact division used by the Bareiss recurrence.

Divisibility holds at every call site by the algorithmic invariant, so this function performs no runtime divisibility check: the @[extern] binding compiles the call directly to lean_int_div_exact, matching Int.divExact. The Lean-level reduction is the same num / denom that Int.divExact uses as its logical model.

Equations

• Hex.Matrix.exactDiv num denom = num / denom

theorem Hex.Matrix.exactDiv_eq_divExact {num denom : Int} (h : denom ∣ num) : exactDiv num denom = num.divExact denom h

When divisibility is known, exactDiv is the GMP-backed exact quotient.

def Hex.Matrix.findPivotAux {n : Nat} (M : Matrix Int n n) (col : Fin n) (start fuel : Nat) : Option (Fin n)

Search column col for a nonzero pivot at or below start.

Equations

• M.findPivotAux col start 0 = none
• M.findPivotAux col start fuel_2.succ = if h : start < n then have i := ⟨start, h⟩; if M[(i, col)] = 0 then M.findPivotAux col (start + 1) fuel_2 else some i else none

def Hex.Matrix.findPivot? {n : Nat} (M : Matrix Int n n) (col : Fin n) (start : Nat) : Option (Fin n)

Search column col for a nonzero pivot at or below start.

Equations

• M.findPivot? col start = M.findPivotAux col start (n - start)

theorem Hex.Matrix.findPivotAux_ge_start {n : Nat} (M : Matrix Int n n) (col : Fin n) (start fuel : Nat) {pivot : Fin n} (hfind : M.findPivotAux col start fuel = some pivot) : start ≤ ↑pivot

A pivot returned by findPivotAux is always at or below its starting row.

theorem Hex.Matrix.findPivot?_ge_start {n : Nat} (M : Matrix Int n n) (col : Fin n) (start : Nat) {pivot : Fin n} (hfind : M.findPivot? col start = some pivot) : start ≤ ↑pivot

A pivot returned by findPivot? is always at or below its starting row.

theorem Hex.Matrix.findPivotAux_eq_zero_of_none {n : Nat} (M : Matrix Int n n) (col : Fin n) (start fuel : Nat) (hfind : M.findPivotAux col start fuel = none) (i : Fin n) (hstart : start ≤ ↑i) (hfuel : ↑i < start + fuel) : M[i][col] = 0

If bounded pivot search fails, every checked entry in the pivot column is zero.

theorem Hex.Matrix.findPivot?_eq_zero_of_none {n : Nat} (M : Matrix Int n n) (col : Fin n) (start : Nat) (hfind : M.findPivot? col start = none) (i : Fin n) (hstart : start ≤ ↑i) : M[i][col] = 0

If pivot search fails, every entry in the searched suffix of the pivot column is zero.

theorem Hex.Matrix.findPivotAux_eq_none_of_zero {n : Nat} (M : Matrix Int n n) (col : Fin n) (start fuel : Nat) (hzero : ∀ (i : Fin n), start ≤ ↑i → ↑i < start + fuel → M[i][col] = 0) : M.findPivotAux col start fuel = none

If every entry in the bounded suffix searched by findPivotAux is zero, the search fails.

theorem Hex.Matrix.findPivot?_eq_none_of_zero {n : Nat} (M : Matrix Int n n) (col : Fin n) (start : Nat) (hzero : ∀ (i : Fin n), start ≤ ↑i → M[i][col] = 0) : M.findPivot? col start = none

If every entry in the suffix searched by findPivot? is zero, pivot search fails. This is the converse of findPivot?_eq_zero_of_none and lets callers turn a column-zero invariant into the executable no-replacement-pivot condition used by pivotLoop.

theorem Hex.Matrix.findPivotAux_some_ne_zero {n : Nat} (M : Matrix Int n n) (col : Fin n) (start fuel : Nat) {pivot : Fin n} (hfind : M.findPivotAux col start fuel = some pivot) : M[pivot][col] ≠ 0

A pivot returned by findPivotAux indexes a nonzero entry in the pivot column.

theorem Hex.Matrix.findPivot?_some_ne_zero {n : Nat} (M : Matrix Int n n) (col : Fin n) (start : Nat) {pivot : Fin n} (hfind : M.findPivot? col start = some pivot) : M[pivot][col] ≠ 0

A pivot returned by findPivot? indexes a nonzero entry in the pivot column. Lets row-pivoted Bareiss callers read off the nonzero post-swap pivot without unfolding the findPivotAux recursion.

def Hex.Matrix.stepMatrix {n : Nat} (M : Matrix Int n n) (k : Nat) (pivot prevPivot : Int) : Matrix Int n n

Apply one Bareiss update step to the trailing submatrix strictly below and to the right of the current pivot.

Built in place: rows at or above the pivot (i ≤ k) are left untouched, and only the rows below the pivot are rebuilt, via mapRowsIdx threading the matrix through per-row Vector.modifys. The pivot row is read once into pivotRow before the scatter (it is never mutated, since only rows i > k change), so the update reuses the outer vector and the finished prefix rows rather than reallocating the whole n × n matrix as a fresh ofFn.

Equations

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

theorem Hex.Matrix.stepMatrix_eq_ofFn {n : Nat} (M : Matrix Int n n) (k : Nat) (pivot prevPivot : Int) : M.stepMatrix k pivot prevPivot = ofFn fun (i j : Fin n) => if hkij : k < ↑i ∧ k < ↑j then have colK := ⟨k, ⋯⟩; have rowK := ⟨k, ⋯⟩; exactDiv (pivot * M[(i, j)] - M[(i, colK)] * M[(rowK, j)]) prevPivot else if k < ↑i ∧ ↑j = k then 0 else M[(i, j)]

The in-place stepMatrix agrees entrywise with the ofFn form it replaces; lets the existing entry lemmas reduce through the same body.

theorem Hex.Matrix.stepMatrix_eq_of_not_update {n : Nat} (M : Matrix Int n n) (k : Nat) (pivot prevPivot : Int) (i j : Fin n) (htrail : ¬(k < ↑i ∧ k < ↑j)) (hcol : ¬(k < ↑i ∧ ↑j = k)) : (M.stepMatrix k pivot prevPivot)[i][j] = M[i][j]

Outside the trailing update region and pivot column below the pivot, stepMatrix leaves entries unchanged.

theorem Hex.Matrix.stepMatrix_diag_of_le {n : Nat} (M : Matrix Int n n) (k : Nat) (pivot prevPivot : Int) (i : Fin n) (hi : ↑i ≤ k) : (M.stepMatrix k pivot prevPivot)[i][i] = M[i][i]

stepMatrix preserves diagonal entries whose index is at or before the current pivot step.

theorem Hex.Matrix.stepMatrix_pivot_col_below {n : Nat} (M : Matrix Int n n) (k : Nat) (pivot prevPivot : Int) (i colK : Fin n) (hi : k < ↑i) (hcolK : ↑colK = k) : (M.stepMatrix k pivot prevPivot)[i][colK] = 0

stepMatrix clears the pivot column below the current pivot.

theorem Hex.Matrix.stepMatrix_update_eq {n : Nat} (M : Matrix Int n n) (k : Nat) (pivot prevPivot : Int) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) : (M.stepMatrix k pivot prevPivot)[i][j] = let colK := ⟨k, ⋯⟩; have rowK := ⟨k, ⋯⟩; exactDiv (pivot * M[i][j] - M[i][colK] * M[rowK][j]) prevPivot

Entry formula for the trailing block updated by one Bareiss step.

theorem Hex.Matrix.stepMatrix_borderedMinor_update {n : Nat} (source current : Matrix Int n n) (k : Nat) (hk : k < n) (hnext : k + 1 < n) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) (pivot prevPivot : Int) (hpivot : pivot = (source.borderedMinor k hk ⟨k, ⋯⟩ ⟨k, ⋯⟩).det) (hentry : current[i][j] = (source.borderedMinor k hk i j).det) (hleft : current[i][⟨k, ⋯⟩] = (source.borderedMinor k hk i ⟨k, ⋯⟩).det) (htop : current[⟨k, ⋯⟩][j] = (source.borderedMinor k hk ⟨k, ⋯⟩ j).det) (hexact : exactDiv ((source.borderedMinor k hk ⟨k, ⋯⟩ ⟨k, ⋯⟩).det * (source.borderedMinor k hk i j).det - (source.borderedMinor k hk i ⟨k, ⋯⟩).det * (source.borderedMinor k hk ⟨k, ⋯⟩ j).det) prevPivot = (source.borderedMinor (k + 1) hnext i j).det) : (current.stepMatrix k pivot prevPivot)[i][j] = (source.borderedMinor (k + 1) hnext i j).det

If the current matrix entries already match bordered minors and exact division evaluates to the next bordered minor, then one stepMatrix update preserves the bordered-minor invariant at the updated entry.

theorem Hex.Matrix.bareissExactDiv_borderedMinor_of_mul_eq {n : Nat} (source : Matrix Int n n) (k : Nat) (hk : k < n) (hnext : k + 1 < n) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) (prevPivot : Int) (hprev_ne : prevPivot ≠ 0) (hdesnanot : (source.borderedMinor (k + 1) hnext i j).det * prevPivot = (source.borderedMinor k hk ⟨k, ⋯⟩ ⟨k, ⋯⟩).det * (source.borderedMinor k hk i j).det - (source.borderedMinor k hk i ⟨k, ⋯⟩).det * (source.borderedMinor k hk ⟨k, ⋯⟩ j).det) : exactDiv ((source.borderedMinor k hk ⟨k, ⋯⟩ ⟨k, ⋯⟩).det * (source.borderedMinor k hk i j).det - (source.borderedMinor k hk i ⟨k, ⋯⟩).det * (source.borderedMinor k hk ⟨k, ⋯⟩ j).det) prevPivot = (source.borderedMinor (k + 1) hnext i j).det

Exact-division equation for one Bareiss bordered-minor update.

Once a determinant identity supplies the numerator as nextMinor * prevPivot, this lemma packages it as the exactDiv premise expected by stepMatrix_borderedMinor_update.

structure Hex.Matrix.BareissArrayState : Type

• step : Nat
• matrix : Array (Array Int)
• prevPivot : Int
• rowSwaps : Nat
• singularStep : Option Nat

@[inline]

def Hex.Matrix.getEntry (rows : Array (Array Int)) (row col : Nat) : Int

Read an entry from an Array (Array Int) row-storage representation.

Exposed so downstream Mathlib-free clients (notably the shared scaled Gram-Schmidt loop in HexGramSchmidt.Int) can speak about array storage without re-deriving the conversion lemmas.

Equations

• Hex.Matrix.getEntry rows row col = rows[row]![col]!

def Hex.Matrix.matrixToRows {n : Nat} (M : Matrix Int n n) : Array (Array Int)

Pack a Matrix Int n n as an Array (Array Int) of size n × n. The representation used by the executable Bareiss array pass.

Equations

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

def Hex.Matrix.rowsToMatrix (rows : Array (Array Int)) (n : Nat) : Matrix Int n n

Unpack an Array (Array Int) row-storage representation back into a Matrix Int n n. Inverse-on-the-left of matrixToRows.

Equations

• Hex.Matrix.rowsToMatrix rows n = Hex.Matrix.ofFn fun (i j : Fin n) => Hex.Matrix.getEntry rows ↑i ↑j

theorem Hex.Matrix.getEntry_matrixToRows {n : Nat} (M : Matrix Int n n) (i j : Fin n) : getEntry M.matrixToRows ↑i ↑j = M[i][j]

Pointwise round-trip: getEntry (matrixToRows M) reads back the matrix entry at the same index.

theorem Hex.Matrix.rowsToMatrix_matrixToRows {n : Nat} (M : Matrix Int n n) : rowsToMatrix M.matrixToRows n = M

Reading back the array storage produced by matrixToRows recovers the original matrix.

def Hex.Matrix.pivotLoop {n : Nat} (fuel : Nat) (state : BareissState n) : BareissState n

Bareiss elimination with row pivoting. If a column has no nonzero pivot, the elimination aborts and the determinant is zero.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.pivotLoop 0 state = state

theorem Hex.Matrix.pivotLoop_zero_fuel {n : Nat} (state : BareissState n) : pivotLoop 0 state = state

With zero fuel, the row-pivoted Bareiss loop returns its input state.

theorem Hex.Matrix.pivotLoop_done {n : Nat} (fuel : Nat) (state : BareissState n) (hDone : ¬state.step + 1 < n) : pivotLoop (fuel + 1) state = state

If the current step is already past the last update step, the row-pivoted Bareiss loop returns its input state.

theorem Hex.Matrix.pivotLoop_regular_branch_no_swap {n : Nat} (fuel : Nat) (state : BareissState n) (hDone : state.step + 1 < n) (hp : state.matrix[state.step][state.step] ≠ 0) : pivotLoop (fuel + 1) state = pivotLoop fuel { 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 }

If the current row-pivoted Bareiss pivot is already nonzero, one loop iteration applies stepMatrix, advances the step, and recurses without changing the row-swap counter.

theorem Hex.Matrix.pivotLoop_singular_branch_no_pivot {n : Nat} (fuel : Nat) (state : 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) : pivotLoop (fuel + 1) state = { step := state.step, matrix := state.matrix, prevPivot := state.prevPivot, rowSwaps := state.rowSwaps, singularStep := some state.step }

If the current pivot is zero and pivot search finds no replacement row, the row-pivoted Bareiss loop records a singular step.

theorem Hex.Matrix.pivotLoop_regular_branch_swap {n : Nat} (fuel : Nat) (state : BareissState n) (hDone : state.step + 1 < n) (hp0 : state.matrix[state.step][state.step] = 0) {pivot : Fin n} (hfind : state.matrix.findPivot? ⟨state.step, ⋯⟩ (state.step + 1) = some pivot) (hp : (state.matrix.rowSwap ⟨state.step, ⋯⟩ pivot)[state.step][state.step] ≠ 0) : pivotLoop (fuel + 1) state = pivotLoop fuel { 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 }

If the current pivot is zero, pivot search finds a replacement row, and the swapped pivot is nonzero, one loop iteration swaps rows, applies stepMatrix, advances the step, increments the row-swap counter, and recurses.

def Hex.Matrix.bareissArrayState {n : Nat} (M : Matrix Int n n) : BareissArrayState

bareissArrayState runs the matrix-level Bareiss elimination via pivotLoop and repackages the reduced result as a BareissArrayState, storing the matrix row-by-row via matrixToRows.

Equations

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

def Hex.Matrix.arraySign (rowSwaps : Nat) : Int

arraySign is the determinant sign contributed by rowSwaps recorded row swaps, 1 for an even count and -1 for an odd count.

Equations

• Hex.Matrix.arraySign rowSwaps = if rowSwaps % 2 = 0 then 1 else -1

def Hex.Matrix.arrayLastDiag? (rows : Array (Array Int)) (n : Nat) : Option Int

arrayLastDiag? reads the last diagonal entry (n-1, n-1) of the reduced rows, returning none when n = 0.

Equations

• Hex.Matrix.arrayLastDiag? rows 0 = none
• Hex.Matrix.arrayLastDiag? rows fuel_1.succ = some (Hex.Matrix.getEntry rows fuel_1 fuel_1)

def Hex.Matrix.bareissArrayDet (state : BareissArrayState) (n : Nat) : Int

bareissArrayDet assembles the determinant value from the final array state, returning 0 when elimination recorded a singular column and the signed last diagonal entry otherwise.

Equations

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

def Hex.Matrix.finish {n : Nat} (state : BareissState n) : BareissData n

Package a Bareiss state as public elimination data.

Equations

• Hex.Matrix.finish state = { matrix := state.matrix, rowSwaps := state.rowSwaps, singularStep := state.singularStep }

def Hex.Matrix.noPivotLoop {n : Nat} (fuel : Nat) (state : BareissState n) : BareissState n

Bareiss elimination without pivoting. A zero pivot aborts and records the singular step.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.noPivotLoop 0 state = state

theorem Hex.Matrix.noPivotLoop_zero_fuel {n : Nat} (state : BareissState n) : noPivotLoop 0 state = state

With zero fuel, the no-pivot Bareiss loop returns its input state.

theorem Hex.Matrix.noPivotLoop_done {n : Nat} (fuel : Nat) (state : BareissState n) (hDone : ¬state.step + 1 < n) : noPivotLoop (fuel + 1) state = state

If the current step is already past the last update step, the no-pivot loop returns its input state.

theorem Hex.Matrix.noPivotLoop_singular_branch {n : Nat} (fuel : Nat) (state : BareissState n) (hDone : state.step + 1 < n) (hp : state.matrix[state.step][state.step] = 0) : noPivotLoop (fuel + 1) state = { step := state.step, matrix := state.matrix, prevPivot := state.prevPivot, rowSwaps := state.rowSwaps, singularStep := some state.step }

If the no-pivot loop sees a zero pivot before completion, it records the current step as singular.

theorem Hex.Matrix.noPivotLoop_regular_branch {n : Nat} (fuel : Nat) (state : BareissState n) (hDone : state.step + 1 < n) (hp : state.matrix[state.step][state.step] ≠ 0) : noPivotLoop (fuel + 1) state = noPivotLoop fuel { 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 }

If the current no-pivot Bareiss pivot is nonzero, one loop iteration applies stepMatrix, advances the step, and recurses on the remaining fuel.

theorem Hex.Matrix.noPivotLoop_matrix_entry_of_row_le_or_col_lt {n : Nat} (fuel : Nat) (state : BareissState n) (i j : Fin n) (hfixed : ↑i ≤ state.step ∨ ↑j < state.step) : (noPivotLoop fuel state).matrix[i][j] = state.matrix[i][j]

Entries in rows already processed, or in columns strictly before the current step, are unchanged by subsequent no-pivot loop iterations.

theorem Hex.Matrix.noPivotLoop_diag_of_le_step {n : Nat} (fuel : Nat) (state : BareissState n) (i : Fin n) (hi : ↑i ≤ state.step) : (noPivotLoop fuel state).matrix[i][i] = state.matrix[i][i]

Diagonal entries at or before the current step are unchanged by subsequent no-pivot loop iterations.

theorem Hex.Matrix.noPivotLoop_rowSwaps {n : Nat} (fuel : Nat) (state : BareissState n) : (noPivotLoop fuel state).rowSwaps = state.rowSwaps

The no-pivot loop never changes the row-swap counter.

theorem Hex.Matrix.noPivotLoop_id_at_done {n : Nat} (fuel : Nat) (state : BareissState n) (hDone : ¬state.step + 1 < n) : noPivotLoop fuel state = state

Once a no-pivot Bareiss state is already at the terminal step boundary, additional fuel leaves it unchanged.

theorem Hex.Matrix.noPivotLoop_id_at_singular_fixedpoint {n : Nat} (fuel : Nat) (state : BareissState n) (hDone : state.step + 1 < n) (hp : state.matrix[⟨state.step, ⋯⟩][⟨state.step, ⋯⟩] = 0) (hsing : state.singularStep = some state.step) : noPivotLoop fuel state = state

Once a no-pivot Bareiss state has recorded a zero pivot at the current step, additional fuel leaves that singular fixed point unchanged.

theorem Hex.Matrix.noPivotLoop_add {n : Nat} (a b : Nat) (state : BareissState n) : noPivotLoop (a + b) state = noPivotLoop b (noPivotLoop a state)

Fuel composition for the no-pivot Bareiss loop: running a + b units of fuel from state equals running b more units after a initial units.

theorem Hex.Matrix.noPivotLoop_step_eq_add_of_singularStep_none {n : Nat} (fuel : Nat) (state : BareissState n) (h_init : state.singularStep = none) (h_room : state.step + fuel + 1 ≤ n) (h_no_sing : (noPivotLoop fuel state).singularStep = none) : (noPivotLoop fuel state).step = state.step + fuel

When a no-pivot Bareiss run records no singular step and has enough room, the step field advances by exactly the amount of consumed fuel.

theorem Hex.Matrix.pivotLoop_eq_noPivotLoop_of_no_singular {n : Nat} (fuel : Nat) (state : BareissState n) (h_no_sing : (noPivotLoop fuel state).singularStep = none) : pivotLoop fuel state = noPivotLoop fuel state

When the no-pivot Bareiss loop completes fuel iterations without recording a singular step, the row-pivoted Bareiss loop produces an identical state: every diagonal pivot is nonzero, so the row search and swap branches of pivotLoop are never entered and both loops apply the same stepMatrix updates.

def Hex.Matrix.noPivotInitialState {n : Nat} (M : Matrix Int n n) : BareissState n

Initial state used by the no-pivot Bareiss recurrence.

Equations

• M.noPivotInitialState = { step := 0, matrix := M, prevPivot := 1, rowSwaps := 0, singularStep := none }

def Hex.Matrix.bareissNoPivotData {n : Nat} (M : Matrix Int n n) : BareissData n

Run the no-pivot Bareiss recurrence and return the final elimination data.

Equations

• M.bareissNoPivotData = Hex.Matrix.finish (Hex.Matrix.noPivotLoop n M.noPivotInitialState)

def Hex.Matrix.bareissNoPivot {n : Nat} (M : Matrix Int n n) : Int

Determinant computed by the no-pivot Bareiss recurrence.

Equations

• M.bareissNoPivot = M.bareissNoPivotData.det

def Hex.Matrix.bareissData {n : Nat} (M : Matrix Int n n) : BareissData n

Run the row-pivoted Bareiss elimination and return the final elimination data together with the swap/sign bookkeeping.

Equations

• M.bareissData = { matrix := Hex.Matrix.rowsToMatrix M.bareissArrayState.matrix n, rowSwaps := M.bareissArrayState.rowSwaps, singularStep := M.bareissArrayState.singularStep }

theorem Hex.Matrix.bareissData_eq_finish_pivotLoop {n : Nat} (M : Matrix Int n n) : M.bareissData = finish (pivotLoop n M.noPivotInitialState)

The packaged row-pivoted Bareiss data is exactly the structured pivot loop state finished into public determinant data. This is the equality consumed by the Mathlib determinant proof; array storage is erased by rowsToMatrix.

def Hex.Matrix.bareiss {n : Nat} (M : Matrix Int n n) : Int

Determinant computed by the row-pivoted Bareiss algorithm.

Equations

• M.bareiss = Hex.Matrix.bareissArrayDet M.bareissArrayState n

theorem Hex.Matrix.bareiss_eq_bareissData_det {n : Nat} (M : Matrix Int n n) : M.bareiss = M.bareissData.det

The public row-pivoted determinant agrees with the determinant encoded by bareissData. This separates executable array evaluation from the packaged elimination data used by correctness proofs.

theorem Hex.Matrix.bareiss_eq_noPivotLoop_last_of_no_singular {k : Nat} (M : Matrix Int (k + 1) (k + 1)) (h_no_sing : (noPivotLoop k M.noPivotInitialState).singularStep = none) : M.bareiss = (noPivotLoop k M.noPivotInitialState).matrix[Fin.last k][Fin.last k]

If the no-pivot Bareiss pass reaches the final pivot without recording a singular step, then the public row-pivoted bareiss determinant is exactly the no-pivot final diagonal entry.