def HexMatrixTheory.decodeScalar (d : ℕ) (z : ℤ) : ℚ

Decode a scalar; used only in the soundness layer.

Equations

• HexMatrixTheory.decodeScalar d z = ↑z / ↑d

theorem HexMatrixTheory.decodeScalar_zero (d : ℕ) : decodeScalar d 0 = 0

def HexMatrixTheory.decodeList (s : Hex.Matrix.Lists.Scaled) : List ℚ

Decode a common-denominator vector.

Equations

• HexMatrixTheory.decodeList s = List.map (HexMatrixTheory.decodeScalar s.denom) s.nums

def HexMatrixTheory.decodeRows (s : Hex.Matrix.Lists.ScaledRows) : List (List ℚ)

Decode a common-denominator matrix.

Equations

• HexMatrixTheory.decodeRows s = List.map (fun (row : List ℤ) => List.map (HexMatrixTheory.decodeScalar s.denom) row) s.nums

theorem HexMatrixTheory.decodeScalar_eq (q : ℚ) (z : ℤ) (d : ℕ) (hd : 0 < d) (h : q.num * ↑d = z * ↑q.den) : q = decodeScalar d z

theorem HexMatrixTheory.scaleRow_sound (d : ℕ) (q : List ℚ) (z : List ℤ) (hd : 0 < d) (h : Hex.Matrix.Lists.scaleRow d q z = true) : q = List.map (decodeScalar d) z

theorem HexMatrixTheory.scaleRows_sound (d : ℕ) (q : List (List ℚ)) (z : List (List ℤ)) (hd : 0 < d) (h : Hex.Matrix.Lists.scaleRows d q z = true) : q = decodeRows { denom := d, nums := z }

theorem HexMatrixTheory.decodeList_getD (s : Hex.Matrix.Lists.Scaled) (i : ℕ) : (decodeList s).getD i 0 = decodeScalar s.denom (s.nums.getD i 0)

theorem HexMatrixTheory.decodeRows_getD (s : Hex.Matrix.Lists.ScaledRows) (i j : ℕ) : ((decodeRows s).getD i []).getD j 0 = decodeScalar s.denom ((s.nums.getD i []).getD j 0)

theorem HexMatrixTheory.encode_denom_pos (xs : List ℚ) : 0 < (Hex.Matrix.Lists.Scaled.encode xs).denom

The actual common-denominator producer always chooses a positive denominator, including for the empty list.

theorem HexMatrixTheory.encode_denom_dvd (xs : List ℚ) (q : ℚ) (hq : q ∈ xs) : q.den ∣ (Hex.Matrix.Lists.Scaled.encode xs).denom

Every entry denominator divides the denominator chosen by the producer.

theorem HexMatrixTheory.encode_scaleRow (xs : List ℚ) : Hex.Matrix.Lists.scaleRow (Hex.Matrix.Lists.Scaled.encode xs).denom xs (Hex.Matrix.Lists.Scaled.encode xs).nums = true

Clearing denominators in the shared producer passes the literal integer cross-product checker.

theorem HexMatrixTheory.decode_encode (xs : List ℚ) : decodeList (Hex.Matrix.Lists.Scaled.encode xs) = xs

Decoding the producer output recovers every rational entry in its original order.

theorem HexMatrixTheory.encodeRows_denom_pos (xs : List (List ℚ)) : 0 < (Hex.Matrix.Lists.ScaledRows.encode xs).denom

theorem HexMatrixTheory.encode_scaleRows (xs : List (List ℚ)) : Hex.Matrix.Lists.scaleRows (Hex.Matrix.Lists.ScaledRows.encode xs).denom xs (Hex.Matrix.Lists.ScaledRows.encode xs).nums = true

theorem HexMatrixTheory.decodeRows_encode (xs : List (List ℚ)) : decodeRows (Hex.Matrix.Lists.ScaledRows.encode xs) = xs

Matrix encoding preserves empty rows, dimensions and entry order.