2025/09/09 by Lauri Alha, Alha, Lauri
Computer Science · Mathematics · #Advanced Algebra and Logic #Advanced Mathematical Identities #Classical Analysis and ODEs (math.CA) #FOS: Mathematics #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2509.07598
openalex publication_date 2025/09/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
A machine-checked, sorry-free development in Lean 4 over Mathlib (about 1500 lines) that fills a gap in Mathlib — the dilogarithm Li2, which the library cites but does not define — and follows it into a quantum-mechanics problem. To the best of the author's knowledge, the first formalization in any proof assistant of: the real dilogarithm with Euler's reflection identity, Landen's transformation and the duplication formula; the golden-ratio ladder Li2(1/φ2) = π2/15 − ln2φ (derived from a 3×3 linear system, no five-term relation) and the Lee–Yang effective central charge ceff = 2/5 (the simplest thermodynamic-Bethe-ansatz dilogarithm identity); the Clausen function Cl2 and Catalan's constant G = Cl2(π/2); the Fejér–Jackson inequality; the bound Cl2(θ) ≥ sin(θ)/2 by an asymptotics-free Abel summation; and the Margolus–Levitin and (an L1 form of the) Mandelstam–Tamm quantum speed limits. These assemble into the title theorem: the weight-2 zeta state (populations proportional to 1/n2 on equally spaced energy levels) has infinite mean energy and infinite energy variance — so both textbook speed limits say nothing — yet never reaches a state orthogonal to itself, because its autocorrelation is (6/π2)·Li2(e−iθ) and the dilogarithm has no zero on the unit circle. A clock with an unbounded energy budget that never ticks. Every identity is classical (Euler, Landen, Clausen, Fejér, Jackson, Mandelstam–Tamm, Margolus–Levitin); the contribution is the machine-checked development and its assembly. Every named theorem depends only on the three standard axioms (propext, Classical.choice, Quot.sound). Formalized with AI assistance (Claude, Anthropic); the mathematics and all claims are the author's responsibility.