The Padé attention-decay exponent as a Möbius transform

The Padé exponent γ_Padé(θ, T) = (2θ − T s) / (2θ + T s), with s = √2, is the Möbius (Cayley) transform (1 − u) / (1 + u) of the single reduced variable u = T / (θ s). The collapse uses s² = 2: for another constant the numerator and denominator do not factor. The constant s is kept abstract (0 < s, s ^ 2 = 2) and instantiated at √2 at the end.

Main results

• gammaPade_eq_mobius: γ_Padé = (1 − u) / (1 + u) (uses s² = 2).
• mobius_mobius: x ↦ (1 − x) / (1 + x) is an involution, (1 − γ) / (1 + γ) = u.
• dHorizon_eq: θ s (1 − γ) / (1 + γ) = T at γ = γ_Padé, so the information horizon d_horizon evaluated at the Padé exponent is the training length T.
• beta_mobius: −(1 − γ²) / 2 = −2u / (1 + u)² for γ = (1 − u) / (1 + u).
• gammaPade_sqrt_two_eq_mobius: the collapse at s = √2.

Related

The same exponent appears, as pade11 (T √2 / θ), in TransformerAttention.Pade (pade11_z_substitution). No Möbius form of it is in Mathlib at the pinned commit (existence check of 2026-10-19 against Mathlib, LeanSearch, the AFP and GitHub); the algebra is elementary.

References

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

noncomputable def TransformerAttention.GammaMobius.gammaPade (s θ T : ℝ) : ℝ

The Padé attention-decay exponent; s stands for √2.

Equations

• TransformerAttention.GammaMobius.gammaPade s θ T = (2 * θ - T * s) / (2 * θ + T * s)

noncomputable def TransformerAttention.GammaMobius.reducedVar (s θ T : ℝ) : ℝ

The reduced distance variable u = T / (θ s).

Equations

• TransformerAttention.GammaMobius.reducedVar s θ T = T / (θ * s)

theorem TransformerAttention.GammaMobius.gammaPade_eq_mobius {s θ T : ℝ} (hs2 : s ^ 2 = 2) (hs : 0 < s) (hθ : 0 < θ) (hT : 0 < T) : gammaPade s θ T = (1 - reducedVar s θ T) / (1 + reducedVar s θ T)

Möbius collapse. With u = T / (θ √2), the Padé exponent is (1 − u) / (1 + u). The hypothesis s ^ 2 = 2 is essential.

theorem TransformerAttention.GammaMobius.mobius_mobius {u : ℝ} (hu : 1 + u ≠ 0) : (1 - (1 - u) / (1 + u)) / (1 + (1 - u) / (1 + u)) = u

Inverse Möbius. x ↦ (1 − x) / (1 + x) is an involution: (1 − γ) / (1 + γ) = u when γ = (1 − u) / (1 + u).

theorem TransformerAttention.GammaMobius.dHorizon_eq {s θ T : ℝ} (hs2 : s ^ 2 = 2) (hs : 0 < s) (hθ : 0 < θ) (hT : 0 < T) : θ * s * ((1 - gammaPade s θ T) / (1 + gammaPade s θ T)) = T

The information horizon d_horizon = θ √2 (1 − γ) / (1 + γ) evaluated at γ = γ_Padé is exactly the training length T.

theorem TransformerAttention.GammaMobius.beta_mobius {u : ℝ} (hu : 1 + u ≠ 0) : -(1 - ((1 - u) / (1 + u)) ^ 2) / 2 = -2 * u / (1 + u) ^ 2

RG β-function in the reduced variable. −(1 − γ²) / 2 = −2u / (1 + u)² for γ = (1 − u) / (1 + u).

theorem TransformerAttention.GammaMobius.sq_sqrt_two_and_pos : √2 ^ 2 = 2 ∧ 0 < √2

√2 satisfies the two hypotheses on s.

theorem TransformerAttention.GammaMobius.gammaPade_sqrt_two_eq_mobius {θ T : ℝ} (hθ : 0 < θ) (hT : 0 < T) : gammaPade (√2) θ T = (1 - reducedVar (√2) θ T) / (1 + reducedVar (√2) θ T)

The Möbius collapse at s = √2.