The packed same-lattice certificate: decide M * A = C and hence sameLatticeCert over integer arithmetic by comparing rows packed as single big integers in balanced base 2 ^ K, never forming the matrix product.

def Hex.Internal.packDigits (P : Int) : List Int → Int

Horner evaluation of an integer digit list at base P.

Equations

• Hex.Internal.packDigits P [] = 0
• Hex.Internal.packDigits P (x_1 :: xs) = x_1 + P * Hex.Internal.packDigits P xs

def Hex.Internal.packRow {m : Nat} (K : Nat) (v : Vector Int m) : Int

Pack the entries of a row as one integer in balanced base 2^K.

Equations

• Hex.Internal.packRow K v = Hex.Internal.packDigits (2 ^ K) v.toList

def Hex.Internal.maxAbs {n m : Nat} (M : Matrix Int n m) : Nat

Maximum absolute value of the entries of an integer matrix.

Equations

• Hex.Internal.maxAbs M = List.foldl (fun (acc : Nat) (row : Vector Int m) => acc.max (List.foldl (fun (a : Nat) (x : Int) => a.max x.natAbs) 0 row.toList)) 0 M.rows.toList

def Hex.Internal.packWidth {n m : Nat} (M : Matrix Int n n) (A C : Matrix Int n m) : Nat

Digit width at which every entry of M * A and of C packs injectively: 2 · |entry| < 2^K for all entries, since each is bounded by n · maxAbs M · maxAbs A + maxAbs C.

Equations

• Hex.Internal.packWidth M A C = (n * Hex.Internal.maxAbs M * Hex.Internal.maxAbs A + Hex.Internal.maxAbs C).log2 + 2

def Hex.Internal.mulEqCert {n m : Nat} (M : Matrix Int n n) (A C : Matrix Int n m) : Bool

Packed product-equality certificate: decides M * A = C without forming the product. Each row of A and of C is packed into one integer in balanced base 2^K at the width packWidth M A C, and row i of the (unformed) product is compared via the single packed dot product Σ_l M[i][l] · packA[l]: n big-integer dot products in place of the n · m entry dot products of a materialized Matrix.mul.

When the entries are word-scale the multiplications are big-by-small and the same-lattice clause costs O(n²) big-by-small multiplications; on wide entries the packed dot products cost the same bit operations as the materialized product. Either way the single packed comparison decides exactly M * A = C (mulEqCert_iff).

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Internal.natAbs_le_maxAbs {n m : Nat} (M : Matrix Int n m) (i : Fin n) (j : Fin m) : M[i][j].natAbs ≤ maxAbs M

Every entry of an integer matrix is bounded by the maxAbs scan.

theorem Hex.Internal.packDigits_zipWith_muladd (P c : Int) (r s : List Int) (h : r.length = s.length) : packDigits P (List.zipWith (fun (a b : Int) => c * a + b) r s) = c * packDigits P r + packDigits P s

Packing is linear over a coefficient-times-row update.

theorem Hex.Internal.packRow_zipWith_muladd {m : Nat} (K : Nat) (c : Int) (r s : Vector Int m) : packRow K (Vector.zipWith (fun (a b : Int) => c * a + b) r s) = c * packRow K r + packRow K s

Row-level form of packDigits_zipWith_muladd.

theorem Hex.Internal.dotProduct_packRow {n m : Nat} (K : Nat) (M : Matrix Int n n) (A : Matrix Int n m) (i : Fin n) : (M.row i).dotProduct (Vector.ofFn fun (l : Fin n) => packRow K (A.row l)) = packRow K ((M * A).row i)

The packed dot product evaluates to the pack of the corresponding row of the (unformed) product M * A.

theorem Hex.Internal.packDigits_inj (K : Nat) {xs ys : List Int} (hlen : xs.length = ys.length) (hxs : ∀ (x : Int), x ∈ xs → 2 * x.natAbs < 2 ^ K) (hys : ∀ (y : Int), y ∈ ys → 2 * y.natAbs < 2 ^ K) (h : packDigits (2 ^ K) xs = packDigits (2 ^ K) ys) : xs = ys

Uniqueness of the balanced base-2^K representation: digit lists of equal length whose digits all satisfy 2 · |digit| < 2^K pack injectively.

theorem Hex.Internal.natAbs_dotProduct_le {k : Nat} (u v : Vector Int k) (Bu Bv : Nat) (hu : ∀ (l : Fin k), u[l].natAbs ≤ Bu) (hv : ∀ (l : Fin k), v[l].natAbs ≤ Bv) : (u.dotProduct v).natAbs ≤ k * (Bu * Bv)

Entrywise bound on an integer dot product.

theorem Hex.Internal.natAbs_mul_entry_le {n m : Nat} (M : Matrix Int n n) (A : Matrix Int n m) (i : Fin n) (j : Fin m) : (M * A)[i][j].natAbs ≤ n * (maxAbs M * maxAbs A)

Every entry of the product M * A is bounded by the maxAbs scans.

theorem Hex.Internal.mulEqCert_iff {n m : Nat} {M : Matrix Int n n} {A C : Matrix Int n m} : mulEqCert M A C = true ↔ M * A = C

The packed certificate decides product equality: sound (= true implies M * A = C, by balanced-digit uniqueness at width packWidth M A C) and complete (M * A = C implies = true, by congruence through dotProduct_packRow).

def Hex.Matrix.sameLatticeCert {n m : Nat} (B B' : Matrix Int n m) (U V : Matrix Int n n) : Bool

Executable same-lattice certificate: two integer transforms that multiply the bases into each other. Each product equality is verified by the packed certificate mulEqCert, so neither product matrix is ever formed.

Equations

• B.sameLatticeCert B' U V = (Hex.Internal.mulEqCert U B B' && Hex.Internal.mulEqCert V B' B)

theorem Hex.Matrix.sameLatticeCert_sound {n m : Nat} {B B' : Matrix Int n m} {U V : Matrix Int n n} : B.sameLatticeCert B' U V = true → ∀ (v : Vector Int m), B.memLattice v ↔ B'.memLattice v

Soundness of sameLatticeCert: accepted certificates prove identical integer row lattices.