Abstract
Let \( C=\{m^3:m\in Z\} \). We prove that there is a set \( A\subseteq Z \) for which the addition map \( A\times C\to Z \) is a bijection. If \( k \) is a fixed noncube and \( [E_k(N)=\{n\in[N,2N)\cap Z:n^3-k\in C-C\}, \) we prove the quantitative estimate \( \#E_k(N)\ll_{k,\delta} N^{18/19+\delta} \qquad(\delta>0). \) The small-gap contribution is handled by a square sieve on the progression polynomial attached to the gap \( a=y-x \); all local branches, including sieve primes dividing \( a \) and the zero values of the polynomial, are treated explicitly. For larger gaps, a theorem of Heath–Brown on fixed levels of diagonal ternary forms gives the required power saving after a direct height calculation and an exclusion of every special solution. Density zero then gives simultaneous avoidance for every finite collection of noncubes, and a two-sided greedy construction produces \( A \). Independently of this source-level proof, a complete Lean 4 development checks the exact theorem and a self-contained determinant–conic–binary-sextic route to the coarser bound \( O_k(N^{99/100}) \). The formal sources, dependency lock, and axiom audit are supplied as a separate companion archive; they are not used as a substitute for the mathematical arguments in the paper.