The renormalization-group flow of the decay exponent

The paper's β-function is β(γ) = −(1 − γ²)/2. Its formula tables also state the potential V(γ) = γ − γ³/3 with β = −V'; the two are inconsistent by a factor 2.

Main results

• logistic_beta: with x = (1 − γ)/2, x (1 − x) = (1 − γ²)/4 (logistic ODE ↔ β).
• deriv_V, neg_deriv_V_ne_beta: for V(γ) = γ − γ³/3, V' = 1 − γ², and −V'(γ) ≠ β(γ) for γ ∉ {−1, 1} (the factor-2 finding).
• deriv_V_correct, neg_deriv_V_correct: the corrected potential γ/2 − γ³/6 has −V' = −(1 − γ²)/2 = β.
• trajectory_sign_inversion: negating a trajectory flips the sign of the velocity.
• rg_flow_tanh: γ(t) = tanh (t/2 + c) solves γ' = (1 − γ²)/2.

Related

Mathlib has Real.hasDerivAt_sinh, Real.hasDerivAt_cosh and Real.tanh_eq_sinh_div_cosh; at the pinned commit it has no derivative lemma for Real.tanh, so rg_flow_tanh uses the quotient rule. Current Mathlib has none either (checked with Loogle and LeanSearch, October 2026); physlib has one, prepared for Mathlib, in Physlib/Mathematics/ForMathlib/Trigonometry/Tanh.lean.

References

• C. Marín, Predicting How Transformers Attend (2026), §19, §23 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.RGFlow.logistic_beta (γ : ℝ) : (1 - γ) / 2 * (1 - (1 - γ) / 2) = (1 - γ ^ 2) / 4

Logistic ↔ β: with x = (1 − γ)/2, x (1 − x) = (1 − γ²)/4.

theorem TransformerAttention.RGFlow.deriv_V (γ : ℝ) : deriv (fun (x : ℝ) => x - x ^ 3 / 3) γ = 1 - γ ^ 2

V(γ) = γ − γ³/3 has V'(γ) = 1 − γ².

theorem TransformerAttention.RGFlow.neg_deriv_V_ne_beta (γ : ℝ) (hne1 : γ ≠ 1) (hne2 : γ ≠ -1) : -deriv (fun (x : ℝ) => x - x ^ 3 / 3) γ ≠ -(1 - γ ^ 2) / 2

The factor-2 finding: −V'(γ) ≠ β(γ) = −(1 − γ²)/2 unless γ = ±1.

theorem TransformerAttention.RGFlow.deriv_V_correct (γ : ℝ) : deriv (fun (x : ℝ) => x / 2 - x ^ 3 / 6) γ = (1 - γ ^ 2) / 2

The corrected potential V(γ) = γ/2 − γ³/6 has V'(γ) = (1 − γ²)/2.

theorem TransformerAttention.RGFlow.neg_deriv_V_correct (γ : ℝ) : -deriv (fun (x : ℝ) => x / 2 - x ^ 3 / 6) γ = -(1 - γ ^ 2) / 2

−V'_correct(γ) = −(1 − γ²)/2 = β(γ).

theorem TransformerAttention.RGFlow.trajectory_sign_inversion (γ : ℝ) : -((1 - γ ^ 2) / 2) = -(1 - (-γ) ^ 2) / 2

Negating the trajectory inverts the sign of the velocity: −((1 − γ²)/2) = −(1 − (−γ)²)/2.

theorem TransformerAttention.RGFlow.rg_flow_tanh (c t : ℝ) : HasDerivAt (fun (s : ℝ) => Real.tanh (s / 2 + c)) ((1 - Real.tanh (t / 2 + c) ^ 2) / 2) t

γ(t) = tanh (t/2 + c) solves the flow γ'(t) = (1 − γ²)/2.