Padé approximants of e^{−z} in the attention-decay model

[1/1] and [2/2] Padé approximants of e^{−z}: P₁₁(z) = (1 − z/2) / (1 + z/2) and P₂₂(z) = (1 − z/2 + z²/12) / (1 + z/2 + z²/12). In the paper γ_Padé = P₁₁(z) with z = T √2 / θ.

Main results

• pade22_sub_pade11 (G-15): P₂₂ − P₁₁ = 2 z³ / ((z + 2)(z² + 6z + 12)), also in the cleared form pade22_sub_pade11'.
• pade_difference_at_zero, pade_saturation_leading_coefficient: the difference vanishes at 0 with leading coefficient 2 / 24 = 1/12 of z³.
• one_sub_pade11: 1 − (2 − z)/(2 + z) = 2z / (2 + z).
• pade11_z_substitution: γ_Padé = (2θ − T√2) / (2θ + T√2).
• theta_eff_pade: T √2 / (1 − γ_Padé) = θ + T / √2.

References

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

noncomputable def TransformerAttention.Pade.pade11 (z : ℝ) : ℝ

The [1/1] Padé approximant of e^{−z}.

Equations

• TransformerAttention.Pade.pade11 z = (1 - z / 2) / (1 + z / 2)

noncomputable def TransformerAttention.Pade.pade22 (z : ℝ) : ℝ

The [2/2] Padé approximant of e^{−z}.

Equations

• TransformerAttention.Pade.pade22 z = (1 - z / 2 + z ^ 2 / 12) / (1 + z / 2 + z ^ 2 / 12)

theorem TransformerAttention.Pade.pade22_sub_pade11' (z : ℝ) (h1 : z + 2 ≠ 0) (h2 : z ^ 2 + 6 * z + 12 ≠ 0) : (12 - 6 * z + z ^ 2) / (12 + 6 * z + z ^ 2) - (2 - z) / (2 + z) = 2 * z ^ 3 / ((z + 2) * (z ^ 2 + 6 * z + 12))

G-15, cleared form: (12 − 6z + z²)/(12 + 6z + z²) − (2 − z)/(2 + z) = 2 z³ / ((z + 2)(z² + 6z + 12)).

theorem TransformerAttention.Pade.pade22_sub_pade11 (z : ℝ) (h11 : 1 + z / 2 ≠ 0) (h22 : 1 + z / 2 + z ^ 2 / 12 ≠ 0) : pade22 z - pade11 z = 2 * z ^ 3 / ((z + 2) * (z ^ 2 + 6 * z + 12))

P₂₂ − P₁₁ = 2 z³ / ((z + 2)(z² + 6z + 12)).

theorem TransformerAttention.Pade.pade_difference_at_zero : have f := fun (z : ℝ) => 2 * z ^ 3 / ((z + 2) * (z ^ 2 + 6 * z + 12)); f 0 = 0

The difference 2 z³ / ((z + 2)(z² + 6z + 12)) vanishes at z = 0.

theorem TransformerAttention.Pade.pade_saturation_leading_coefficient : 2 / ((0 + 2) * (0 ^ 2 + 6 * 0 + 12)) = 1 / 12

Leading coefficient of z³ in the difference: 2 / ((0 + 2)(0 + 0 + 12)) = 1/12.

theorem TransformerAttention.Pade.one_sub_pade11 (z : ℝ) (h : 2 + z ≠ 0) : 1 - (2 - z) / (2 + z) = 2 * z / (2 + z)

1 − (2 − z)/(2 + z) = 2z / (2 + z).

theorem TransformerAttention.Pade.pade11_z_substitution (θ T : ℝ) (hθ : θ ≠ 0) (hsum_θ : 2 * θ + T * √2 ≠ 0) : (2 - T * √2 / θ) / (2 + T * √2 / θ) = (2 * θ - T * √2) / (2 * θ + T * √2)

With z = T √2 / θ: (2 − z)/(2 + z) = (2θ − T√2) / (2θ + T√2).

theorem TransformerAttention.Pade.theta_eff_pade (θ T : ℝ) (hθ : θ ≠ 0) (hT : T ≠ 0) (hsum : 2 * θ + T * √2 ≠ 0) : T * √2 / (1 - (2 - T * √2 / θ) / (2 + T * √2 / θ)) = θ + T / √2

θ_eff: with z = T √2 / θ, T √2 / (1 − (2 − z)/(2 + z)) = θ + T / √2.