# Verification report

The written argument proves the stated weighted quadratic cube Gibbs theorem
for all nonnegative weights and all a>=0. The bound is uniform over starting
points, including boundary points. Combining it with the credited prior
Wasserstein lower bound proves the fixed-graph asymptotic order at TV
tolerance 1/4. This is an originating-researcher self-audit, not independent
peer review or formal verification.

The audit checked the compact-support transport maps, preservation of the
complementary marginal, entropy sign, exact coordinate curvatures, scan-word
density marginalization, the unconditioned singular branch, zero-parameter
case, recurrence denominators, Pinsker constant, contraction-coefficient
amplification and the lower-bound parameter conversion. The mathematical
proof is in main.tex and main.pdf.

The portable standard-library checker runs 19,274 finite exact rational or
combinatorial conditions in both normal and optimized Python modes, with
identical results. These include quadratic identities, potential inequalities,
reciprocal inequalities, density-bound constants and coverage enumeration.
Its deliberately incorrect curvature and coverage alternatives are rejected.
The supporting checks are not a numerical proof of the analytic transport
or entropy arguments. Recurrence tests use exact rational values with
periodic downward rounding to limit denominator size; the general recurrence
is proved symbolically in the text.

An initial checker error mishandled the zero interpolation parameter by
dividing an inequality and substituting zero. It was corrected by testing
the undivided inequality. This did not alter the proof.

Both the desktop LaTeX compiler and the exported PDF build succeeded. All
five final pages were visually inspected for equations, footnote, references,
clipping and spacing. The initial layout's isolated bibliography entry was
removed by compacting the bibliography; the final build has no unresolved
LaTeX diagnostics.

The essential entropy method is due to Ascolani, Lavenant and Zanella. The
square result and the higher-dimensional Wasserstein lower bound are due
to Gerencser and to Gerencser--Ottolini, respectively. The bounded literature
search does not certify novelty. No arbitrary-Metropolis, optimal graph-
dependence or growing-dimension theorem is asserted, and the original
proposal-ambiguous AIM record is not counted as unconditionally closed.