hex

6.7. Worked example🔗

The block reduces the rank-2 lattice with basis rows (1, 12) and (0, 1). The skewed first row is far from orthogonal. Reduction returns (0, 1), (1, 0) (the two unit vectors), which generate the same lattice and are as short as possible.

open Hex Hex.Matrix Hex.Internal

namespace HexLLLChapterExample

-- B = [[1, 12], [0, 1]]: a skewed basis.
private def B : Matrix Int 2 2 :=
  Matrix.ofFn fun i j =>
    match i.val, j.val with
    | 0, 0 => 1
    | 0, 1 => 12
    | 1, 1 => 1
    | _, _ => 0

-- R = [[0, 1], [1, 0]]: the reduced basis.
private def R : Matrix Int 2 2 :=
  Matrix.ofFn fun i j =>
    match i.val, j.val with
    | 0, 1 => 1
    | 1, 0 => 1
    | _, _ => 0

-- U, V: the integer transforms witnessing that B
-- and R generate the same lattice (U·B = R,
-- V·R = B).
private def U : Matrix Int 2 2 :=
  Matrix.ofFn fun i j =>
    match i.val, j.val with
    | 0, 1 => 1
    | 1, 0 => 1
    | 1, 1 => -12
    | _, _ => 0

private def V : Matrix Int 2 2 :=
  Matrix.ofFn fun i j =>
    match i.val, j.val with
    | 0, 0 => 12
    | 0, 1 => 1
    | 1, 0 => 1
    | _, _ => 0

-- The δ = 3/4 preconditions for the exact reducer.
private theorem hlo : (1 / 4 : Rat) < 3 / 4 := by⊢ 1 / 4 < 3 / 4 grindAll goals completed! 🐙
private theorem hhi : (3 / 4 : Rat) ≤ 1 := by⊢ 3 / 4 ≤ 1 grindAll goals completed! 🐙

-- Reduction turns the skewed basis into R.
#guard lllNative B (3 / 4) hlo hhi (by⊢ 1 ≤ 2 decideAll goals completed! 🐙) = R

-- Its first row is a shortest lattice vector.
#guard ((lllNative B (3 / 4) hlo hhi (by⊢ 1 ≤ 2 decideAll goals completed! 🐙)).row
          ⟨0, by⊢ 0 < 2 decideAll goals completed! 🐙⟩).toArray = #[0, 1]

-- The verified checker rejects the input basis
-- (not size-reduced) and accepts the output.
#guard lllReducedInt B (3 / 4) (11 / 20) = false
#guard lllReducedInt R (3 / 4) (11 / 20) = true

-- U, V certify that B and R share a lattice, and
-- certCheck combines that with reducedness of R.
#guard Matrix.sameLatticeCert B R U V = true
#guard certCheck B R U V (3 / 4) (11 / 20) = true

end HexLLLChapterExample