4.3. Entry points🔗

The public entry points run the row-pivoting elimination. Hex.Matrix.bareissData returns the full record. Hex.Matrix.bareiss returns just the integer determinant. The no-pivot variants skip the pivot search, for inputs whose leading pivots are already nonzero.

def

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

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

def

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

Determinant computed by the row-pivoted Bareiss algorithm.

def

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

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

def

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

Determinant computed by the no-pivot Bareiss recurrence.

The division at each step is Int.divExact (a GMP-backed mpz_divexact), which is always exact and carries its divisibility proof. The bordered minors are the intermediate determinants the correctness proof uses as its elimination invariant.

def

Hex.Matrix.borderedMinor.{u_1} {R : Type u_1} {n : Nat}
  (M : Hex.Matrix R n n) (k : Nat) (hk : k < n) (i j : Fin n) :
  Hex.Matrix R (k + 1) (k + 1)
Hex.Matrix.borderedMinor.{u_1}
  {R : Type u_1} {n : Nat}
  (M : Hex.Matrix R n n) (k : Nat)
  (hk : k < n) (i j : Fin n) :
  Hex.Matrix R (k + 1) (k + 1)

Bordered Bareiss minor with the first k rows/columns and one extra border row i and column j. For Bareiss applications i and j are in the trailing part, but the constructor is total and leaves that side condition to the invariant using it.