hex

4.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 : Nat}
  (M : Hex.Matrix Int n n) :
  M.bareissData =
    Hex.Matrix.finish (Hex.Matrix.pivotLoop n M.noPivotInitialState)
Hex.Matrix.bareissData_eq_finish_pivotLoop
  {n : Nat} (M : Hex.Matrix Int n n) :
  M.bareissData =
    Hex.Matrix.finish
      (Hex.Matrix.pivotLoop 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.

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

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