The Cayley map γ(z) = (2 − z)/(2 + z) and its fixed point

The Padé decay exponent γ_Padé(z) = −(z − 2)/(z + 2) is a Cayley map. Its positive fixed point is z* = (√17 − 3)/2, with susceptibility χ = (5 + √17)/4 and Floquet multiplier μ = γ'(z*) = (√17 − 9)/8.

Main results

• cayley_fixed_point_iff: γ(z) = z ↔ z² + 3z − 2 = 0 (for z ≠ −2).
• cayley_root, cayley_root_pos: z* = (√17 − 3)/2 is a positive root of z² + 3z − 2.
• chi_root: χ = (5 + √17)/4 satisfies 2χ² − 5χ + 1 = 0.
• floquet_multiplier, cayley_floquet_form_equivalence: μ = (√17 − 9)/8, in the cleared form μ (2 + z*)² = −4 and in the table's form −4(√17 + 1)/(5√17 + 13).
• cayley_floquet_stable: |μ| < 1.
• cayley_at_zero, cayley_at_two: γ(0) = 1 (Hagedorn), γ(2) = 0.

References

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

theorem TransformerAttention.CayleyMap.cayley_fixed_point_iff (z : ℝ) (h : z + 2 ≠ 0) : -(z - 2) / (z + 2) = z ↔ z ^ 2 + 3 * z - 2 = 0

γ(z) = −(z − 2)/(z + 2) = z ↔ z² + 3z − 2 = 0.

theorem TransformerAttention.CayleyMap.cayley_root : ((√17 - 3) / 2) ^ 2 + 3 * ((√17 - 3) / 2) - 2 = 0

z* = (√17 − 3)/2 is a root of z² + 3z − 2.

theorem TransformerAttention.CayleyMap.chi_root : 2 * ((5 + √17) / 4) ^ 2 - 5 * ((5 + √17) / 4) + 1 = 0

χ = (5 + √17)/4 satisfies 2χ² − 5χ + 1 = 0.

theorem TransformerAttention.CayleyMap.cayley_root_pos : 0 < (√17 - 3) / 2

z* = (√17 − 3)/2 > 0: the physical root.

theorem TransformerAttention.CayleyMap.floquet_multiplier : (√17 - 9) / 8 * (2 + (√17 - 3) / 2) ^ 2 = -4

Floquet multiplier in cleared form: ((√17 − 9)/8) (2 + z*)² = −4, i.e. γ'(z*) = −4/(2 + z*)² = (√17 − 9)/8.

theorem TransformerAttention.CayleyMap.cayley_floquet_form_equivalence : -4 * (√17 + 1) / (5 * √17 + 13) = (√17 - 9) / 8

The table's form of the Floquet multiplier: −4(√17 + 1)/(5√17 + 13) = (√17 − 9)/8.

theorem TransformerAttention.CayleyMap.cayley_floquet_stable : |(√17 - 9) / 8| < 1

Stability of the fixed point: |(√17 − 9)/8| < 1.

theorem TransformerAttention.CayleyMap.cayley_at_zero : -(0 - 2) / (0 + 2) = 1

γ(0) = 1 (the Hagedorn point).

theorem TransformerAttention.CayleyMap.cayley_at_two : -(2 - 2) / (2 + 2) = 0

γ(2) = 0.