The Pentagon, Machine-Checked: Abel's five-term relation for the dilogarithm in Lean 4

A machine-checked, sorry-free proof, in Lean 4 over Mathlib, of Abel's five-term relation for the dilogarithm. With L the Rogers L-function, for x,y in (0,1): L(x)+L(y) = L(xy) + L(x(1-y)/(1-xy)) + L(y(1-x)/(1-xy)). This single identity is the whole weight-2 theory in one line: by theorems of Wojtkowiak and de Jeu, every functional equation of the dilogarithm with rational arguments is a consequence of it; it is the defining relation of the Bloch group and the pentagon of cluster algebras and of the quantum dilogarithm. It is the sequel to The Clock That Never Ticks (doi:10.5281/zenodo.20675271), which built a dilogarithm in Lean from scratch and climbed the golden-ratio ladder without this relation, leaving it explicitly open; this paper closes that thread. The proof is the classical differentiation argument made fully rigorous (vanishing derivative → constant → boundary value). The mathematics is entirely classical (Spence, Abel, Rogers; Wojtkowiak's and de Jeu's universality); the contribution is the formalization — to the best of the author's knowledge the first machine-checked five-term relation, on the first machine-checked dilogarithm, in any proof assistant — together with three reusable building blocks. Every theorem depends only on the three standard axioms (propext, Classical.choice, Quot.sound). This deposit contains the paper in English (five-term-lean.pdf) and Spanish (five-term-lean-es.pdf). Lean sources: github.com/karlesmarin/godsil-gutman-lean, Dilog/FiveTerm.lean.