Motivation

Transformer sequence models modulate attention scores by a function of the relative position between a query and a key: the attention logit between token $m$ and token $n$ is scaled by a fixed profile $f(p_m - p_n)$. Realizing this modulation the naive way means evaluating $f$ once per pair $(m,n)$ and materializing an $L\times L$ adjustment over the whole sequence — quadratic in the sequence length $L$. Rotary Position Embedding (RoPE) Su et al. 2021 avoids this entirely: it rotates the query at position $p_m$ and the key at position $p_n$ independently, each by an angle depending only on its own position, so that the pairwise quantity $f(p_m-p_n)$ falls out of the dot product of the two separately rotated vectors — $f$ is never evaluated pairwise, and no $L\times L$ matrix is ever built. This is what lets RoPE stay a linear, per-token preprocessing step compatible with efficient (sub-quadratic) attention implementations, rather than an $O(L^2)$ modulation. The catch is that RoPE's specific log-linear frequency schedule bakes in one particular profile: a monotone, decaying $f$. That schedule is a poor fit whenever the correlation structure of the data is not monotonically decaying with distance — the leading example being periodicity: in sequential recommendation, interactions separated by exactly one day or one week are more correlated than interactions separated by, say, half a day, and a decaying profile cannot express that "attention comes back" at the period.

Chen, Ainslie, Choromanski et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling (arXiv:2607.26369), ask a more general question first: which attention-modulation profiles $f$ can be realized at all by this same per-token, pairwise-iteration-free rotation trick — rotate each token once, on its own, and let the pairwise profile emerge from the dot product — and by what rotation-frequency schedule? Their answer is a random-features construction — sample the rotation frequencies from the kernel's own Fourier transform, rather than fixing them log-linearly — that realizes any continuous, normalized, positive-definite profile in expectation, with a quantified concentration rate, all while keeping the exact same per-token rotate-then-dot-product computation RoPE already uses. ClockRoPE is the periodic instance of this general theory, later deployed in a production-scale generative-retrieval system.

Setting

Fix an embedding dimension $d = 2n$ and group a vector $v \in \mathbb{R}^d$ into $n$ consecutive feature pairs $v^{(j)} = (v_{2j}, v_{2j+1}) \in \mathbb{R}^2$ for $j = 0, \dots, n-1$. For an angle $\theta$, let

$$R(\theta) = \begin{pmatrix} \cos\theta & -\sin\theta \\ \sin\theta & \cos\theta \end{pmatrix}$$

be the $2\times 2$ (Givens) rotation matrix. A real kernel $f : \mathbb{R} \to \mathbb{R}$ is positive definite if for every finite family of points $x_1,\dots,x_N \in \mathbb{R}$ and complex coefficients $c_1,\dots,c_N$, $\sum_{i,j} \overline{c_i} c_j f(x_i - x_j)$ has nonnegative real part; it is normalized if $f(0) = 1$. When $f$ is also continuous and Lebesgue-integrable, its Fourier transform

$$\tau(\xi) = \int_{\mathbb{R}} f(x) e^{-i2\pi\xi x}\,dx$$

is (by Bochner's theorem) a genuine probability density on $\mathbb{R}$: this is the distribution the mission's rotation frequencies are sampled from.

Given a query $q_m \in \mathbb{R}^{2n}$ at position $p_m$, a key $k_n \in \mathbb{R}^{2n}$ at position $p_n$, and $n$ i.i.d. frequencies $\xi_0, \dots, \xi_{n-1} \sim \tau$, the Random Fourier Rotation (RFR) estimator is

$$\hat g(q_m, k_n, p_m, p_n) = \sum_{j=0}^{n-1} \big(R(2\pi\xi_j p_m)\, q_m^{(j)}\big)^\top \big(R(2\pi\xi_j p_n)\, k_n^{(j)}\big).$$

$\hat g$ is exactly the modulated attention logit computed by rotating query/key feature pairs with per-pair, sampled RoPE frequencies — the same operation standard RoPE performs, but with $\xi_j$ drawn from $\tau$ instead of fixed by a log-linear schedule.

Formalization targets

Goal — convergence of the RFR estimator (Proposition 3.2)

$$P\!\left(\left|\tfrac1n \hat g(q_m,k_n,p_m,p_n) - \tfrac1n\, q_m^\top k_n f(p_m-p_n)\right| \ge \epsilon\right) \le 2\exp\!\left(-\frac{\epsilon^2(2n)^2}{8\sum_{j=0}^{n-1}\big(\lVert q_m^{(j)}\rVert\, \lVert k_n^{(j)}\rVert\big)^2}\right)$$

for every $\epsilon > 0$. This is the mission's central target: it upgrades the mean identity below into a quantitative, non-asymptotic guarantee that the sampled estimator is close to the target profile with high probability, at a rate that is exponential in the embedding dimension $d = 2n$.

Milestone — unbiasedness of the RFR estimator (Proposition 3.1)

$$\mathbb{E}_{\xi_0,\dots,\xi_{n-1}\sim\tau}\big[\hat g(q_m,k_n,p_m,p_n)\big] = q_m^\top k_n\, f(p_m-p_n).$$

The expectation identity that the concentration bound above sharpens; it is the feasibility half of the claim ("this construction is correct on average") that the convergence half needs as its starting point.

Milestone — periodic case via Herglotz's theorem (Corollary 3.3)

For a continuous, positive-definite, $T$-periodic $f$ with $f(0)=1$ and Fourier coefficients $\alpha_k = \frac1T \int_0^T f(x) e^{-i2\pi kx/T}\,dx$,

$$\alpha_k \ge 0 \text{ for all } k \in \mathbb{Z}, \qquad \sum_{k=-\infty}^{\infty} \alpha_k = f(0) = 1.$$

The periodic specialization needed to apply the goal and first milestone with a discrete frequency distribution over harmonics $k/T$ — the regime ClockRoPE actually deploys, since daily/weekly routines are periodic rather than merely decaying.

Significance

The result gives a general recipe — sample, don't hand-design — for turning any admissible attention-modulation profile into a RoPE-compatible rotation schedule, with a concentration guarantee that says how many feature pairs are needed before the sampled schedule reliably approximates the target profile. Crucially, the recipe changes only which frequencies the per-token rotation uses — it never touches the computational shape of RoPE itself: each query and key is still rotated once, independently, by an angle depending only on its own position, and the target pairwise profile $f(p_m-p_n)$ is still recovered purely from the dot product of the two rotated vectors. So realizing an arbitrary positive-definite $f$ this way costs exactly what realizing RoPE's own log-linear profile costs — linear in the sequence length, with no pairwise evaluation of $f$ and no $L\times L$ matrix ever materialized — rather than the quadratic cost a direct, per-pair implementation of an arbitrary modulation function would require. This subsumes standard RoPE's log-linear schedule as one instance and explains, via the periodic corollary, why a schedule built from the kernel's own spectrum (rather than an arbitrary log-linear one) is the right way to encode periodicity: nothing about the construction, or its efficiency, is specific to decay. The paper reports this translated into measured gains in a production-scale generative-retrieval system, which is unusual weight of practical evidence behind a Bochner/Herglotz-style spectral argument.

At the time of writing, none of these three results have a machine-checked proof; this mission asks for the first formalization of all three, together with the shared scaffolding (feature-pair extraction, the rotation estimator, and the notion of a positive-definite kernel) they are stated over.

Difficulty

The natural first attempt at the concentration bound is a direct union bound or a naive variance argument, but the estimator $\hat g$ is a sum of $n$ terms that are each bounded (each rotated pair lies on a fixed-radius circle) rather than governed by a variance bound that shrinks with $n$ under a fixed frequency; the source proof instead applies McDiarmid's bounded-differences inequality, treating each sampled frequency $\xi_j$ as one coordinate of the input and bounding the one-coordinate change in $\hat g$ by $2\lVert q_m^{(j)}\rVert\lVert k_n^{(j)}\rVert$ via the maximal distance between two points on the unit circle — not by directly bounding a variance term. Establishing Proposition 3.1 itself already requires care: it requires justifying that $\tau$, defined purely as an integral transform of $f$, is in fact a legitimate probability density (Bochner's theorem), and then a real/complex bookkeeping argument identifying the real inner product of rotated pairs with the real part of a product of complex exponentials.

Formalization scope

The mission works over the reals and represents feature pairs as functions Fin (2 * n) → ℝ sliced into Fin n-indexed pairs, matching the "$n$ feature pairs, dimension $d = 2n$" convention used throughout; $2\times2$ rotations are ordinary Matrix (Fin 2) (Fin 2) ℝ values built with Matrix.mulVec/Matrix.dotProduct, and expectation over i.i.d. $\tau$-distributed frequencies is formalized as integration against the product measure MeasureTheory.Measure.pi of n independent copies of the measure with density $\tau$ (MeasureTheory.Measure.withDensity) — this is mathematically equivalent to, and more directly usable in Lean than, introducing an abstract probability space with named i.i.d. random variables.

Since a general continuous positive-definite kernel need not have an integrable Fourier transform (the periodic case in Corollary 3.3 is exactly the counterexample: its "Fourier transform" is a discrete measure, not a density) — the goal and first milestone add Integrable f as an explicit hypothesis beyond what the paper states in prose, so that $\tau$ is genuinely a density rather than a junk value. This is not a strengthening of the target profiles the paper cares about in practice (Gaussian, Laplace, and the cosine/Gaussian priors used by ClockRoPE itself are all integrable) and mirrors the paper's own split between the density case (Propositions 3.1–3.2) and the discrete, purely-periodic case (Corollary 3.3). A formalization that dropped this hypothesis and instead let the Fourier integral silently evaluate to Lean's junk value (0 for non-integrable integrands) would make the goal statement possible to "prove" vacuously and must be avoided.

Definitions needed: a positive-definite-kernel predicate, the real-valued Fourier transform of a kernel, feature-pair extraction, the $2\times2$ rotation matrix, and the RFR estimator itself — all reusable by any future mission formalizing RoPE-family positional encodings (e.g. STRING, nD-RoPE) or other random-Fourier-feature results. McDiarmid's inequality, if not already in Mathlib in the needed form, is itself a independently reusable contribution.

Selected references

• Yiwen Chen, Joshua Ainslie, Krzysztof Choromanski, Xiang Gao, Su-Lin Wu, Yiping Yuan, Qian Sun, ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling, 2026. arXiv:2607.26369
• Jianlin Su, Yu Lu, Shengfeng Pan, Ahmed Murtadha, Bo Wen, Yunfeng Liu, RoFormer: Enhanced Transformer with Rotary Position Embedding, arXiv, 2021. arXiv:2104.09864
• Ali Rahimi, Benjamin Recht, Random Features for Large-Scale Kernel Machines, NeurIPS, 2007.
• Salomon Bochner, Monotone Funktionen, Stieltjessche Integrale und harmonische Analyse, Springer, 1933.
• Gustav Herglotz, Über Potenzreihen mit positivem, reellem Teil im Einheitskreis, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, 1911.