The Eventual Exact Value of g₅(n) in the Choi–Erdős–Szemerédi Pairwise-Sums Problem

This record contains a preliminary computer-assisted proof that g5(n) = 4 for every integer n >= 2^64, in the version of the Choi–Erdős–Szemerédi pairwise-sums problem where the five summands are distinct integers and may be non-positive. Different pairs may have the same sum. The result concerns the integer k = 5 case of Erdős problem #866, not the full problem for general k. The paper builds on the structural program proposed in Section 10 of John Erlbacher's Demonstrandum draft and supplies explicit mathematical arguments and a completed finite verification. The accompanying package includes the English PDF and TeX source, two enumeration implementations, all eighteen candidate lists, explicit refutation certificates for 12,089 candidates, a separate Python checker, and file-integrity manifests. The certificates contain 451,269 proof nodes. AI tools contributed substantially to proof development, code, manuscript preparation and subsequent checks; the paper gives the research provenance and AI disclosure. Human verification and a Lean 4 formalization remain in progress. No Lean formalization is included in this version. The manuscript has not undergone external peer review, and successful certificate checking does not by itself verify the complete mathematical reduction or enumeration completeness.