Sharp integer full-slack inequality and its conditional coordinate bound

This is the authors' abstract. We don't add key points for this paper.

This note proves that Erebos Labs' full-slack inequality has sharp additive constant 1 on the integer points of its unchanged feasible algebraic domain, improving the real-domain constant 17/16. The argument retains the predecessor's dispersion term and uses the rational lattice of the remaining expression; two feasible integer tuples attain equality. No geometric realization is required for this local algebraic theorem. For the pinned conditional graph-profile application, the same matrix certificate gives M <= 49 rather than 50, with mode removal sufficient at even D >= 588. The separate higher-defect estimate keeps the complete sufficient threshold at even D >= 600. All inherited analytic assumptions remain; this is not a new unconditional Sidorenko counterexample or a reduction of the complete dimension threshold. The self-contained packet includes the written proof, unchanged public source files at b38300a50094dc550394e29765cd6005a4d68d2c, exact polynomial and matrix checks, 358488 finite boundary profiles, 11 unit/integration tests, ten rejecting controls, source hashes, and fresh staged verification logs. The finite grid is supporting evidence, not the proof of the unbounded statement. This is not proof-assistant verification. Earlier separate AI review is documented; human peer review and an exhaustive novelty assessment are not claimed. Alexander Richard Towell is the contributor, with substantial OpenAI Codex assistance. Erebos Labs' real theorem, reductions, dispersion identity and certificates, predecessor contributions, and the underlying OpenAI manuscript are credited with licenses preserved. First public disclosure was upstream PR1 on 20 October 2026; the PR remains open without review at archival preparation. Archival publication and repository acceptance are distinct.