Our contribution is a bounded cubic compilation theorem. For each fixed resource parameter $k$, syntactic proof checking at resource level $k$ is faithfully represented by a finite bounded-domain system of cubic polynomial equations. Every emitted equation has degree at most 3. Degree-3 terms arise only when a linear selector variable activates a quadratic verification obligation. Earlier versions of this manuscript claimed a reduction from unbounded theoremhood to satisfiability of a fixed bounded-domain cubic polynomial instance. That claim is withdrawn. The error and its source are identified precisely. The bounded construction, the degree bookkeeping, and the Zeckendorf-based carryless encoding stand independently of the withdrawn claim. The note closes by identifying the uniformization gap that separates a family of decidable bounded slices from a single many-one reduction target, and records why closing that gap would require a compression principle not supplied here.

翻译：我们的贡献是一个有界三次编译定理。对于每个固定的资源参数$k$，在资源级别$k$上的语法证明验证被忠实地表示为一个有限有界域的三次多项式方程组。每个生成的方程次数至多为3。三次项仅当线性选择变量激活二次验证义务时出现。本手稿的早期版本声称从无界定理证明性归约到固定有界域三次多项式实例的可满足性。该声称已被撤回。该错误及其来源已被精确识别。有界构造、次数簿记以及基于Zeckendorf的无进位编码独立于被撤回的声称而成立。本文最后指出了分离可判定有界切片族与单一多一归约目标的均匀化缺口，并记录了为何弥合该缺口需要一个未在此处提供的压缩原理。