We prove that $\mathrm{H}\mathbb{N}(3,n)=\mathrm{U}$ for some fixed $n$. The core result is a uniform primitive recursive compiler from sentence codes to finite cubic Diophantine systems over $\mathbb{N}$, such that arithmetic theoremhood is equivalent to cubic solvability on the compiler image. The translation is explicit: finite proof traces are arithmetized, local syntactic and inference checks are compiled to quadratic constraints, and one guard gadget $u = 1+v^2, u\cdot E = 0$ provides the unique degree escalation from $2$ to $3$ while preserving solvability. The construction is mechanized in $\textsf{Rocq}$ and certified in the Calculus of Inductive Constructions, including uniform computability, checker--constraint equivalence, and a global degree-$3$ bound for emitted systems. From this certified core, undecidability is obtained by a classical fixed-point Diagonal Argument: any total correct decider for cubic satisfiability computes a mirror cubic instance on which it fails. Consequently cubic satisfiability is $Σ^0_1$-complete, and in particular there is no total correct procedure deciding all degree-$3$ Diophantine instances.

翻译：我们证明对于某个固定的n，有$\mathrm{H}\mathbb{N}(3,n)=\mathrm{U}$。核心结果是一个从句子编码到$\mathbb{N}$上有限三次丢番图系统的统一原始递归编译器，使得算术定理性等价于编译器映像上的三次可解性。该转换是显式的：有限证明轨迹被算术化，局部句法和推理检查被编译为二次约束，而一个守卫装置$u = 1+v^2, u\cdot E = 0$在保持可解性的同时，提供了从2次到3次的唯一次数提升。该构造在$\textsf{Rocq}$中实现机械化，并在归纳构造演算中完成形式化验证，包括统一可计算性、检查器-约束等价性，以及生成系统的全局3次界限。基于此经过验证的核心结果，通过经典的固定点对角论证获得不可判定性：任何用于三次可满足性的完全正确判定器，都会在某个镜像三次实例上失效。因此，三次可满足性是Σ⁰₁完备的，特别地，不存在能够判定所有3次丢番图实例的完全正确过程。