35.4.1. Integer least squares🔗

For the row basis (2,0), (1,2) and target (1,1), minimize ‖z₀(2,0)+z₁(1,2)−(1,1)‖² over integer coefficients. Babai nearest-plane rounding supplies a finite initial bound, but its squared distance is two. Exact closest-vector search finds (1,2), at squared distance one.

closest returns every minimizer, sorted by ambient coordinates. Each record also contains coefficients in the original input basis and its exact rational squared distance. The companion's closest_spec proves the global minimum and completeness of this list, without a prepared-data witness supplied by the caller.

35.4.2. The hexagonal lattice in three dimensions🔗

The rows (1,−1,0), (0,1,−1) generate the integer lattice A₂ in the plane x+y+z=0. Its six shortest nonzero vectors have squared norm two. The closed ball of that squared radius also contains zero.

realLattice is an integer submodule of Euclidean space. Its real span is used only as the ambient space for packing. Taking rational or real linear combinations instead would introduce arbitrarily short nonzero vectors. For any shortest answer with squared norm s, packing_radius proves that open balls centred at lattice points are disjoint within that span exactly when their radius is at most sqrt(s)/2. The theorem kissing_number identifies the number of contacting spheres with the complete shortest-vector list length. Both signs are included. Rank zero returns none from shortest.

35.4.3. Rectangular bases and resource limits🔗

Targets may lie outside the row span. Exact Gram–Schmidt preparation retains the target's orthogonal residual; its squared norm is included in every bound. Negative squared radii give empty balls, and zero radii retain exact matches. ofMatrix? rejects dependent rows before a search starts.

enumerateWith, closestWith and shortestWith accept independent limits on visited nodes, retained answers and allocated certificate nodes. Limits are shared across the optimization and tie passes. A complete result proves exhaustion; an incomplete result contains checked points, a checked incumbent for optimization, and pending suffixes or coefficient streams. An incomplete incumbent carries no global optimality claim. The unlimited forms have no resource-related failure branch.

35.4.4. The Mathlib correspondence🔗

The companion proves validity of preparation, exhaustive traversal, coefficient uniqueness and global minima for the executable definitions. closest_real_spec and shortest_real_spec express the same complete lists in real Euclidean space. checkEnumeration_sound applies even to certificates received from an untrusted producer; the native acceptance theorems prove that completed native runs always pass replay.

35.4.5. Preparation, preprocessing and certificates🔗

prepare computes exact data once. retarget reuses the basis orthogonalization for another target. lllPreprocess uses Hex's existing optional LLL provider policy and checks both integer row transformations. Calling the resulting BasisChange methods searches the reduced basis while returning original-basis coefficients. Pending work remains expressed in the working basis.

Certificates contain that working basis, both transforms, rational Gram–Schmidt identities, an exhaustive coefficient tree, and sorted original points. Replay independently recomputes each interval, checks every child label and reconstructs every leaf. An optimum certificate adds an attained candidate and checks that its complete closed ball contains no eligible improvement. Soundness applies to arbitrary accepted certificates.

encodeCertificate and decodeCertificate use the versioned hex-lattice-enum-1 text format. DecodeLimits bounds bytes, dimensions, numeric token sizes, tree nodes and points before allocation. Decoding returns untrusted data: call checkEnumeration, checkClosest or checkShortest afterward. All of these operations are in the Mathlib-free library.

Literal certificates can also be replayed by Lean's kernel. For example, the two closest integers to one half are zero and one: