The Cardy entropy shift and the PDI

For a decay exponent γ ∈ (−1, 1), a scale θ > 0 and z > 0, the paper sets d_horizon = θ (1 − γ) √2 / (1 + γ) (from the Padé saturation), PDI = d_horizon / (z θ), and two forms of the Cardy entropy shift: ΔH₇ = log (z / √2) + 2 artanh γ (Phase 7) and ΔH₈ = log (z / 2) + 2 artanh γ (Phase 8).

Main results

• log_pdi_add_dHCardyPhase7 (D-DEEP-15): log PDI + ΔH₇ = 0 exactly.
• log_pdi_add_dHCardyPhase8: with the Phase 8 form the residual is −log 2 / 2.
• hasDerivAt_artanh: d/dx artanh x = 1 / (1 − x²) on (−1, 1).
• deriv_dHCardyPhase8 (D-DEEP-22): d ΔH₈ / dγ = 2 / (1 − γ²) on (−1, 1).

Related

Mathlib defines Real.artanh (with Real.artanh_eq_half_log) but, at the pinned commit, has no derivative lemma for it; hasDerivAt_artanh derives it from artanh_eq_half_log and HasDerivAt.log. Current Mathlib has none either (checked with Loogle and LeanSearch, October 2026). The same lemma, under the same name, is in TauCeti (TauCeti/Analysis/SpecialFunctions/Artanh.lean).

References

• C. Marín, Predicting How Transformers Attend (2026), Zenodo 19826343. Ported from Taf/Identities.lean of karlesmarin/lean-taf (Lean v4.30.0-rc2). The original refers to Real.arctanh, Real.arctanh_eq_log, Real.deriv_arctanh and Real.differentiableAt_arctanh, which do not exist in Mathlib (neither at the commit pinned by lean-taf nor here): the three statements above were not machine-checked there.

noncomputable def TransformerAttention.CardyPDI.dHCardyPhase7 (z γ : ℝ) : ℝ

Phase 7 Cardy entropy shift log (z / √2) + 2 artanh γ.

Equations

• TransformerAttention.CardyPDI.dHCardyPhase7 z γ = Real.log (z / √2) + 2 * Real.artanh γ

noncomputable def TransformerAttention.CardyPDI.dHCardyPhase8 (z γ : ℝ) : ℝ

Phase 8 Cardy entropy shift log (z / 2) + 2 artanh γ.

Equations

• TransformerAttention.CardyPDI.dHCardyPhase8 z γ = Real.log (z / 2) + 2 * Real.artanh γ

noncomputable def TransformerAttention.CardyPDI.dHorizon (θ γ : ℝ) : ℝ

d_horizon = θ (1 − γ) √2 / (1 + γ), the solution T of γ_Padé(θ, T) = γ.

Equations

• TransformerAttention.CardyPDI.dHorizon θ γ = θ * (1 - γ) * √2 / (1 + γ)

noncomputable def TransformerAttention.CardyPDI.pdi (θ z γ : ℝ) : ℝ

PDI = d_horizon / T_eval with T_eval = z θ.

Equations

• TransformerAttention.CardyPDI.pdi θ z γ = TransformerAttention.CardyPDI.dHorizon θ γ / (z * θ)

theorem TransformerAttention.CardyPDI.log_pdi_add_dHCardyPhase7 (θ z γ : ℝ) (hθ : θ > 0) (hz : z > 0) (hγ_lo : 0 < 1 - γ) (hγ_hi : 0 < 1 + γ) : Real.log (pdi θ z γ) + dHCardyPhase7 z γ = 0

D-DEEP-15: log PDI + ΔH₇ = 0.

theorem TransformerAttention.CardyPDI.hasDerivAt_artanh {x : ℝ} (hlo : -1 < x) (hhi : x < 1) : HasDerivAt Real.artanh (1 / (1 - x ^ 2)) x

d/dx artanh x = 1 / (1 − x²) for x ∈ (−1, 1).

theorem TransformerAttention.CardyPDI.deriv_dHCardyPhase8 (z γ : ℝ) (hγ_lo : -1 < γ) (hγ_hi : γ < 1) : deriv (fun (γ' : ℝ) => dHCardyPhase8 z γ') γ = 2 / (1 - γ ^ 2)

D-DEEP-22: d ΔH₈ / dγ = 2 / (1 − γ²) for γ ∈ (−1, 1).

theorem TransformerAttention.CardyPDI.log_pdi_add_dHCardyPhase8 (θ z γ : ℝ) (hθ : θ > 0) (hz : z > 0) (hγ_lo : 0 < 1 - γ) (hγ_hi : 0 < 1 + γ) : Real.log (pdi θ z γ) + dHCardyPhase8 z γ = -Real.log 2 / 2

With the Phase 8 form, log PDI + ΔH₈ = −log 2 / 2.