一步复制递归器的取向边界：机械化的不可行性、逃逸与认证

我们形式化化化第一阶步骤复制递归器的取向边界，聚焦于右复制递归器模式（RDRS），即 $\mathrm{recur}(b,s,\mathrm{succ}(n))\to\mathrm{wrap}(s,\mathrm{recur}(b,s,n))$。在Lean 4中，否定侧排除了十二类直接测量类（两类无条件类、六类标量增长类、四类跟踪向量/序对类），包含极冷/极热矩阵延续、面向WPO的多项式分支后果，以及KBO阻挡。四个元定理组织了该堆栈：投影主导性、标量投影提升、混合矩阵标量化以及符号比较器障碍。该表面覆盖72个模式层面的复制-步骤不可行性，以及80个具体系统全局步骤定理，包含一条76行的RDRS方法宇宙收尾，以及一个证明每种有效载荷擦除语义直接测量均被支配的语义帽子。成功侧包含透明性必然性见证、依赖-序对投影逃逸、在冻结基底失效下的广义多项式障碍、可计算见证提取器、系数表决策程序，以及互递归/同步SCC障碍。KO7见证微积分具有两层链。其受保护片段强归约、根-收敛且可归约，具有单指数情境导数界限，以及在 $\omega^{\omega}$ 以下的精确 $\omega^{\omega}$ 序数校准。完整的未受保护系统通过非线性多项式见证和专用MPO实现根终止，上下文封闭的强归约通过每个构造函数位置提升。经检查的TPDB导出与Lean侧的FAST证书认证将开发与TTT2/CeTA相连。据我们了解，这是首个在固定终止系统上进行的机械化对象级障碍定理，无需化简或不可判定性论证即可完成。