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.

翻译：通过在$\mathsf{Rocq}$中的机械化实现，我们证明了在$\mathbb{N}$上（变量数量依实例计算有界）总次数$\le 3$的单个丢番图方程的可满足性是$Σ^0_1$完全的，因而在希尔伯特第十问题的意义上是不可判定的。核心构造是一个将算术语句编码映射到有限结构化三次约束系统的统一原始递归编译器，使得在$\mathrm{I}Δ_0 + \mathrm{B}Σ_1$中的可证性等价于所生成系统的可解性。合取无需平方化即可消除：所有生成的约束通过一个斐波那契带双通道等式合并为单个三次丢番图方程，该等式在保持三次界的同时避免了平方和膨胀。所有句法和推理检查均编译为二次约束；仅有的三次项来自线性选择变量与这些二次义务的乘积。机械化核心是构造性的且无需经典公理：统一可计算性、检查器-约束等价性以及次数-$3$界均通过结构归纳法验证。基于此，不可判定性通过经典对角线论证获得：任何用于三次可满足性的完全正确判定器将与编译器复合以判定算术定理性，而一个不动点构造将产生一个使其失败的实例。因此，三次可满足性是$Σ^0_1$完全的。