The heat-capacity coefficient at the Hagedorn point (erratum)

Theorem 5.2 of the paper states C_V(γ = 1, N) = (log N)²/4; the erratum corrects it to (log N)²/12 (a factor 3). This file checks the algebraic chain of both derivations of the corrected coefficient, with L = log N. The asymptotic statement (→ as N → ∞, which needs Euler–Maclaurin bounds for the harmonic sums) is not formalized. The integral ∫₁ᴺ log x / x dx = (log N)²/2 behind it is integral_log_div_self (Formalizations.Analysis.SpecialFunctions.Integrals.LogDivSelf).

Main results

• var_log_d_identity, cv_from_cumulant_at_hagedorn (cumulant route): L²/3 − (L/2)² = L²/12, and C_V = γ² Var(log d) = L²/12 at γ = 1.
• log_one_plus_x_coefficient_24, log_z_quadratic_coefficient, log_z_to_U_coefficient (Taylor route): 1/6 − 1/8 = 1/24, 2 · L²/24 = L²/12.
• deriv_U_corrected_at_one, cv_corrected_at_hagedorn: for U(γ) = L/2 + (1 − γ) L²/12, U'(1) = −L²/12 and C_V = −γ² U'(1) = L²/12.
• original_is_three_times_corrected, original_ne_corrected, cv_factor_three_decomposition: the published L²/4 is three times the corrected value and differs from it for L ≠ 0.

References

• C. Marín, Predicting How Transformers Attend (2026), §5.2, and its erratum (2026-05-02), Zenodo 19826343. Ported from Taf/ErratumCV.lean of karlesmarin/lean-taf (Lean v4.30.0-rc2).

Cumulant route

theorem TransformerAttention.HeatCapacity.var_log_d_identity (L : ℝ) : L ^ 2 / 3 - (L / 2) ^ 2 = L ^ 2 / 12

(log N)²/3 − ((log N)/2)² = (log N)²/12.

theorem TransformerAttention.HeatCapacity.cv_from_cumulant_at_hagedorn (L : ℝ) : 1 ^ 2 * (L ^ 2 / 3 - (L / 2) ^ 2) = L ^ 2 / 12

C_V(γ = 1) = γ² Var(log d) = (log N)²/12.

Taylor route

theorem TransformerAttention.HeatCapacity.log_one_plus_x_coefficient_24 : 1 / 6 - 1 / 8 = 1 / 24

1/6 − 1/8 = 1/24 (the log (1 + x) step).

theorem TransformerAttention.HeatCapacity.log_z_quadratic_coefficient (L : ℝ) : L ^ 2 / 6 - L ^ 2 / 8 = L ^ 2 / 24

L²/6 − L²/8 = L²/24.

theorem TransformerAttention.HeatCapacity.log_z_to_U_coefficient (L : ℝ) : 2 * (L ^ 2 / 24) = L ^ 2 / 12

2 · (L²/24) = L²/12 (derivative of the quadratic Taylor term).

noncomputable def TransformerAttention.HeatCapacity.U_corrected (L γ : ℝ) : ℝ

The corrected internal energy U(γ) = L/2 + (1 − γ) L²/12.

Equations

• TransformerAttention.HeatCapacity.U_corrected L γ = L / 2 + (1 - γ) * L ^ 2 / 12

theorem TransformerAttention.HeatCapacity.deriv_U_corrected_at_one (L : ℝ) : deriv (fun (γ : ℝ) => U_corrected L γ) 1 = -L ^ 2 / 12

Erratum eq. (5): dU/dγ at γ = 1 is −(log N)²/12.

theorem TransformerAttention.HeatCapacity.cv_corrected_at_hagedorn (L : ℝ) : -1 ^ 2 * deriv (fun (γ : ℝ) => U_corrected L γ) 1 = L ^ 2 / 12

Erratum eq. (6): C_V(γ = 1, N) = −γ² dU/dγ = (log N)²/12.

Original versus corrected

theorem TransformerAttention.HeatCapacity.original_is_three_times_corrected (L : ℝ) : L ^ 2 / 4 = 3 * (L ^ 2 / 12)

The published (log N)²/4 is exactly three times (log N)²/12.

theorem TransformerAttention.HeatCapacity.original_ne_corrected (L : ℝ) (hL : L ≠ 0) : L ^ 2 / 4 ≠ L ^ 2 / 12

The two coefficients differ unless L = 0.

theorem TransformerAttention.HeatCapacity.cv_factor_three_decomposition (L : ℝ) : L ^ 2 / 8 = 3 * (L ^ 2 / 24)

The residual of the wrong derivation: L²/8 = 3 · (L²/24).