# Verification report for Gaussian lattice entropy selection

The written argument proves the displayed lattice theorems, not the
all-configuration AIM question. The crucial uniformity step is linear
packing loss from positive eutaxy and perfection. Comparison with the
undeformed lattice bounds the full shape displacement by O(1/t).
A Gaussian-moment bound controls the entire nonminimal tail and its
first two derivatives uniformly on bounded rescaled shape sets.

The next correction uses exp(C/2) for the lattice and exp(C) for squared
lengths. Stationarity is on trace-zero matrices, making the weighted
covariance (m c_H/d)I. This yields the negative correction
-m c_H tr(B_H^2)/(2dt). Properness, Mahler compactness and the finite
Hermite classes precede minimization of the expansions. Ties are broken
by greatest squared drift only after minimizing the leading coefficient.
The reciprocal Gaussian parameter is pi^2/alpha. Both signs are included
in the shortest shell and energies use ordered pairs.

The C10 example has 160 shortest vectors, a rank-45 projector span and
an exact selected-minor determinant of 400000000000000000000.
Positive rational weights give covariance (960/13)P_W, and a rational
exponential bound gives coefficient at most 479621/3000 < 160.
The example is not claimed to be Hermite-optimal.

The standard-library checker independently enumerates the shell twice,
uses rational elimination and integer Bareiss elimination with three
modular cross-checks, and verifies every matrix entry in its projection
and covariance identities. Normal and optimized modes agree on 1510
checks. These are exact finite certificates, not formal verification of
the general analytic theorem.

The seven-page English manuscript compiled with the built-in LaTeX
compiler and Tectonic without remaining warnings. All seven final pages
were visually inspected, including equations, the author footnote,
the shell table and references. Package readiness additionally requires
a clean-directory source-ZIP build with identical page content streams
and portable reruns of both checker modes.

The originating researcher accepts the complete scoped theorem after
written self-audit. No outside reviewer or proof assistant has certified
it. The cited classical results and substantial earlier energy theory
remain attributed. The literature comparison is bounded and does not
certify absolute priority. AI assistance is disclosed in the manuscript.
