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

Output of an executable Bareiss elimination pass.

• matrix : Matrix R 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 {R : Type u} {n : Nat} [One R] [Neg R] (data : BareissData R n) : R

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? {R : Type u} {n : Nat} (M : Matrix R n n) : Option R

Equations

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

def Hex.Matrix.BareissData.det {R : Type u} {n : Nat} [Zero R] [One R] [Neg R] [Mul R] (data : BareissData R n) : R

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 {R : Type u} {n : Nat} [Zero R] [One R] [Neg R] [Mul R] {data : BareissData R 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 {R : Type u} [Zero R] [One R] [Neg R] [Mul R] {k : Nat} (data : BareissData R (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 {R : Type u} [Zero R] [One R] [Neg R] [Mul R] (data : BareissData R 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 (R : Type u) (n : Nat) : Type u

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 R n n

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

• prevPivot : R

  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.

@[reducible, inline]

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

Compatibility alias for the exact-division primitive now owned by hex-arith. New code should use HexArith.Int.exactDiv.

Equations

• Hex.Matrix.exactDiv num denom = HexArith.Int.exactDiv 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 {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (M : Matrix R 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? {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (M : Matrix R 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 {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (M : Matrix R 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 {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (M : Matrix R 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 {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (M : Matrix R 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 {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (M : Matrix R 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 {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (M : Matrix R 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 {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (M : Matrix R 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 pivotLoopWith.

theorem Hex.Matrix.findPivotAux_some_ne_zero {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (M : Matrix R 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 {R : Type u} {n : Nat} [Zero R] [DecidableEq R] (M : Matrix R 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.

@[specialize #[5]]

def Hex.Matrix.stepMatrixWith {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] (quot : R → R → R) (M : Matrix R n n) (k : Nat) (pivot prevPivot : R) : Matrix R n n

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

Rows at or above the pivot (i ≤ k) are left untouched, and only the rows below the pivot are rebuilt. The pivot row is read once into pivotRow before the scatter (it is never mutated, since only rows i > k change). This mapRowsIdx form is the reference the entry lemmas reduce through; compiled code runs the per-entry in-place stepMatrixWithImpl via the @[csimp] below.

Equations

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

@[specialize #[5]]

def Hex.Matrix.stepMatrixWithImpl {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] (quot : R → R → R) (M : Matrix R n n) (k : Nat) (pivot prevPivot : R) : Matrix R n n

Fast in-place implementation of stepMatrixWith: each updated row is written through per-entry Matrix.modifyEntries updates of the flat backing buffer, with no per-row materialization or write-back. Swapped in for compiled code by the @[csimp] lemma below; stepMatrixWith stays the reference form for proofs.

Equations

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

theorem Hex.Matrix.stepMatrixWith_eq_ofFn {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] (quot : R → R → R) (M : Matrix R n n) (k : Nat) (pivot prevPivot : R) : stepMatrixWith quot M k pivot prevPivot = ofFn fun (i j : Fin n) => if hkij : k < ↑i ∧ k < ↑j then have colK := ⟨k, ⋯⟩; have rowK := ⟨k, ⋯⟩; quot (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 stepMatrixWith agrees entrywise with the ofFn form it replaces; lets the existing entry lemmas reduce through the same body.

@[csimp]

theorem Hex.Matrix.stepMatrixWith_eq_stepMatrixWithImpl : @stepMatrixWith = @stepMatrixWithImpl

theorem Hex.Matrix.stepMatrixWith_eq_of_not_update {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] (quot : R → R → R) (M : Matrix R n n) (k : Nat) (pivot prevPivot : R) (i j : Fin n) (htrail : ¬(k < ↑i ∧ k < ↑j)) (hcol : ¬(k < ↑i ∧ ↑j = k)) : (stepMatrixWith quot M k pivot prevPivot)[i][j] = M[i][j]

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

theorem Hex.Matrix.stepMatrixWith_diag_of_le {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] (quot : R → R → R) (M : Matrix R n n) (k : Nat) (pivot prevPivot : R) (i : Fin n) (hi : ↑i ≤ k) : (stepMatrixWith quot M k pivot prevPivot)[i][i] = M[i][i]

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

theorem Hex.Matrix.stepMatrixWith_pivot_col_below {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] (quot : R → R → R) (M : Matrix R n n) (k : Nat) (pivot prevPivot : R) (i colK : Fin n) (hi : k < ↑i) (hcolK : ↑colK = k) : (stepMatrixWith quot M k pivot prevPivot)[i][colK] = 0

stepMatrixWith clears the pivot column below the current pivot.

theorem Hex.Matrix.stepMatrixWith_update_eq {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] (quot : R → R → R) (M : Matrix R n n) (k : Nat) (pivot prevPivot : R) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) : (stepMatrixWith quot M k pivot prevPivot)[i][j] = let colK := ⟨k, ⋯⟩; have rowK := ⟨k, ⋯⟩; quot (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.stepMatrixWith_borderedMinor_update {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (quot : R → R → R) (source current : Matrix R n n) (k : Nat) (hk : k < n) (hnext : k + 1 < n) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) (pivot prevPivot : R) (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 : quot ((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) : (stepMatrixWith quot current 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 stepMatrixWith update preserves the bordered-minor invariant at the updated entry.

theorem Hex.Matrix.exactQuot_borderedMinor_of_mul_eq {R : Type u} {n : Nat} [Lean.Grind.CommRing R] (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Matrix R n n) (k : Nat) (hk : k < n) (hnext : k + 1 < n) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) (prevPivot : R) (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) : quot ((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 quot premise expected by stepMatrixWith_borderedMinor_update.

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

Integer specialization of exactQuot_borderedMinor_of_mul_eq.

structure Hex.Matrix.BareissArrayState (R : Type u) : Type u

Array-backed state used by the executable row-pivoted Bareiss loop.

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

@[inline]

def Hex.Matrix.getEntry {R : Type u} [Zero R] (rows : Array (Array R)) (row col : Nat) : R

Read an entry from an Array (Array R) 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.getD row #[]).getD col 0

def Hex.Matrix.matrixToRows {R : Type u} {n : Nat} [Zero R] (M : Matrix R n n) : Array (Array R)

Pack a Matrix R n n as an Array (Array R) 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 {R : Type u} [Zero R] (rows : Array (Array R)) (n : Nat) : Matrix R n n

Unpack an Array (Array R) row-storage representation back into a Matrix R 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 {R : Type u} {n : Nat} [Zero R] (M : Matrix R 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 {R : Type u} {n : Nat} [Zero R] (M : Matrix R n n) : rowsToMatrix M.matrixToRows n = M

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

@[specialize #[6]]

def Hex.Matrix.pivotLoopWith {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] (quot : R → R → R) (fuel : Nat) (state : BareissState R n) : BareissState R 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.pivotLoopWith quot 0 state = state

theorem Hex.Matrix.pivotLoopWith_zero_fuel {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (state : BareissState R n) : pivotLoopWith quot 0 state = state

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

theorem Hex.Matrix.pivotLoopWith_done {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (fuel : Nat) (state : BareissState R n) (hDone : ¬state.step + 1 < n) : pivotLoopWith quot (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.pivotLoopWith_of_regular_no_swap {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (fuel : Nat) (state : BareissState R n) (hDone : state.step + 1 < n) (hp : state.matrix[state.step][state.step] ≠ 0) : pivotLoopWith quot (fuel + 1) state = pivotLoopWith quot fuel { step := state.step + 1, matrix := stepMatrixWith quot state.matrix 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 stepMatrixWith quot, advances the step, and recurses without changing the row-swap counter.

theorem Hex.Matrix.pivotLoopWith_of_singular_no_pivot {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (fuel : Nat) (state : BareissState R n) (hDone : state.step + 1 < n) (hp0 : state.matrix[state.step][state.step] = 0) (hfind : state.matrix.findPivot? ⟨state.step, ⋯⟩ (state.step + 1) = none) : pivotLoopWith quot (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.pivotLoopWith_of_regular_swap {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (fuel : Nat) (state : BareissState R 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) : pivotLoopWith quot (fuel + 1) state = pivotLoopWith quot fuel { step := state.step + 1, matrix := stepMatrixWith quot (state.matrix.rowSwap ⟨state.step, ⋯⟩ pivot) 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 stepMatrixWith quot, advances the step, increments the row-swap counter, and recurses.

@[specialize #[7]]

def Hex.Matrix.bareissArrayStateWith {R : Type u} {n : Nat} [Zero R] [One R] [Sub R] [Mul R] [DecidableEq R] (quot : R → R → R) (M : Matrix R n n) : BareissArrayState R

bareissArrayStateWith runs the matrix-level Bareiss elimination via pivotLoopWith quot and repackages the reduced result as a BareissArrayState R, 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 {R : Type u} [One R] [Neg R] (rowSwaps : Nat) : R

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? {R : Type u} [Zero R] (rows : Array (Array R)) (n : Nat) : Option R

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 {R : Type u} [Zero R] [One R] [Neg R] [Mul R] (state : BareissArrayState R) (n : Nat) : R

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 {R : Type u} {n : Nat} (state : BareissState R n) : BareissData R n

Package a Bareiss state as public elimination data.

Equations

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

@[specialize #[6]]

def Hex.Matrix.noPivotLoopWith {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] (quot : R → R → R) (fuel : Nat) (state : BareissState R n) : BareissState R 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.noPivotLoopWith quot 0 state = state

theorem Hex.Matrix.noPivotLoopWith_zero_fuel {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (state : BareissState R n) : noPivotLoopWith quot 0 state = state

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

theorem Hex.Matrix.noPivotLoopWith_done {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (fuel : Nat) (state : BareissState R n) (hDone : ¬state.step + 1 < n) : noPivotLoopWith quot (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.noPivotLoopWith_of_singular {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (fuel : Nat) (state : BareissState R n) (hDone : state.step + 1 < n) (hp : state.matrix[state.step][state.step] = 0) : noPivotLoopWith quot (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.noPivotLoopWith_of_regular {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (fuel : Nat) (state : BareissState R n) (hDone : state.step + 1 < n) (hp : state.matrix[state.step][state.step] ≠ 0) : noPivotLoopWith quot (fuel + 1) state = noPivotLoopWith quot fuel { step := state.step + 1, matrix := stepMatrixWith quot state.matrix 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 stepMatrixWith quot, advances the step, and recurses on the remaining fuel.

theorem Hex.Matrix.noPivotLoopWith_matrix_entry_of_row_le_or_col_lt {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (fuel : Nat) (state : BareissState R n) (i j : Fin n) (hfixed : ↑i ≤ state.step ∨ ↑j < state.step) : (noPivotLoopWith quot 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.noPivotLoopWith_diag_of_le_step {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (fuel : Nat) (state : BareissState R n) (i : Fin n) (hi : ↑i ≤ state.step) : (noPivotLoopWith quot 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.noPivotLoopWith_rowSwaps {R : Type u} {n : Nat} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (fuel : Nat) (state : BareissState R n) : (noPivotLoopWith quot fuel state).rowSwaps = state.rowSwaps

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

theorem Hex.Matrix.noPivotLoopWith_id_at_done {R : Type u} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} {n : Nat} (fuel : Nat) (state : BareissState R n) (hDone : ¬state.step + 1 < n) : noPivotLoopWith quot fuel state = state

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

theorem Hex.Matrix.noPivotLoopWith_id_at_singular_fixedpoint {R : Type u} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} {n : Nat} (fuel : Nat) (state : BareissState R n) (hDone : state.step + 1 < n) (hp : state.matrix[⟨state.step, ⋯⟩][⟨state.step, ⋯⟩] = 0) (hsing : state.singularStep = some state.step) : noPivotLoopWith quot 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.noPivotLoopWith_add {R : Type u} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} {n : Nat} (a b : Nat) (state : BareissState R n) : noPivotLoopWith quot (a + b) state = noPivotLoopWith quot b (noPivotLoopWith quot 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.noPivotLoopWith_step_eq_add_of_singularStep_none {R : Type u} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} {n : Nat} (fuel : Nat) (state : BareissState R n) (h_init : state.singularStep = none) (h_room : state.step + fuel + 1 ≤ n) (h_no_sing : (noPivotLoopWith quot fuel state).singularStep = none) : (noPivotLoopWith quot 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.pivotLoopWith_eq_noPivotLoopWith_of_no_singular {R : Type u} [Zero R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} {n : Nat} (fuel : Nat) (state : BareissState R n) (h_no_sing : (noPivotLoopWith quot fuel state).singularStep = none) : pivotLoopWith quot fuel state = noPivotLoopWith quot 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 pivotLoopWith quot are never entered and both loops apply the same stepMatrixWith quot updates.

def Hex.Matrix.noPivotInitialState {R : Type u} {n : Nat} [One R] (M : Matrix R n n) : BareissState R 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.bareissNoPivotDataWith {R : Type u} {n : Nat} [Zero R] [One R] [Sub R] [Mul R] [DecidableEq R] (quot : R → R → R) (M : Matrix R n n) : BareissData R n

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

Equations

• Hex.Matrix.bareissNoPivotDataWith quot M = Hex.Matrix.finish (Hex.Matrix.noPivotLoopWith quot n M.noPivotInitialState)

theorem Hex.Matrix.bareissNoPivotDataWith_eq_finish {R : Type u} {n : Nat} [Zero R] [One R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (M : Matrix R n n) : bareissNoPivotDataWith quot M = finish (noPivotLoopWith quot n M.noPivotInitialState)

Characterisation of the generic no-pivot result by its completed loop state. Consumers can use this theorem without unfolding the public wrapper.

def Hex.Matrix.bareissNoPivotWith {R : Type u} {n : Nat} [Zero R] [One R] [Neg R] [Sub R] [Mul R] [DecidableEq R] (quot : R → R → R) (M : Matrix R n n) : R

Determinant computed by the no-pivot Bareiss recurrence.

Equations

• Hex.Matrix.bareissNoPivotWith quot M = (Hex.Matrix.bareissNoPivotDataWith quot M).det

def Hex.Matrix.bareissDataWith {R : Type u} {n : Nat} [Zero R] [One R] [Sub R] [Mul R] [DecidableEq R] (quot : R → R → R) (M : Matrix R n n) : BareissData R n

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

Equations

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

theorem Hex.Matrix.bareissDataWith_eq_finish_pivotLoopWith {R : Type u} {n : Nat} [Zero R] [One R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (M : Matrix R n n) : bareissDataWith quot M = finish (pivotLoopWith quot 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.

@[specialize #[8]]

def Hex.Matrix.bareissWith {R : Type u} {n : Nat} [Zero R] [One R] [Neg R] [Sub R] [Mul R] [DecidableEq R] (quot : R → R → R) (M : Matrix R n n) : R

Determinant computed by the row-pivoted Bareiss algorithm.

Equations

• Hex.Matrix.bareissWith quot M = Hex.Matrix.bareissArrayDet (Hex.Matrix.bareissArrayStateWith quot M) n

theorem Hex.Matrix.bareissWith_eq_bareissDataWith_det {R : Type u} {n : Nat} [Zero R] [One R] [Neg R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} (M : Matrix R n n) : bareissWith quot M = (bareissDataWith quot M).det

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

theorem Hex.Matrix.bareissWith_eq_noPivotLoopWith_last_of_no_singular {R : Type u} [Zero R] [One R] [Neg R] [Sub R] [Mul R] [DecidableEq R] {quot : R → R → R} {k : Nat} (M : Matrix R (k + 1) (k + 1)) (h_no_sing : (noPivotLoopWith quot k M.noPivotInitialState).singularStep = none) (hone : ∀ (x : R), 1 * x = x) : bareissWith quot M = (noPivotLoopWith quot 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 bareissWith determinant is exactly the no-pivot final diagonal entry.

@[reducible, inline]

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

Integer specialization of the generic Bareiss matrix update.

Equations

• M.stepMatrix k pivot prevPivot = Hex.Matrix.stepMatrixWith Hex.Matrix.exactDiv M k pivot prevPivot

@[reducible, inline]

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

Integer specialization of the generic row-pivoted Bareiss loop.

Equations

• Hex.Matrix.pivotLoop fuel state = Hex.Matrix.pivotLoopWith Hex.Matrix.exactDiv fuel state

@[reducible, inline]

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

Integer specialization of the generic no-pivot Bareiss loop.

Equations

• Hex.Matrix.noPivotLoop fuel state = Hex.Matrix.noPivotLoopWith Hex.Matrix.exactDiv fuel state

@[reducible, inline]

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

Integer specialization returning the executable array-backed state.

Equations

• M.bareissArrayState = Hex.Matrix.bareissArrayStateWith Hex.Matrix.exactDiv M

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

Integer specialization returning no-pivot elimination data.

Equations

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

@[reducible, inline]

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

Integer specialization of the no-pivot Bareiss determinant.

Equations

• M.bareissNoPivot = Hex.Matrix.bareissNoPivotWith Hex.Matrix.exactDiv M

@[reducible, inline]

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

Integer specialization returning row-pivoted elimination data.

Equations

• M.bareissData = Hex.Matrix.bareissDataWith Hex.Matrix.exactDiv M

@[reducible, inline]

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

Integer specialization of the row-pivoted Bareiss determinant.

Equations

• M.bareiss = Hex.Matrix.bareissWith Hex.Matrix.exactDiv M

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)]

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]

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]

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

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

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

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

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

theorem Hex.Matrix.pivotLoop_of_regular_no_swap {n : Nat} (fuel : Nat) (state : BareissState Int 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 }

theorem Hex.Matrix.pivotLoop_of_singular_no_pivot {n : Nat} (fuel : Nat) (state : BareissState Int 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 }

theorem Hex.Matrix.pivotLoop_of_regular_swap {n : Nat} (fuel : Nat) (state : BareissState Int 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 }

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

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

theorem Hex.Matrix.noPivotLoop_of_singular {n : Nat} (fuel : Nat) (state : BareissState Int 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 }

theorem Hex.Matrix.noPivotLoop_of_regular {n : Nat} (fuel : Nat) (state : BareissState Int 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 }

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

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

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

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

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

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

theorem Hex.Matrix.noPivotLoop_step_eq_add_of_singularStep_none {n : Nat} (fuel : Nat) (state : BareissState Int 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

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

theorem Hex.Matrix.bareissNoPivotData_eq_finish {n : Nat} (M : Matrix Int n n) : M.bareissNoPivotData = finish (noPivotLoop n M.noPivotInitialState)

The integer no-pivot result is the completed integer no-pivot loop state.

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

The integer row-pivoted result is the completed pivot-loop state.

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

The integer determinant entry point agrees with its packaged result.

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]