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.
CARLES MARÍN MUÑOZ (Fri,) studied this question.