17.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
namespace HexLLLChapterExample
-- B = [[1, 12], [0, 1]]: a skewed basis.
private def B : Hex.Matrix Int 2 2 := #m[1, 12; 0, 1]
-- R = [[0, 1], [1, 0]]: the reduced basis.
private def R : Hex.Matrix Int 2 2 := #m[0, 1; 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 : Hex.Matrix Int 2 2 := #m[0, 1; 1, -12]
private def V : Hex.Matrix Int 2 2 := #m[12, 1; 1, 0]
-- The δ = 3/4 preconditions for the exact reducer.
private theorem hlo : (1 / 4 : Rat) < 3 / 4 := ⊢ 1 / 4 < 3 / 4 All goals completed! 🐙
private theorem hhi : (3 / 4 : Rat) ≤ 1 := ⊢ 3 / 4 ≤ 1 All goals completed! 🐙
-- Reduction turns the skewed basis into R.
#guard lllNative B (3 / 4) hlo hhi (⊢ 1 ≤ 2 All goals completed! 🐙) = R
-- Its first row is a shortest lattice vector.
#guard (lllNative B (3 / 4) hlo hhi (⊢ 1 ≤ 2 All goals completed! 🐙)).row
⟨0, ⊢ 0 < 2 All goals completed! 🐙⟩ = #v[0, 1]
-- The verified checker rejects the input basis
-- (not size-reduced) and accepts the output.
#guard lllReduced B (3 / 4) (11 / 20) = false
#guard lllReduced 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
17.7.1. Recovering a minimal polynomial from a decimal
A short vector of a well-chosen lattice recovers an integer relation among
real numbers. The classic application is guessing the minimal polynomial
of an algebraic number from a numerical approximation. Take the decimal
α = 1.220744…, and suppose all we know is that it is a root of some monic
integer polynomial of degree at most four, but not which one.
Scale the powers 1, α, α², α³, α⁴ by C = 10⁶ and round to integers. The
lattice has one row per power: an identity block that remembers the
coefficient, and a last column holding the scaled power. A combination
Σ aᵢ · rowᵢ has last coordinate ≈ C · Σ aᵢ αⁱ, which is tiny exactly
when Σ aᵢ αⁱ ≈ 0, that is, when the aᵢ are the coefficients of a
polynomial that α nearly satisfies. LLL finds the shortest such vector.
open Hex Hex.Matrix
namespace HexLLLMinPoly
-- One row per power of α: eᵢ in the first five columns,
-- round(10⁶ · αⁱ) in the last, for i = 0..4.
private def L : Hex.Matrix Int 5 6 :=
#m[1, 0, 0, 0, 0, 1000000;
0, 1, 0, 0, 0, 1220744;
0, 0, 1, 0, 0, 1490216;
0, 0, 0, 1, 0, 1819173;
0, 0, 0, 0, 1, 2220744]
private theorem hlo : (1 / 4 : Rat) < 3 / 4 := ⊢ 1 / 4 < 3 / 4 All goals completed! 🐙
private theorem hhi : (3 / 4 : Rat) ≤ 1 := ⊢ 3 / 4 ≤ 1 All goals completed! 🐙
-- The shortest reduced row reads off the coefficients
-- (a₀, a₁, a₂, a₃, a₄) = (-1, -1, 0, 0, 1) with a zero
-- last coordinate: the relation -1 - α + α⁴ = 0, i.e.
-- the minimal polynomial x⁴ - x - 1.
#guard (lllNative L (3 / 4) hlo hhi (⊢ 1 ≤ 5 All goals completed! 🐙)).row
⟨0, ⊢ 0 < 5 All goals completed! 🐙⟩ = #v[-1, -1, 0, 0, 1, 0]
end HexLLLMinPoly
The last coordinate comes out exactly zero, not merely small: because
α⁴ = α + 1 holds exactly and C is an integer, the rounded scaled powers
satisfy round(C·α⁴) − round(C·α) − round(C) = 0 on the nose. So the
recovered vector is a genuine lattice element, and its first five entries
(-1, -1, 0, 0, 1) are the coefficients of x⁴ − x − 1.