Integer row-lattice membership and independence for hex-lll, with the row-operation lemmas showing that an adjacent swap or a size-reduction row combination preserves the generated lattice.

def Hex.Matrix.memLattice {n m : Nat} (b : Matrix Int n m) (v : Vector Int m) : Prop

v lies in the integer lattice generated by the rows of b.

Equations

• b.memLattice v = ∃ (c : Vector Int n), Hex.Matrix.vecMul c b = v

theorem Hex.Internal.vecMul_mul {n' n m : Nat} (U : Matrix Int n' n) (B : Matrix Int n m) (c : Vector Int n') : Matrix.vecMul (U.transpose * c) B = Matrix.vecMul c (U * B)

Row combinations transport across an explicit integer row transform.

theorem Hex.Internal.memLattice_of_mul_eq {n m n' : Nat} {B : Matrix Int n m} {B' : Matrix Int n' m} {U : Matrix Int n' n} {v : Vector Int m} (h : U * B = B') : B'.memLattice v → B.memLattice v

If every row of B' is an integer row combination of rows of B, then membership in the lattice generated by B' implies membership for B.

theorem Hex.Internal.memLattice_iff_of_mul_eq {n m : Nat} {B B' : Matrix Int n m} {U V : Matrix Int n n} (hU : U * B = B') (hV : V * B' = B) (v : Vector Int m) : B.memLattice v ↔ B'.memLattice v

Two explicit integer row transforms in opposite directions prove equality of the generated lattices.

def Hex.Matrix.independent {n m : Nat} (b : Matrix Int n m) : Prop

The rows of b are linearly independent, witnessed by positivity of each executable leading Gram determinant.

Equations

• b.independent = Hex.GramSchmidt.Int.independent b

theorem Hex.Internal.memLattice_of_rowSwap_memLattice {n m : Nat} (b : Matrix Int n m) (i j : Fin n) (v : Vector Int m) : (b.rowSwap i j).memLattice v → b.memLattice v

memLattice_of_rowSwap_memLattice states that any vector in the lattice generated by rowSwap b i j also lies in the lattice generated by b.

theorem Hex.Internal.rowSwap_memLattice_iff {n m : Nat} (b : Matrix Int n m) (i j : Fin n) (v : Vector Int m) : (b.rowSwap i j).memLattice v ↔ b.memLattice v

rowSwap_memLattice_iff states that swapping rows i and j of b preserves lattice membership in both directions.

theorem Hex.Internal.memLattice_of_rowAdd_memLattice {n m : Nat} (b : Matrix Int n m) (src dst : Fin n) (c : Int) (v : Vector Int m) : (b.rowAdd src dst c).memLattice v → b.memLattice v

memLattice_of_rowAdd_memLattice states that any vector in the lattice generated by rowAdd b src dst c also lies in the lattice generated by b.

theorem Hex.Internal.rowAdd_memLattice_iff {n m : Nat} (b : Matrix Int n m) {src dst : Fin n} (hne : src ≠ dst) (c : Int) (v : Vector Int m) : (b.rowAdd src dst c).memLattice v ↔ b.memLattice v

rowAdd_memLattice_iff states that adding c times row src to a distinct row dst of b preserves lattice membership in both directions.