Critical exponents of the attention decay (Phase A)

For the decay exponent γ ≠ 1 (Phase A is 0 < γ < 1) the paper sets ν = 1 / (1 − γ), β = γ − 1, η = γ − 1 (corrected from η = 2γ), α = 2 − 1 / (1 − γ), χ = 1 / (1 − γ) and γ_χ = 1 / (1 − γ) + 2 (1 − γ) (Rushbrooke definition).

Main results

• two_mul_ηc_sq_add_ηc_mul_γχ_add_one (D-SAGE-1): 2 η² + η γ_χ + 1 = 0.
• βc_mul_χ (D-SAGE-2, anti-Ising): β χ = −1; αC_add_χ (D-SAGE-4): α + χ = 2; αC_add_γχ (D-SAGE-5); βc_mul_γχ (D-SAGE-6); νc_mul_βc: ν β = −1.
• rushbrooke, josephson: the scaling relations with d = 1 hold identically.
• fisher_residual, fisher_residual_eq_zero_iff: γ_χ − (2 − η) ν = γ (2γ − 3) / (1 − γ), which vanishes iff γ ∈ {0, 3/2}.
• eta_two_gamma_residual, eta_two_gamma_residual_pos: with the old η = 2γ, D-SAGE-1 has residual (−4γ³ + 5γ + 1) / (1 − γ), positive on all of Phase A.
• two_mul_sqrt_two_le_γχ (AM-GM bound): 2 √2 ≤ γ_χ for γ < 1.
• Other closed forms: nu_imprint_mul_two_pi, central_charge_mul_two_pi, nu_mul_one_sub, levy_index, two_s_sub_deff, sqrt_three_div_six_eq_one_div_sqrt_twelve (RoPE β = 1/√12).

Related

The AM-GM step is Mathlib's two_mul_le_add_of_sq_le_mul (two_mul_sqrt_mul_le_add restates it for √(a b) in one line). nu_imprint_mul_two_pi, central_charge_mul_two_pi and nu_mul_one_sub are instances of div_mul_cancel₀ and one_div_mul_cancel.

References

• C. Marín, Predicting How Transformers Attend (2026), Zenodo 19826343. Ported from Taf/Identities.lean, Taf/AmGmPade.lean, Taf/RGFlow.lean and Taf/ScalingLawIdentities.lean of karlesmarin/lean-taf (Lean v4.30.0-rc2).

noncomputable def TransformerAttention.CriticalExponents.νc (γ : ℝ) : ℝ

ν = 1 / (1 − γ) (correlation-length exponent, Phase A).

Equations

• TransformerAttention.CriticalExponents.νc γ = 1 / (1 - γ)

def TransformerAttention.CriticalExponents.βc (γ : ℝ) : ℝ

β = γ − 1 (order-parameter exponent).

Equations

• TransformerAttention.CriticalExponents.βc γ = γ - 1

def TransformerAttention.CriticalExponents.ηc (γ : ℝ) : ℝ

η = γ − 1 (anomalous dimension; corrected from 2γ).

Equations

• TransformerAttention.CriticalExponents.ηc γ = γ - 1

noncomputable def TransformerAttention.CriticalExponents.αC (γ : ℝ) : ℝ

α = 2 − 1 / (1 − γ) (heat-capacity exponent, Phase A).

Equations

• TransformerAttention.CriticalExponents.αC γ = 2 - 1 / (1 - γ)

noncomputable def TransformerAttention.CriticalExponents.γχ (γ : ℝ) : ℝ

γ_χ = 1 / (1 − γ) + 2 (1 − γ) (susceptibility exponent, Rushbrooke definition).

Equations

• TransformerAttention.CriticalExponents.γχ γ = 1 / (1 - γ) + 2 * (1 - γ)

noncomputable def TransformerAttention.CriticalExponents.χ (γ : ℝ) : ℝ

χ = 1 / (1 − γ) (susceptibility scaling, Phase A).

Equations

• TransformerAttention.CriticalExponents.χ γ = 1 / (1 - γ)

Identities

theorem TransformerAttention.CriticalExponents.two_mul_ηc_sq_add_ηc_mul_γχ_add_one (γ : ℝ) (h : γ ≠ 1) : 2 * ηc γ ^ 2 + ηc γ * γχ γ + 1 = 0

D-SAGE-1: 2 η² + η γ_χ + 1 = 0.

theorem TransformerAttention.CriticalExponents.βc_mul_χ (γ : ℝ) (h : γ ≠ 1) : βc γ * χ γ = -1

D-SAGE-2 (anti-Ising): β χ = −1.

theorem TransformerAttention.CriticalExponents.αC_add_χ (γ : ℝ) (h : γ ≠ 1) : αC γ + χ γ = 2

D-SAGE-4: α + χ = 2.

theorem TransformerAttention.CriticalExponents.αC_add_γχ (γ : ℝ) (h : γ ≠ 1) : αC γ + γχ γ = 2 * (2 - γ)

D-SAGE-5: α + γ_χ = 2 (2 − γ).

theorem TransformerAttention.CriticalExponents.βc_mul_γχ (γ : ℝ) (h : γ ≠ 1) : βc γ * γχ γ = -2 * γ ^ 2 + 4 * γ - 3

D-SAGE-6: β γ_χ = −2γ² + 4γ − 3.

theorem TransformerAttention.CriticalExponents.rushbrooke (γ : ℝ) (h : γ ≠ 1) : 2 * βc γ + γχ γ - νc γ * 1 = 0

Rushbrooke with d = 1: 2β + γ_χ − ν = 0.

theorem TransformerAttention.CriticalExponents.josephson (γ : ℝ) (h : γ ≠ 1) : 2 - αC γ - νc γ * 1 = 0

Josephson with d = 1: 2 − α − ν = 0.

theorem TransformerAttention.CriticalExponents.fisher_residual (γ : ℝ) (h : γ ≠ 1) : γχ γ - (2 - ηc γ) * νc γ = γ * (2 * γ - 3) / (1 - γ)

Fisher residual: γ_χ − (2 − η) ν = γ (2γ − 3) / (1 − γ).

theorem TransformerAttention.CriticalExponents.fisher_residual_eq_zero_iff (γ : ℝ) (h : γ ≠ 1) : γχ γ - (2 - ηc γ) * νc γ = 0 ↔ γ = 0 ∨ γ = 3 / 2

The Fisher residual vanishes iff γ = 0 or γ = 3/2.

theorem TransformerAttention.CriticalExponents.eta_two_gamma_residual (γ : ℝ) (h : γ ≠ 1) : 2 * (2 * γ) ^ 2 + 2 * γ * γχ γ + 1 = (-4 * γ ^ 3 + 5 * γ + 1) / (1 - γ)

With the old η = 2γ, D-SAGE-1 has residual (−4γ³ + 5γ + 1) / (1 − γ).

theorem TransformerAttention.CriticalExponents.eta_two_gamma_residual_pos (γ : ℝ) (hγ_lo : 0 < γ) (hγ_hi : γ < 1) : 2 * (2 * γ) ^ 2 + 2 * γ * γχ γ + 1 > 0

η = 2γ fails D-SAGE-1 everywhere in Phase A: the residual is positive on (0, 1).

theorem TransformerAttention.CriticalExponents.βc_mul_χ_add_one (γ : ℝ) (h : γ ≠ 1) : βc γ * χ γ + 1 = 0

β χ + 1 = 0: D-SAGE-2 rearranged.

theorem TransformerAttention.CriticalExponents.νc_mul_βc (γ : ℝ) (h : γ ≠ 1) : νc γ * βc γ = -1

ν β = −1.

AM-GM bound on γ_χ

theorem TransformerAttention.CriticalExponents.two_mul_sqrt_mul_le_add {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 2 * √(a * b) ≤ a + b

AM-GM for two variables, 2 √(a b) ≤ a + b: Mathlib's two_mul_le_add_of_sq_le_mul.

theorem TransformerAttention.CriticalExponents.two_mul_sqrt_two_le_γχ (γ : ℝ) (hγ : γ < 1) : 2 * √2 ≤ 1 / (1 - γ) + 2 * (1 - γ)

γ_χ = 1 / (1 − γ) + 2 (1 − γ) ≥ 2 √2 for γ < 1 (the product of the two terms is 2).

Other closed forms

theorem TransformerAttention.CriticalExponents.nu_imprint_mul_two_pi (π_val : ℝ) (hπ : π_val > 0) : -1 / (2 * π_val) * (2 * π_val) = -1

ν_imprint · 2π = −1 with ν_imprint = −1 / (2π): an instance of div_mul_cancel₀.

theorem TransformerAttention.CriticalExponents.central_charge_mul_two_pi (π_val : ℝ) (hπ : π_val > 0) : 3 * (1 / (2 * π_val)) * (2 * π_val) = 3

D-SAGE-7: c · |ν_imprint| · 2π = 3 with c = 3.

theorem TransformerAttention.CriticalExponents.nu_mul_one_sub (γ : ℝ) (h : 1 - γ ≠ 0) : 1 / (1 - γ) * (1 - γ) = 1

CFT₂: ν (1 − γ) = 1 for ν = 1 / (1 − γ): an instance of one_div_mul_cancel.

theorem TransformerAttention.CriticalExponents.levy_index (γ : ℝ) : 2 * ((γ - 1) / 2) = γ - 1

Lévy / fractional-Laplacian index: with s = (γ − 1)/2, 2s = γ − 1.

theorem TransformerAttention.CriticalExponents.two_s_sub_deff (γ : ℝ) (hγ : γ ≠ 0) : (γ ^ 2 - γ - 1) / γ + γ = (2 * γ + 1) * (γ - 1) / γ

(γ² − γ − 1)/γ + γ = (2γ + 1)(γ − 1)/γ, so 2s − d_eff vanishes iff γ ∈ {1, −1/2}.

theorem TransformerAttention.CriticalExponents.sqrt_three_div_six_eq_one_div_sqrt_twelve : √3 / 6 = 1 / √12

RoPE coefficient: √3 / 6 = 1 / √12 (σ of the uniform law on [−1, 0]).