复sin²算法的双重重述：精确恒等式、下降性与有限性
A dual reformulation of the complex sin^2-algorithm: exact identities, descent, and finiteness
中文总结 AI 辅助
本文针对复三次域的sin²型算法，解决Karpenkov问题4的复符号情形，证明软回弹引理、有限性定理及高度下降定理，其核心在Lean 4中完成机器验证。
中文摘要 AI 辅助
我们发展了在 companion 论文中引入的复三次域确定性sin²型算法的结构理论，解决了Karpenkov问题4的复符号情形。该选择规则被证明恰好是共形模的最小化：即状态的横向复结构与圆之间距离的双曲余弦。所有控制量均为该域实嵌入的精确元素，且满足闭合的双重型恒等式；特别地，不会出现任何各向同性候选，且横向偏差格具有精确固定的协体积。我们证明了无条件软回弹引理（共形模在一步中最多可增长φ²=2.618…倍），在固定坐标判别式下，具有有界模和高度的状态的有限性定理（带有显式静态常数），以及在两个命名假设下的逐域周期性定理：(C_κ)，高相位下共形模的收缩，在此部分简化为对五参数紧空间上具有有理目标的固定有限极小极大；(B)，有界高度的 recurrence，我们随后仅在(C_κ)下证明该假设：高度下降定理表明高度永远不会超过max(H(s₀), C_H)，其中C_H为显式常数。逐域周期性的剩余方案简化为紧空间上的(R)和已证明的拉伸子情形。所有已证明的陈述和证书都是有限且精确的。本文的机器验证核心在Lean 4中完成，仅使用内核，基于标准公理：高度下降定理的解析核心、有限性鸽巢原理、双重与共形恒等式层，以及通过命名接口假设组合它们的抽象组装定理。
英文摘要
We develop the structure theory of the deterministic $\sin^2$-type algorithm for complex cubic fields introduced in the companion paper, addressing the complex-signature case of Karpenkov's Problem 4. The selection rule is shown to be, exactly, the minimization of a conformal module: the hyperbolic cosine of the distance between the transverse complex structure of the state and the round point. All governing quantities are exact elements of the real embedding of the field and satisfy closed dual-type identities; in particular no isotropic candidate ever arises, and the transverse deviation lattice has exactly pinned covolume. We prove an unconditional soft-rebound lemma (the module can grow by at most the factor $φ^2 = 2.618\ldots$ in one step), a finiteness theorem for states of bounded module and height at fixed coordinate discriminant, with explicit static constants, and a per-field periodicity theorem under two named hypotheses: $(C_κ)$, contraction of the module in the high phase, partially reduced here to a fixed finite minimax over a five-parameter compact with rational objective; and (B), recurrence of bounded height, which we then prove under $(C_κ)$ alone: a height-descent theorem shows the height can never exceed $\max(H(s_0), C_H)$ with an explicit constant. The remaining program for per-field periodicity is reduced to (R) on the compact and to the proved stretched subcases. All proved statements and certificates are finite and exact. A machine-checked core of the paper is sealed in Lean 4, kernel-only, under the standard axioms: the analytic core of the height-descent theorem, the finiteness pigeonhole, the dual and conformal identity layer, and an abstract assembly theorem composing them through named interface hypotheses.
