A dual reformulation of the complex sin^2-algorithm: exact identities, descent, and finiteness
Ludovic Tagnon
math.NT
Aug 25, 2026 · v1
TL;DR
A kernel-only Lean 4 core seals the height-descent analytic core, finiteness pigeonhole, dual/conformal identity layer, and an abstract assembly theorem.
Abstract
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 $\varphi^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.
Problem
Karpenkov's Problem 4 asks to extend the sin^2-algorithm and prove eventual periodicity for cubic fields of complex signature (one real, one complex pair of embeddings). A companion paper gave a deterministic algorithm but no proof mechanism for periodicity.
Approach
The selection rule is reformulated as minimization of a conformal module m equal to the hyperbolic cosine of a distance to a round point, with exact closed dual-type identities in the real embedding of the field. A soft-rebound lemma, combinatorial descent, and finiteness theorem yield conditional per-field periodicity under named hypotheses (C_kappa) and (B). A machine-checked core is formalized in Lean 4, kernel-only (no native_decide, no sorry, standard axioms), covering the height-descent analytic core, finiteness pigeonhole, dual/conformal identity layer, and an abstract assembly theorem composing them via named interface hypotheses.
Results
An unconditional bound shows the module grows by at most phi^2=2.618 per step, and a height-descent theorem bounds height by max(H(s_0),C_H). Finiteness of states of bounded module/height at fixed discriminant is proved with explicit constants. The remaining program reduces to a finite minimax certificate (R) on a five-parameter compact.