theorem HexMatrixMathlib.isDomain_of_quot {R : Type u} [CommRing R] [DecidableEq R] (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (h1 : 1 ≠ 0) : IsDomain R

An exact quotient makes a nontrivial commutative ring an integral domain.

theorem HexMatrixMathlib.borderedMinor_corner_eq_principalSubmatrix {n : ℕ} {R : Type u} (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 {R : Type u} [CommRing R] {n : ℕ} (M : Hex.Matrix R 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 {R : Type u} [CommRing R] {n : ℕ} (source : Hex.Matrix R n n) (state : Hex.Matrix.BareissState R 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_initialWith {n : ℕ} {R : Type u} [CommRing R] (M : Hex.Matrix R n n) (h1 : 1 ≠ 0) : 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.bareissNoPivotInvariant_initial {n : ℕ} (M : Hex.Matrix ℤ n n) : BareissNoPivotInvariant M M.noPivotInitialState

Integer compatibility form of bareissNoPivotInvariant_initialWith.

theorem HexMatrixMathlib.bareissPivotInvariant_regular_no_swap {n : ℕ} {R : Type u} [CommRing R] (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R n n) (state : Hex.Matrix.BareissState R 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 := Hex.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 }

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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} (state : Hex.Matrix.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) (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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} (source : Hex.Matrix R n n) (state : Hex.Matrix.BareissState R 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 : ℕ} {R : Type u} [CommRing R] (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R 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 : ℕ} {R : Type u} [CommRing R] (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R 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 quot hquot. 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} (state : Hex.Matrix.BareissState R 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} (source : Hex.Matrix R n n) (state : Hex.Matrix.BareissState R 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 : ℕ} {R : Type u} [CommRing R] (data : Hex.Matrix.BareissData R 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 {R : Type u} [CommRing R] {n : ℕ} (state : Hex.Matrix.BareissState R n) : R

Sign contributed by the row swaps recorded in a Bareiss state.

Equations

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

def HexMatrixMathlib.BareissPivotInvariant {R : Type u} [CommRing R] {n : ℕ} (source : Hex.Matrix R n n) (state : Hex.Matrix.BareissState R 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 : ℕ} {R : Type u} [CommRing R] (M : Hex.Matrix R n n) (h1 : 1 ≠ 0) : 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 : ℕ} {R : Type u} [CommRing R] (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R n n) (state : Hex.Matrix.BareissState R 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 := Hex.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 }

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

theorem HexMatrixMathlib.bareissPivotInvariant_regular_swap_step {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R n n) (state : Hex.Matrix.BareissState R 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 := Hex.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 }

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

theorem HexMatrixMathlib.pivotLoop_invariant_of_singularStep_eq_none {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R n n) (fuel : ℕ) (state : Hex.Matrix.BareissState R n) (hinv : BareissPivotInvariant source state) (hregular : (Hex.Matrix.pivotLoopWith quot fuel state).singularStep = none) : BareissPivotInvariant source (Hex.Matrix.pivotLoopWith quot 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R n n) (fuel : ℕ) (state : Hex.Matrix.BareissState R n) (hinv : BareissNoPivotInvariant source state) (hpivots : ∀ (k : Fin n), state.step ≤ ↑k → (source.principalSubmatrix (↑k + 1) ⋯).det ≠ 0) : BareissNoPivotInvariant source (Hex.Matrix.noPivotLoopWith quot 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (h1 : 1 ≠ 0) (M : Hex.Matrix R n n) (h : NonzeroBareissPivots M) : BareissNoPivotInvariant M (Hex.Matrix.noPivotLoopWith quot 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (h1 : 1 ≠ 0) (M : Hex.Matrix R n n) (h : NonzeroBareissPivots M) : (Hex.Matrix.noPivotLoopWith quot 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (h1 : 1 ≠ 0) (M : Hex.Matrix R n n) (h : NonzeroBareissPivots M) : (Hex.Matrix.bareissNoPivotDataWith quot M).singularStep = none

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

theorem HexMatrixMathlib.noPivotLoopWith_invariant_of_singularStep_eq_none {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R n n) (fuel : ℕ) (state : Hex.Matrix.BareissState R n) (hinv : BareissNoPivotInvariant source state) (hregular : (Hex.Matrix.noPivotLoopWith quot fuel state).singularStep = none) : BareissNoPivotInvariant source (Hex.Matrix.noPivotLoopWith quot 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.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)

Integer compatibility form of noPivotLoopWith_invariant_of_singularStep_eq_none.

theorem HexMatrixMathlib.bareissNoPivotWith_eq_det {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (M : Hex.Matrix R n n) (h : NonzeroBareissPivots M) : Hex.Matrix.bareissNoPivotWith quot M = (matrixEquiv M).det

A no-pivot Bareiss computation over any commutative ring with an exact quotient agrees with Mathlib's determinant when its leading pivots are nonzero. No separate nontriviality or domain assumption is required.

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

Integer compatibility specialization of bareissNoPivotWith_eq_det.

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

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 {R : Type u} [CommRing R] {n : ℕ} (source : Hex.Matrix R n n) (k : ℕ) (hk : k < n) : Fin n → R

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 : ℕ} {R : Type u} [CommRing R] (source : Hex.Matrix R n n) (k : ℕ) (hk : k < n) (c : Fin n) (hc : k < ↑c) : failedBareissColumn source k hk c = 0

theorem HexMatrixMathlib.failedBareissColumn_at_pivot {n : ℕ} {R : Type u} [CommRing R] (source : Hex.Matrix R n n) (k : ℕ) (hk : k < n) : failedBareissColumn source k hk ⟨k, hk⟩ = (source.principalSubmatrix k ⋯).det

theorem HexMatrixMathlib.failed_bareiss_column_dependence {n : ℕ} {R : Type u} [CommRing R] (source : Hex.Matrix R 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 → R), α ⟨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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (h1 : 1 ≠ 0) (source : Hex.Matrix R 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R n n) (state : Hex.Matrix.BareissState R 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R n n) (fuel : ℕ) (state : Hex.Matrix.BareissState R n) (hinv : BareissPivotInvariant source state) (hsing : (Hex.Matrix.pivotLoopWith quot 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (source : Hex.Matrix R n n) (fuel : ℕ) (state : Hex.Matrix.BareissState R n) (hinv : BareissPivotInvariant source state) {k : ℕ} (hsing : (Hex.Matrix.pivotLoopWith quot 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (h1 : 1 ≠ 0) (M : Hex.Matrix R n n) (hsing : (Hex.Matrix.pivotLoopWith quot 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 {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (h1 : 1 ≠ 0) (M : Hex.Matrix R n n) (hsing : (Hex.Matrix.bareissDataWith quot M).singularStep ≠ none) : M.det = 0

If the row-pivoted Bareiss result records a singular step, the Mathlib determinant of the input is zero.

theorem HexMatrixMathlib.bareissWith_eq_mathlib_det {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (M : Hex.Matrix R n n) : Hex.Matrix.bareissWith quot M = (matrixEquiv M).det

Row-pivoted Bareiss over any commutative ring with an exact quotient agrees with Mathlib's determinant.

theorem HexMatrixMathlib.bareissWith_eq_det {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} (quot : R → R → R) (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (M : Hex.Matrix R n n) : Hex.Matrix.bareissWith quot M = M.det

Row-pivoted Bareiss over an exact-division commutative ring agrees with Hex's executable determinant.

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

Integer compatibility specialization of bareissWith_eq_mathlib_det.

theorem HexMatrixMathlib.noPivotLoop_full_eq_borderedMinor_det {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} {quot : R → R → R} (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a) (h1 : 1 ≠ 0) (M : Hex.Matrix R n n) (k : ℕ) (hk : k + 1 < n) (a c : Fin n) (hak : k + 1 ≤ ↑a) (hck : k + 1 ≤ ↑c) (h_no_sing : (Hex.Matrix.noPivotLoopWith quot (k + 1) M.noPivotInitialState).singularStep = none) : (Hex.Matrix.noPivotLoopWith quot (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 noPivotLoopWith_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).