Following a mechanization in $\mathsf{Rocq}$, we prove that satisfiability of single Diophantine equations of total degree $\le 3$ over $\mathbb{N}$ (with a computably bounded number of variables depending on the instance) is $Σ^0_1$-complete, and hence undecidable, in the sense of Hilbert's Tenth Problem. The core construction is a uniform primitive recursive compiler mapping arithmetic sentence codes to finite structured cubic constraint systems, such that provability in $\mathrm{I}Δ_0 + \mathrm{B}Σ_1$ is equivalent to solvability of the emitted system. Conjunction is eliminated without squaring: all emitted constraints are merged into a single cubic Diophantine equation via a Fibonacci-banded two-channel equality that preserves the cubic bound without sum-of-squares blow-up. All syntactic and inference checks compile to quadratic constraints; the only cubic terms come from linear selector variables multiplying those quadratic obligations. The mechanized core is constructive and requires no classical axioms: uniform computability, checker-constraint equivalence, and the degree-$3$ bound are verified by structural induction. From this base, undecidability is obtained by a classical Diagonal Argument: any total correct decider for cubic satisfiability would compose with the compiler to decide arithmetic theoremhood, and a fixed-point construction yields an instance on which it fails. Consequently, cubic satisfiability is $Σ^0_1$-complete.

翻译：暂无翻译