A Machine-Checked Backbone for the Thermodynamic Attention Framework: Lean/Mathlib Identities, Zero Sorries, and the Errata the Prover Caught

Companion formalization paper to the “Predicting How Transformers Attend” series (Marín 2026), Parts I–III. The Thermodynamic Attention Framework (TAF) rests on a dense web of closed-form algebraic identities — a Möbius transform relating the attention-decay exponent γ to the RoPE configuration, a renormalisation-group β-function, a Hagedorn heat-capacity CV, critical-exponent tautologies, and a Cayley fixed point. Dense formula tables are exactly where sign and factor errors hide. We mechanise this backbone in Lean 4 / Mathlib: 52 theorems, zero sorrys, each statement pinned to the paper section it supports. Formalization is used here not as decoration but as an adversarial audit — and it earned its keep: it caught three factor/sign errors in the published formula tables (the V/β potential, off by a factor of 2; the CV coefficient at the Hagedorn point, ¼ → 1/12, a factor of 3; and the critical-exponent identity η = 2γ, residual non-zero throughout Phase A), and it distinguished a genuine prediction from a tautology by proving that the “information horizon” dhorizon = T is an identity of the Padé formula, not an empirical coincidence. It also yields two positive results: the γ–Möbius collapse γ = (1−u)/(1+u) with u = T/(θ√2) (the √2 is load-bearing), and an arithmetic–geometric-mean bound γχ ≥ 2√2. All errata were incorporated into the corrected Parts I–II; this paper is the honest-revision ledger, machine-checked line by line. Repository: github.com/karlesmarin/lean-taf (Lean toolchain leanprover/lean4:v4.30.0-rc2; Mathlib pinned; lake build re-verifies the whole library). English and Spanish editions included. Prepared with the assistance of an AI system (Claude, Anthropic); the mathematics and all claims are the author's responsibility.