hex

23.4. Structural theorems🔗

HexBareiss proves the structural facts about the elimination: that the packaged record is the pivot loop's final state packaged as determinant data, and that the public Hex.Matrix.bareiss value agrees with the determinant encoded by Hex.Matrix.bareissData. It does not prove that the Bareiss determinant equals the Leibniz Hex.Matrix.det. That identification is in HexBareissMathlib. Within HexBareiss itself the agreement is checked at build time by value-level conformance fixtures: a fixed bank of matrices on which Hex.Matrix.bareiss M = Hex.Matrix.det M is verified.

🔗theorem
Hex.Matrix.bareissData_eq_finish_pivotLoop {n : ℕ}
  (M : Hex.Matrix ℤ n n) :
  M.bareissData =
    Hex.Matrix.finish (Hex.Matrix.pivotLoop n M.noPivotInitialState)
Hex.Matrix.bareissData_eq_finish_pivotLoop
  {n : ℕ} (M : Hex.Matrix ℤ n n) :
  M.bareissData =
    Hex.Matrix.finish
      (Hex.Matrix.pivotLoop n
        M.noPivotInitialState)

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

🔗theorem
Hex.Matrix.bareiss_eq_bareissData_det {n : ℕ} (M : Hex.Matrix ℤ n n) :
  M.bareiss = M.bareissData.det
Hex.Matrix.bareiss_eq_bareissData_det
  {n : ℕ} (M : Hex.Matrix ℤ n n) :
  M.bareiss = M.bareissData.det

The integer determinant entry point agrees with its packaged result.