Harmonic Analysis

Motivation

The Cauchy–Riemann operator $\bar\partial=\partial_s+i\,\partial_t$ on $\mathbb{C}$ is the model elliptic operator of symplectic topology: pseudoholomorphic curves solve nonlinear perturbations of $\bar\partial u=0$, and their regularity, compactness and Fredholm theory all start from an $L^p$ a priori estimate for $\bar\partial$. In Hofer–Wysocki–Zehnder's asymptotic analysis of pseudoholomorphic curves in symplectisations, this estimate appears as formula (49): on a disc $B$ of radius $R$, every smooth map $\varphi$ supported in the interior of $B$ satisfies

$$\|\varphi\|_{W^{k,p}(B)}\le M(k,p,R)\,\|\bar\partial\varphi\|_{W^{k-1,p}(B)},\qquad k\ge1,\ p>1 .$$

Hofer–Wysocki–Zehnder cite it from E. M. Stein's Singular Integrals and Differentiability Properties of Functions and from Abbas–Hofer's Holomorphic Curves and Global Questions in Contact Geometry.

This mission formalizes estimate (49), together with the core of the real-variable theory of singular integrals on $\mathbb{R}^d$ from Stein, Chapters I–III, and the $L^2$ and $L^p$ estimates for ar\partial of Abbas–Hofer, § 4.2. None of these results is in Mathlib, which has no Hardy–Littlewood maximal function, no Calderón–Zygmund decomposition, no Marcinkiewicz interpolation theorem and no $L^p$ theory of singular integral operators.

Setting

• $\mathbb{R}^d$ carries Lebesgue measure $m$, and $\|\cdot\|_p$ is the $L^p(\mathbb{R}^d)$ norm for complex-valued functions.
• Maximal function. $Mf(x)=\sup_{r>0}m(B(x,r))^{-1}\int_{B(x,r)}|f|\in[0,\infty]$.
• Weak type. An operator $T$ is of weak type $(q,q)$, $q<\infty$, if $m\{|Tf|>\alpha\}\le(A\|f\|_q/\alpha)^q$ for all $\alpha>0$, and of strong type $(p,p)$ if $\|Tf\|_p\le A\|f\|_p$.
• Truncated singular integrals. For a kernel $K$ on $\mathbb{R}^d\setminus\{0\}$ and $\varepsilon>0$, $T_\varepsilon f(x)=\int_{|y|\ge\varepsilon}f(x-y)K(y)\,dy$.
• Cauchy–Riemann operator. For $\varphi:\mathbb{C}\to\mathbb{C}^n$ and $z=s+it$, $\bar\partial\varphi=\varphi_s+i\varphi_t$ (without the factor $\tfrac12$).
• Sobolev norms of smooth maps on a set $U\subset\mathbb{C}$: $\|\varphi\|_{W^{k,p}(U)}=\sum_{j\le k}\|D^j\varphi\|_{L^p(U)}$, where $D^j\varphi$ is the $j$-th derivative.

Formalization targets

Goal: the $W^{k,p}$ estimate for $\bar\partial$ on a disc

For an integer $k\ge1$, $p>1$ and $R>0$ there is $M=M(k,p,R)$ such that for every disc $B\subset\mathbb{C}$ of radius $R$ and every smooth $\varphi:\mathbb{C}\to\mathbb{C}^n$ supported in the interior of $B$, $\|\varphi\|_{W^{k,p}(B)}\le M\|\bar\partial\varphi\|_{W^{k-1,p}(B)}$ (Hofer–Wysocki–Zehnder I, estimate (49), p. 366).

Milestones

1. Maximal theorem. $Mf$ is finite a.e. for $f\in L^p$, $1\le p\le\infty$; $M$ is of weak type $(1,1)$ and of strong type $(p,p)$ for $1<p\le\infty$ (Stein I, § 1.3, Theorem 1).
2. Calderón–Zygmund decomposition. A non-negative integrable $f$ and a height $\alpha>0$ give $\mathbb{R}^d=F\cup\Omega$ with $f\le\alpha$ a.e. on $F$ and $\Omega$ a union of cubes with disjoint interiors on which the average of $f$ lies in $(\alpha,2^d\alpha]$ (Stein I, § 3.2, Theorem 4).
3. Marcinkiewicz interpolation theorem. A sub-additive operator of weak types $(1,1)$ and $(r,r)$, $1<r\le\infty$, is of strong type $(p,p)$ for $1<p<r$ (Stein I, § 4.2, Theorem 5).
4. Convolution kernels with bounded Fourier transform. If $K\in L^2$, $|\hat K|\le B$ and $|\nabla K(x)|\le B|x|^{-d-1}$, then $f\mapsto K*f$ is bounded on $L^p$, $1<p<\infty$, with a constant depending only on $p$, $B$, $d$ (Stein II, § 2.2, Theorem 1).
5. Truncated singular integrals. If $|K(x)|\le B|x|^{-d}$, $\int_{|x|\ge2|y|}|K(x-y)-K(x)|\,dx\le B$ and $K$ has integral zero over every annulus, then the truncations $T_\varepsilon$ are bounded on $L^p$ uniformly in $\varepsilon$ and converge in $L^p$ as $\varepsilon\to0$ (Stein II, § 3.2, Theorem 2).
6. Homogeneous kernels. The same conclusion for $K(y)=\Omega(y)/|y|^d$ with $\Omega$ homogeneous of degree $0$, of mean zero on the unit sphere and Dini-continuous there (Stein II, § 4.2, Theorem 3 (a), (b)).
7. The Cauchy–Riemann estimate on the plane. $\|\partial_1f\|_p+\|\partial_2f\|_p\le A_p\|\partial_1f+i\partial_2f\|_p$ for compactly supported $C^1$ functions $f:\mathbb{R}^2\to\mathbb{C}$, $1<p<\infty$ (Stein III, § 1.3, Proposition 4).
8. $L^2$ identity. $\|\bar\partial\varphi\|_{L^2}^2=\|\varphi_s\|_{L^2}^2+\|\varphi_t\|_{L^2}^2$ for smooth compactly supported $\varphi:\mathbb{C}\to\mathbb{C}^n$ (Abbas–Hofer, § 4.2, (4.4)).
9. $L^2$ estimate on a disc. $\|\varphi_s\|_{L^2}^2+\|\varphi_t\|_{L^2}^2+\|\varphi\|_{L^2}^2\le(4R^2+1)\|\bar\partial\varphi\|_{L^2}^2$ for $\varphi$ with compact support in $B_R(0)$ (Abbas–Hofer, Theorem 4.2.1).
10. $L^p$ estimate on a disc. $\|\varphi\|_{W^{1,p}}\le c(p,R)\|\bar\partial\varphi\|_{L^p}$ for $\varphi$ with compact support in $B_R(0)$, $1<p<\infty$ (Abbas–Hofer, Theorem 4.2.2).

Significance

The result. The $W^{k,p}$ estimate for $\bar\partial$ is the analytic input behind elliptic bootstrapping for pseudoholomorphic curves: interior regularity, $C^\infty$ bounds from gradient bounds, removal of singularities, and the Fredholm theory of linearized Cauchy–Riemann operators on Sobolev spaces. In Hofer–Wysocki–Zehnder's work it controls the derivatives of pseudoholomorphic half-cylinders near a nondegenerate periodic orbit.

Formalizing it. The milestones from Stein are the standard real-variable toolkit of harmonic analysis on $\mathbb{R}^d$: the maximal theorem, the Calderón–Zygmund decomposition, Marcinkiewicz interpolation and the $L^p$ theory of singular integrals with smooth or homogeneous kernels. None of them is in Mathlib, and each is reusable well beyond this mission, for instance for elliptic estimates of other operators, Sobolev embeddings in $L^p$, and other $L^p$ estimates.

Difficulty

The statements are quantitative and the order of quantifiers matters: the constants are chosen before the functions, and in milestones 3 and 4 also before the operator or the kernel, with the dependence stated by the source. Several objects take infinite values or are defined only almost everywhere: the maximal function is valued in $[0,\infty]$, the case $r=\infty$ of the interpolation theorem uses a strong-type bound in place of a weak-type one, and the singular integrals are limits in $L^p$ of absolutely convergent truncated integrals. The Dini condition on $\Omega$ is a condition on a supremum over pairs of points of the unit sphere. The Cauchy–Riemann statements involve vector-valued maps $\mathbb{C}\to\mathbb{C}^n$, real derivatives of all orders and Sobolev norms on discs.

Formalization scope

• Namespace DbarRegularity. The definition module DbarRegularity_Setting defines maximalFunction, closedCube, dbar and sobolevNorm. The mission is standalone and imports no definitions from other missions.
• Spaces. $\mathbb{R}^d$ is EuclideanSpace ℝ (Fin d) with volume, functions on it are complex-valued, $\mathbb{R}^2$ in milestone 7 is EuclideanSpace ℝ (Fin 2), and $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n). Stein's dimension is written $d$ throughout, and $n$ is the dimension of the target $\mathbb{C}^n$.
• Norms and exponents. $L^p$ norms are eLpNorm in ℝ≥0∞. Exponents $1<p<\infty$ are real and enter as ENNReal.ofReal p; exponents allowed to be infinite are in ℝ≥0∞. Constants are in ℝ≥0 or ℝ, never in ℝ≥0∞.
• Derivatives. $\varphi_s$, $\varphi_t$ are fderiv ℝ φ z 1, fderiv ℝ φ z Complex.I; smoothness is ContDiff ℝ ∞ ($C^\infty$, not analytic); higher derivatives are iteratedFDeriv ℝ j. Supports are tsupport.
• Limits. Limits as $\varepsilon\to0$ are along 𝓝[>] 0, in the $L^p$ seminorm.

Contributions welcome: reusable general lemmas of real-variable harmonic analysis on $\mathbb{R}^d$, and calculus lemmas for smooth compactly supported maps on $\mathbb{C}$.

Selected references

• E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), Chapters I–III. ISBN 0-691-08079-8.
• C. Abbas, H. Hofer, Holomorphic Curves and Global Questions in Contact Geometry, Birkhäuser Advanced Texts Basler Lehrbücher, Birkhäuser (2019), § 4.2. https://doi.org/10.1007/978-3-030-11803-7
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations I: asymptotics, Ann. Inst. H. Poincaré Anal. Non Linéaire 13(3) (1996), 337–379. http://www.numdam.org/item/AIHPC_1996__13_3_337_0/
• A. P. Calderón, A. Zygmund, On the existence of certain singular integrals, Acta Math. 88 (1952), 85–139. https://doi.org/10.1007/BF02392130

Motivation

Let $S : S^1 \to \mathbb{R}^{2n\times 2n}$ be a loop of symmetric matrices. The asymptotic operator

$$A_S = -J_0\,\partial_t - S(t)$$

acts on loops $S^1 \to \mathbb{R}^{2n}$. It appears wherever a pseudoholomorphic curve approaches a periodic orbit. Near a puncture, a finite-energy curve in a symplectization converges to a Reeb orbit, and in a trivialization along that orbit the linearized Reeb flow is $\Psi' = J_0 S \Psi$. The operator $A_S$ is the Hessian of the action functional at that orbit. The rate of approach and the winding of the curve around the orbit come from its eigenfunctions (Hofer–Wysocki–Zehnder 1995). In Floer theory the operator $-J_0\partial_t - S$ is the Hessian of the symplectic action at a $1$-periodic orbit, and the gradient-flow operator $\partial_s + A_{S(s)}$ is the linearized Floer operator (Robbin–Salamon 1995).

The operator links functional analysis to the linear algebra of stage I. $A_S$ is nondegenerate, i.e. $0$ is not an eigenvalue, exactly when the time-one map $\Psi(1)$ of the linearized flow has no eigenvalue $1$. Then $\Psi|_{[0,1]}$ lies in $\mathrm{SP}(n)$ and has a Conley–Zehnder index. The Fredholm index formula for Cauchy–Riemann operators on punctured surfaces is written in terms of the Conley–Zehnder indices of the asymptotic operators at the punctures (Wendl, Lectures on SFT, Lecture 3).

This is stage II of a series that formalizes the Fredholm theory of linearized Cauchy–Riemann operators. Stage I (Conley–Zehnder Index I: Axiomatic Characterization on Paths of Symplectic Matrices) characterizes the Conley–Zehnder index on $\mathrm{SP}(n)$. This stage sets up the spectral theory of asymptotic operators: the operator itself, self-adjointness, discrete spectrum, compact resolvent, and the dictionary between the kernel of $A_S$ and the time-one map. Later stages are the Fredholm theory of $\partial_s + A_{S(s)}$ in Banach spaces, elliptic regularity for $\bar\partial$, and the index formula.

Setting

$S^1 = \mathbb{R}/\mathbb{Z}$ with its Haar probability measure. $\mathbb{R}^{2n}$ has coordinates $(q,p)$ and the Euclidean inner product, and

$$J_0 = \begin{pmatrix} 0 & -\mathrm{Id}\\ \mathrm{Id} & 0\end{pmatrix}.$$

$S : S^1 \to \mathbb{R}^{2n\times 2n}$ is continuous with $S(t)^{\mathsf T} = S(t)$ for every $t$.

• Fourier coefficients. For $f \in L^2(S^1,\mathbb{R}^{2n})$ and $k \in \mathbb{Z}$, $\hat f_k = \int_{S^1} e^{-2\pi i k t} f(t)\,dt \in \mathbb{C}^{2n}$.
• Domain. $W^{1,2}(S^1,\mathbb{R}^{2n})$ is the set of $f \in L^2$ with $\sum_{k\in\mathbb{Z}} (1+k^2)\,|\hat f_k|^2 < \infty$.
• The operator. For $f \in W^{1,2}$, $A_S f = g$ means $\hat g_k = -2\pi i k\,J_0 \hat f_k - (Sf)^\wedge_k$ for every $k$, i.e. $g = -J_0 f' - S f$ with the derivative taken in $L^2$. This is Wendl's (3.4) with period $1$.
• Fundamental solution. $\Psi : \mathbb{R} \to \mathbb{R}^{2n\times2n}$ with $\Psi(0) = \mathrm{Id}$ and $\Psi'(t) = J_0 S(t)\Psi(t)$. These are the solutions of $(-J_0\partial_t - S)\Psi = 0$. For constant $S$, $\Psi(t) = \exp(tJ_0S)$ is the path in the signature property of stage I.

Formalization targets

Goal: spectral theory of the asymptotic operator

For every continuous loop $S$ of symmetric matrices:

1. $A_S$ with domain $W^{1,2}$ is self-adjoint on $L^2(S^1,\mathbb{R}^{2n})$;
2. $L^2(S^1,\mathbb{R}^{2n})$ has an orthonormal basis of eigenvectors of $A_S$ lying in $W^{1,2}$; the eigenvalues are real, each has finite multiplicity, and they accumulate only at $\pm\infty$;
3. $\ker A_S \cong \ker(\Psi(1) - \mathrm{Id})$, where $\Psi$ is the fundamental solution.

Milestones

1. Well-defined operator. Exactly one partially defined linear map on $L^2$ has graph $\{(f, A_S f)\}$.
2. Domain. The domain of $A_S$ is $W^{1,2}$, and it is dense in $L^2$.
3. Symmetry. $\langle A_S f, g\rangle = \langle f, A_S g\rangle$ for $f, g \in W^{1,2}$.
4. Self-adjointness.
5. Discrete spectrum. An orthonormal eigenbasis exists, with eigenvalues of finite multiplicity tending to $\pm\infty$.
6. Compact resolvent. If $\mu \in \mathbb{R}$ is not an eigenvalue, $A_S - \mu : W^{1,2} \to L^2$ is bijective and its inverse is a compact operator on $L^2$.
7. Unbounded spectrum. For $n \geq 1$ there are eigenvalues of both signs with arbitrarily large absolute value.
8. The unperturbed operator. The eigenvalues of $-J_0\partial_t$ are exactly $2\pi k$, $k\in\mathbb{Z}$, and each eigenspace has dimension $2n$.
9. Fundamental solution. $\Psi$ exists and is unique for every continuous loop $S$.
10. Symplecticity. If $S$ is symmetric, $\Psi(t) \in \mathrm{Sp}(2n)$ for every $t$.
11. Kernel. $\ker A_S \cong \ker(\Psi(1) - \mathrm{Id})$.
12. Nondegeneracy. $0$ is not an eigenvalue of $A_S$ if and only if $\Psi|_{[0,1]} \in \mathrm{SP}(n)$.

Significance

The result. These are the analytic facts that every use of asymptotic operators relies on. Self-adjointness and the discrete spectrum define the eigenvalue branches and the spectral flow. The compact resolvent makes $A_S - \mu$ Fredholm of index $0$ for every real $\mu$, and the weighted Sobolev spaces of the later Fredholm theory are chosen with weights avoiding the spectrum. The kernel dictionary identifies nondegenerate asymptotic operators with the paths of stage I. It is the bridge through which Conley–Zehnder indices enter the index formula.

Formalizing it. All results here are classical. Mathlib has partially defined linear maps and their adjoints, the Fourier basis of $L^2$ on the circle, and compact operators. It has no Sobolev spaces on the circle, no unbounded operator with discrete spectrum beyond trivial cases, and no first-order differential operator treated as an unbounded operator. This stage builds the first such example. The same pattern applies to other first-order elliptic operators on $S^1$, and the library is reusable for spectral flow and for Floer-type operators.

Difficulty

$A_S$ is unbounded and not defined on all of $L^2$, so self-adjointness is a statement about the domain of the adjoint, not a symmetry identity. The spectral statements concern the resolvent of a first-order differential operator with non-constant coefficients, as an operator on $L^2$. The kernel dictionary relates $L^2$ classes, defined through Fourier coefficients, to classical solutions of a linear ODE. The statements about $\Psi$ concern linear ODEs whose coefficients are only continuous.

Formalization scope

• Namespace AsymptoticOperator; all definitions are in AsymptoticOperator_Setting, which imports stage I's ConleyZehnder_Setting (for Mat n, J₀, IsSymplectic and SP).
• The circle is UnitAddCircle ($\mathbb{R}/\mathbb{Z}$) with AddCircle.haarAddCircle. $L^2(S^1,\mathbb{R}^{2n})$ is Lp (EuclideanSpace ℝ (Fin n ⊕ Fin n)) 2 haarAddCircle, a real Hilbert space.
• Fourier coefficients are Mathlib's fourierCoeff, applied to the componentwise complexification $\mathbb{R}^{2n} \to \mathbb{C}^{2n}$. $J_0$ and $S(t)$ act on $\mathbb{C}^{2n}$ through the real-to-complex coercion.
• The operator is a LinearPMap, defined by choice as the map whose graph is the set of pairs $(f, g)$ satisfying the coefficient identity. The fallback is $0$, and milestone 1 makes it unreachable. Self-adjointness is Mathlib's IsSelfAdjoint for LinearPMap, and symmetry is IsFormalAdjoint.
• Eigenspaces are kernels of $A_S - \mu$ on the domain. The discrete spectrum is stated as a HilbertBasis of eigenvectors whose eigenvalues tend to $\infty$ in absolute value along the cofinite filter. This covers $n = 0$, where $L^2 = 0$.
• Regularity of $S$. Wendl assumes $S$ smooth; Hofer–Wysocki–Zehnder (§3, (35)) take $S$ continuous, as here. HWZ state self-adjointness, compact resolvent and discreteness of the spectrum for $n = 1$; this mission states them for all $n$.
• Sign conventions follow Wendl §3.2: $A_S = -J_0\partial_t - S$ and $\Psi' = J_0S\Psi$.

Contributions welcome: reusable lemmas on Sobolev spaces of vector-valued functions on the circle (Fourier characterization, continuity of $W^{1,2}$ functions), on unbounded self-adjoint operators with compact resolvent, and on linear ODEs with continuous periodic coefficients.

Selected references

• C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 3 (§§3.2–3.4). https://arxiv.org/abs/1612.01009
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations II: Embedding controls and algebraic invariants, Geom. Funct. Anal. 5 (1995), 270–328. https://doi.org/10.1007/BF01895669
• J. Robbin, D. Salamon, The spectral flow and the Maslov index, Bull. London Math. Soc. 27 (1995), 1–33. https://doi.org/10.1112/blms/27.1.1
• D. Salamon, Lectures on Floer homology, in: Symplectic Geometry and Topology, IAS/Park City Math. Ser. 7, AMS (1999), 143–229. https://doi.org/10.1090/pcms/007/05
• J. Gutt, Generalized Conley–Zehnder index, Ann. Fac. Sci. Toulouse Math. (6) 23 (2014), 907–932. https://doi.org/10.5802/afst.1430

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.

Motivation

Reflection positivity and infrared bounds form a standard finite-volume route from the geometry of a lattice reflection to quantitative control of long wavelength fluctuations. In the classical argument, reflection positivity supplies a Cauchy--Schwarz inequality for reflected observables, while Fourier diagonalization of the lattice Laplacian identifies the free covariance used in the infrared comparison. These ingredients underlie rigorous results on continuous-symmetry lattice systems in Fröhlich, Simon, and Spencer's development of infrared bounds and spontaneous symmetry breaking (1976), and the general theory of reflection positivity developed by Fröhlich, Israel, Lieb, and Simon (1978). Related technology appears in Fröhlich and Spencer's treatment of the two-dimensional Abelian spin systems and Coulomb gas (1981).

The analytic and model-specific theorems are substantial, but their finite algebraic interface is sharply separable. This mission isolates that interface so later clock, XY, and Gaussian-domination developments can share one checked notion of reflection, one spectral covariance convention, and one treatment of the constant mode.

Setting

Let $X$ be a finite set of configurations on one side of a reflection plane. A full split configuration is a pair $(x,y)\in X\times X$, and reflection exchanges its two entries. A plus-half observable is a function $F:X\to \mathbb R$ lifted to $X\times X$ through the first coordinate. Its reflected copy therefore depends on the second coordinate.

A split weight is specified by a finite feature index $A$, real coefficients $c_a$, and features $\phi_a:X\to\mathbb R$:

$$W(x,y)=\sum_{a\in A}c_a\phi_a(x)\phi_a(y).$$

For a finite family of plus-half observables $F_i$, the reflected kernel is

$$K_{ij}=\sum_{(x,y)\in X\times X} W(x,y)F_i(x)F_j(y).$$

A real matrix is positive semidefinite here when it is symmetric and its quadratic form is nonnegative on every real coordinate vector.

The spectral side uses a finite mode set $I$ with a distinguished zero mode $0$. An infrared spectrum consists of a function $\lambda:I\to\mathbb R$ that is nonnegative and vanishes exactly at $0$. For $\beta>0$, the free mode covariance is diagonal, equals zero at the constant mode, and has entry

$$G_{kk}=\frac{1}{\beta\lambda_k}$$

away from zero. Covariance domination is tested only on source vectors whose zero-mode coordinate vanishes. The concrete spectral fixture is the $4\times4$ periodic square lattice, with tensor-product discrete Fourier modes and the nearest-neighbor graph Laplacian.

Formalization targets

Finite reflection positivity

The first target identifies the split reflection pairing with the explicit double sum over the two halves. Under $c_a\ge0$, the resulting reflected kernel must be positive semidefinite:

$$\sum_{i,j}u_iK_{ij}u_j\ge0.$$

Every such kernel must satisfy the two-observable chessboard inequality

$$K_{ij}^{2}\le K_{ii}K_{jj}.$$

Typed finite spectrum

For every Torus-4 frequency $k$ and site $x$, the registered Fourier mode $\psi_k$ must satisfy the pointwise eigenvalue equation

$$(\Delta_{\mathrm{T4}}\psi_k)(x)=\lambda_k\psi_k(x).$$

The eigenvalues must be nonnegative and vanish exactly at the constant mode, and these laws must be packaged as the same spectrum type consumed by the infrared definitions.

Zero-mode-restricted infrared bound

The diagonal free covariance must be positive semidefinite for $\beta>0$. If an interacting covariance $C$ is quadratically dominated by $G$ on sources with $u_0=0$, then every nonzero Fourier mode must satisfy

$$C_{kk}\le\frac{1}{\beta\lambda_k}\qquad(k\ne0).$$

Two finite counterfixtures are part of the target. They assert that an arbitrary full-vertex reflected two-point matrix need not be positive semidefinite, and that domination restricted away from the zero mode need not extend to full-matrix domination.

Significance

The resulting interface prevents three substitutions that otherwise look notational but change the theorem. Reflection positivity is tested on observables supported on one half rather than on an arbitrary matrix indexed by all vertices. The infrared comparison excludes the constant mode rather than forcing a fluctuating zero mode below a covariance with zero diagonal. The graph-Laplacian eigenvalue is connected to the Fourier mode by an explicit pointwise theorem rather than by assigning a function the name laplacianEigenvalue.

Several ingredients already have machine-checked Lean proofs in the LeanProofs repository: the finite matrix Cauchy--Schwarz theorem, the Torus-4 DFT diagonalization and zero-mode theorem, and the diagonal free-covariance calculation. This mission reorganizes those results around a corrected consumer boundary and adds the split-half and off-zero adapters. It does not present the finite statements as new mathematics.

Difficulty

The main difficulty is maintaining the correct domain at each interface. A reflection of lattice sites does not by itself imply positive semidefiniteness of a correlation matrix indexed by every site; the tested observables and their support are part of the assertion. Likewise, a free covariance whose constant-mode entry is defined to be zero cannot dominate an arbitrary covariance on all source vectors. Finally, a Fourier multiplier used for a pseudospectral derivative is not automatically the eigenvalue of the nearest-neighbor graph Laplacian. The formal statements must keep these three objects distinct.

Formalization scope

All configuration, feature, observable, and mode types are finite. Kernels, weights, coefficients, source vectors, and quadratic forms are real. Complex numbers occur only in the explicit discrete Fourier modes. Reflected pairings are unnormalized finite sums; no partition function or probability measure is introduced. The inverse temperature satisfies $\beta>0$. The distinguished zero mode is part of the spectrum interface, and infrared domination is restricted to source vectors that vanish at that coordinate.

The mission does not assert reflection positivity of a clock or XY Gibbs measure, nonnegative Fourier coefficients of a physical cross-bond weight, Gaussian domination, a thermodynamic limit, a Kosterlitz--Thouless transition, or a universal jump. It also does not identify the Torus-4 graph spectrum with the Grid3 pseudospectral multiplier from the Fourier--Hodge packet. Those are separate future missions requiring additional model and analytic input.

The reusable outputs are the split-weight RP interface, the finite positive-semidefinite kernel API, the typed spectrum object, and the zero-mode-restricted domination predicate. Contributions should preserve the explicit half support and zero-mode restrictions; a proof obtained by adding the desired conclusion as a hypothesis is outside scope.

Selected references

• J. Fröhlich, B. Simon, and T. Spencer, Infrared bounds, phase transitions and continuous symmetry breaking, Communications in Mathematical Physics 50 (1976), 79--95. https://doi.org/10.1007/bf01608557
• J. Fröhlich, R. Israel, E. H. Lieb, and B. Simon, Phase transitions and reflection positivity. I. General theory and long range lattice models, Communications in Mathematical Physics 62 (1978), 1--34. https://doi.org/10.1007/bf01940327
• J. Fröhlich and T. Spencer, The Kosterlitz--Thouless transition in two-dimensional Abelian spin systems and the Coulomb gas, Communications in Mathematical Physics 81 (1981), 527--602. https://doi.org/10.1007/bf01208273
• LeanProofs, ReflectionPositivityInfraredBound.lean, exact repository snapshot dbf503b2909cc17787d40a21eb75a0c9354cc6ef. https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.lean