4.2. The elimination record🔗

An elimination pass returns a small record: the terminal matrix, the number of row swaps performed during pivoting, and an optional record of the first step at which a zero pivot with no replacement row was found (the signal that the matrix is singular).

structure

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

Output of an executable Bareiss elimination pass.

Constructor

Hex.Matrix.BareissData.mk

Fields

matrix : Hex.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.

The sign contributed by the row swaps and the encoded determinant are read off that record. A recorded singular step encodes determinant zero. Otherwise the determinant is the last diagonal entry of the terminal matrix with the swap sign applied.

def

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

The determinant sign contributed by the recorded row swaps.

def

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

The determinant encoded by a Bareiss elimination result.