Harmonic Analysis

1. Motivation

Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, stated unambiguously — by machine.

This mission ports a coherent slice of that material to Prove2Me. It is deliberately a portfolio mission: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. A reader should not assume that proving a milestone advances the goal theorem. The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked.

A rough timeline of the collection's landmarks:

• 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
• 1962 — Radó: the busy beaver function outgrows every computable function.
• 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$.
• 1978 — Apéry: $\zeta(3)$ is irrational.
• 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant subspace.
• 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
• 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
• 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
• 2021 — Gardam: Kaplansky's unit conjecture is false (its zero-divisor and idempotent companions remain open).
• 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$.
• 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$.

2. Setting

The goal theorem concerns prime values of polynomials. Fix a finite set $S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the Bunyakovsky condition if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is irreducible over $\mathbb{Z}$; say that $S$ satisfies the Schinzel condition if for every prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides the product at every argument.

For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some $f_i$ vanishes, let $D=\prod_i \deg f_i$, and let

$$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$

The Bateman–Horn constant is the (conditionally convergent) Euler product

$$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$

The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property $\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function $\mathrm{BB}$.

3. Target

The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, $C$ exists and is positive and

$$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$

Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$, Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the $1/3$–$2/3$ conjecture), and computability (Radó's theorem).

4. Significance

The results themselves. Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right.

Formalizing them. None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$ cannot both be algebraic, and Radó's diagonal argument.

5. Difficulty

For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound $\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered infinite product changes the statement.

Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on $\ell^1$ show that no soft argument can work.

6. Formalization scope

Conventions this mission commits to, all fixed in the definition items:

• Polynomials are elements of ℤ[X]; primality of a polynomial value is primality of its absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$.
• The Bateman–Horn constant is the limit of the ordered partial products over $p<N$, not an unordered infinite product.
• Kakeya sets carry no compactness or measurability hypothesis, matching the source; the conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$.
• Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$.
• Torsion-freeness of a group is spelled out as "every element of finite order is the identity", which is the hypothesis the source intends (it is weaker than Mathlib's IsMulTorsionFree).
• Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities are quotients of set cardinalities in $\mathbb{Q}$.
• The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition included, and $\mathrm{BB}(0)=0$.
• Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me statements must be definite, so each such question is recorded in its affirmative form (e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth theorem rather than guessed at.
• Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).

Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission.

7. Selected references

• P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Math. Comp. 16 (1962), 363–367. DOI
• T. Radó, On non-computable functions, Bell System Tech. J. 41 (1962), 877–884. DOI
• R. O. Davies, Some remarks on the Kakeya problem, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. DOI
• C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$, Bull. London Math. Soc. 17 (1985), 305–317. DOI
• K. Falconer, On the Hausdorff dimensions of distance sets, Mathematika 32 (1985), 206–212. DOI
• W. Zudilin, One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational, Russian Math. Surveys 56 (2001), 774–776. DOI
• P. Mihăilescu, Primary cyclotomic units and a proof of Catalan's conjecture, J. reine angew. Math. 572 (2004), 167–195. DOI
• Z. Dvir, On the size of Kakeya sets in finite fields, J. Amer. Math. Soc. 22 (2009), 1093–1097. DOI
• B. Bukh and T.-W. Chao, Sharp density bounds on the finite field Kakeya problem, Discrete Analysis 26 (2021). DOI
• G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021), 967–979. DOI
• K. Saito, Mills' constant is irrational, Mathematika 71 (2025), e70027. arXiv:2404.19461
• H. Wang and J. Zahl, Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions, arXiv:2502.17655
• Google DeepMind, Formal Conjectures, Apache-2.0, github.com/google-deepmind/formal-conjectures

---

Provenance note. The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; those read-backs are non-blind — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.

Motivation

Reservoir computing learns an input/output system from data in two stages. A dynamical system, the reservoir, is driven by the input sequence and its state is recorded; then only a linear readout of that state is trained, by least squares. The echo state network (ESN) is the most widely used reservoir: its state evolves by $x_t = \sigma(Ax_{t-1} + Cz_t + \zeta)$, with the matrices $A, C$ and the vector $\zeta$ drawn at random and never trained. ESNs predict chaotic systems well in practice (Jaeger & Haas, Science 2004), and they are known to be universal: for every fading-memory input/output map some ESN approximates it (Grigoryeva & Ortega, Neural Netw. 2018). Universality does not explain the practice, where the reservoir weights are random and fixed in advance. Gonon, Grigoryeva & Ortega (Ann. Appl. Probab. 2023) prove that an ESN whose weights are drawn from an explicit distribution that does not depend on the target approximates every sufficiently regular target, with an explicit $L^2$ error bound. This mission formalizes that result, Theorem 2, and the chain of results its proof rests on.

Setting

Time runs over $\mathbb Z_- = \{0, -1, -2, \dots\}$. Inputs take values in a set $D_d$ with $0 \in D_d \subset B_M \subset \mathbb R^d$, where $B_M$ is the closed Euclidean ball of radius $M > 0$. The input $Z = (Z_t)_{t \in \mathbb Z_-}$ is a $D_d$-valued process with law $\mu_Z$. The target is a functional $H^* : (D_d)^{\mathbb Z_-} \to \mathbb R$, the present output as a function of the whole input history. All norms are Euclidean.

Regularity. Fix weights $w_{-i} > 0$ with $\sum_i i\, w_{-i} < \infty$. $H^*$ is $w$-Lipschitz with constant $L > 0$ if $|H^*(u) - H^*(v)| \le L\sum_{i \ge 0} w_{-i}\|u_{-i} - v_{-i}\|$. Assumption 1 asks, in addition, for every $T \ge 1$: with $q = d(T+1)$, the truncation $H^*_T(z_0, \dots, z_{-T}) = H^*(\dots, 0, z_{-T}, \dots, z_0)$ has a Fourier representation $H^*_T(u) = \int_{\mathbb R^q} e^{i\langle w, u\rangle} g_T(w)\,dw$ on $(D_d)^{T+1}$, with $g_T \in L^1$ and $\int \max(1, \|w\|^3)|g_T(w)|^2\,dw < \infty$.

The random ESN. Fix $T, N \ge 1$, $R > 0$, and a bound $M_T$ with $\|(Z_0, \dots, Z_{-T})\| \le M_T$ almost surely. Draw $A_1, \dots, A_N$ i.i.d. uniform on $B_R \subset \mathbb R^q$ and, independently, $\zeta_1, \dots, \zeta_N$ i.i.d. uniform on $[-\max(M_TR,1), \max(M_TR,1)]$. With $S$ the block shift on $\mathbb R^q$ and $c$ the embedding of $\mathbb R^d$ into the first block, and $a$ the matrix with rows $A_i^\top$, put

$$\bar A = \begin{pmatrix} S & 0\\ aS & 0\end{pmatrix},\quad \bar C = \begin{pmatrix} c\\ ac\end{pmatrix},\quad \bar\zeta = \begin{pmatrix} 0\\ \zeta\end{pmatrix},\quad A = \begin{pmatrix}\bar A & -\bar A\\ -\bar A & \bar A\end{pmatrix},\quad C = \begin{pmatrix}\bar C\\ -\bar C\end{pmatrix},\quad \zeta = \begin{pmatrix}\bar\zeta\\ -\bar\zeta\end{pmatrix}.$$

The ESN is $X_t = \sigma(AX_{t-1} + CZ_t + \zeta)$, $Y_t = WX_t$, with $\sigma(x) = \max(x, 0)$ and state space $\mathbb R^{2(N+d(T+1))}$.

Formalization targets

Goal: Theorem 2 (p. 54)

For every $H^*$ satisfying Assumption 1 there is a readout $W$, a function of the random weights alone, such that the ESN has the echo state property (a unique state sequence for every input) and

$$\mathbb E\big[|Y_0 - H^*(Z)|^2\big]^{1/2} \le \frac{\sqrt{C_{T,R}}}{\sqrt N} + \int_{\mathbb R^q \setminus B_R}|g_T(u)|\,du + LM\sum_{i > T} w_{-i},$$

with $C_{T,R} = 16\max(M_TR,1)\mathrm{Vol}_q(B_R)(M_T+1)^2(M_T^3+M_T+16)\int_{B_R}\max(1,\|u\|^3)|g_T(u)|^2\,du$.

Milestones

1. (8), p. 33: a scalar identity expressing $e^{iz} - iz - 1$ as an integral of ReLU ramps.
2. Proposition 2, pp. 31–32: under a Fourier condition, $f$ is an integral of ReLU ridge functions with a compactly supported, square-integrable weight $\pi$.
3. Proposition 3, pp. 41–42: a static ReLU network with uniformly sampled inner weights achieves mean-square error $C^*/N$.
4. Corollary 1, p. 43: the same with a dimension-free integrability condition and a truncation term.
5. Remark 10, p. 53: the shift reservoir is nilpotent, has $K = I$ and stores the last $T+1$ inputs.
6. Proposition 6, p. 51: a linear reservoir with a random ReLU readout satisfies the bound (54).
7. (64)–(66), pp. 55–56: every solution of the ESN reduces to the linear shift reservoir, which gives uniqueness.

Significance

Theorem 2 is the first approximation bound for echo state networks whose recurrent and input weights are sampled from a generic distribution rather than constructed from the target. The bound separates three error sources: a Monte Carlo term decaying like $N^{-1/2}$, a truncation term in the sampling radius $R$, and a memory term in the window length $T$. Because the readout can be taken to be the least-squares readout, the bound also controls the trained networks used in practice, and it is the input to the paper's rate and universality corollaries (Corollaries 4 and 5).

Status: the result is proved on paper. No part of it is formalized; the only reservoir-computing material on the platform is the published definition ReservoirESN (the state equation), which this mission reuses. A formal proof would supply the first machine-checked random-feature approximation bound with explicit constants.

Difficulty

The obvious argument fails in two places. First, the classical integral representations of Barron type place the inner weights on unbounded sets, which cannot be sampled uniformly; Proposition 2 needs a change of variables that makes the weight compactly supported while keeping it square integrable, and this costs the factor $R^{-(2q+2)}$ and the condition (5). Second, a ReLU network is not contractive, so the echo state property of the ESN cannot be taken from the standard contraction criterion; it has to be derived from the block structure of $A$, which makes the difference of the two state halves follow a nilpotent linear recursion.

Formalization scope

$\mathbb R^q$ is EuclideanSpace ℝ (Fin (T+1) × Fin d), block $k$ holding $z_{-k}$; input sequences are ℕ → EuclideanSpace ℝ (Fin d) with index $k = -t$, and $x_t = F(x_{t-1}, z_t)$ is the published ReservoirESN.IsSolution. Points of $\mathbb R^{q+1}$ are pairs with norm $(\|w\|^2 + u^2)^{1/2}$. The uniform laws are Lebesgue measure conditioned on the ball or interval; $N$ i.i.d. rows have the product law. The input is independent of the weights (§4.1) and $D_d$-valued with $0 \in D_d \subset B_M$ (§5.1): expectations are iterated lower Lebesgue integrals over $\mu_Z$ and the product law, and probability-$(1-\delta)$ statements bound the product measure of the bad set. The scalar output case $m = 1$ is used, as in the paper. Assumption 1 is required for every $T \ge 1$, as printed.

A readout allowed to depend on the input would make every bound trivial; in every statement the readout is a measurable function of the inner weights alone.

Departures from the print, each disclosed in the item: the last term of Proposition 6 is the $L^2(\mu_Z)$ norm of $\|K^{-1}S^{T+1}X_{-T-1}\|$, which the page prints outside the expectation; the state space of the linear reservoir (52) is a parameter $D_N$, as in §2.1, and its solution is assumed to be a random process; Proposition 3 omits "$C^* > 0$" (the explicit value (33) is used); measurability of the Fourier density $g$ is stated where the page leaves it implicit.

A complete development needs Fourier integrals on Euclidean spaces, change of variables under linear maps, product measures and Fubini–Tonelli, and an importance-sampling variance bound. The static results (Propositions 2, 3, Corollary 1) are reusable for random-feature models beyond reservoir computing. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• L. Gonon, L. Grigoryeva, J.-P. Ortega, Approximation bounds for random neural networks and reservoir systems, Ann. Appl. Probab. 33(1), 28–69, 2023. https://doi.org/10.1214/22-AAP1806
• L. Grigoryeva, J.-P. Ortega, Echo state networks are universal, Neural Netw. 108, 495–508, 2018. https://doi.org/10.1016/j.neunet.2018.08.025
• H. Jaeger, H. Haas, Harnessing nonlinearity: predicting chaotic systems and saving energy in wireless communication, Science 304, 78–80, 2004. https://doi.org/10.1126/science.1091277
• A. R. Barron, Universal approximation bounds for superpositions of a sigmoidal function, IEEE Trans. Inf. Theory 39, 930–945, 1993. https://doi.org/10.1109/18.256500
• J. M. Klusowski, A. R. Barron, Approximation by combinations of ReLU and squared ReLU ridge functions with ℓ1 and ℓ0 controls, IEEE Trans. Inf. Theory 64, 7649–7656, 2018. https://doi.org/10.1109/tit.2018.2874447
• C. Cuchiero, L. Gonon, L. Grigoryeva, J.-P. Ortega, J. Teichmann, Discrete-time signatures and randomness in reservoir computing, IEEE Trans. Neural Netw. Learn. Syst., 2021. https://doi.org/10.1109/TNNLS.2021.3076777

Motivation

Maximizing a homogeneous polynomial $p$ over the unit sphere, $p_{\max}=\max_{x\in S^{d-1}}p(x)$, covers the largest stable set of a graph (degree three), the $2\to4$ norm of a matrix (degree four) and the best separable state problem of quantum information. For quadratic $p$ it is an eigenvalue problem; for degree at least three it is NP-hard. The sum-of-squares hierarchy of Parrilo and Lasserre replaces "$\gamma-p\ge0$ on the sphere" by "$\gamma-p$ is a sum of squares of polynomials of degree at most $\ell$ on the sphere", giving upper bounds $p_\ell\ge p_{\max}$ that are computable by a semidefinite program of size $d^{O(\ell)}$ and decrease to $p_{\max}$. How fast they converge decides how large $\ell$ has to be for a given accuracy. Fang–Fawzi, §1–1.1

Timeline:

• 1995. Reznick shows, for $p_{\min}=0$, that $p_\ell/p_{\max}\to1$ at rate $d/\ell$ for $\ell$ large enough. Rez95
• 2012. Doherty and Wehner study the same hierarchy on the hypersphere and obtain the same rate. DW12
• 2019. De Klerk and Laurent prove a rate $O(1/\ell^2)$ for a hierarchy of lower bounds on $p_{\max}$, and ask whether the upper bounds $p_\ell$ converge at the same rate. dKL19
• 2019. Fang and Fawzi answer this: for $\ell\ge C_nd$ the error is $O((d/\ell)^2)$, and the statement holds for symmetric matrix-valued polynomials with constants that do not depend on the matrix size. Fang–Fawzi, Theorems 1–2

Setting

Write $x=(x_1,\dots,x_d)$, $\|x\|^2=\sum_ix_i^2$, and $S^{d-1}=\{x\in\mathbb R^d:\|x\|^2=1\}$. A $k\times k$ matrix polynomial $F$ has a real polynomial in each entry, and $F(x)$ is the real matrix of values. $A\succeq0$ means that the symmetric matrix $A$ is positive semidefinite. A matrix polynomial $G$ is $\ell$-sos on $S^{d-1}$ if there are finitely many $k\times k$ matrix polynomials $U_j$, each entry of total degree at most $\ell$, with

$$G(x)=\sum_jU_j(x)U_j(x)^{\mathsf T}\qquad\text{for all }x\in S^{d-1}.$$

For a scalar polynomial $p$, $p_\ell$ is the least $\gamma$ such that $\gamma-p$ (a $1\times1$ matrix) is $\ell$-sos on $S^{d-1}$, and $p_{\min}$ is the minimum of $p$ on $S^{d-1}$. The level value is $+\infty$ when no such $\gamma$ exists.

The milestones use three further objects. A harmonic decomposition of a homogeneous $f$ of degree $2n$ is $f=\sum_{k=0}^n\|x\|^{2(n-k)}f_{2k}$ with $f_{2k}$ homogeneous of degree $2k$ and $\Delta f_{2k}=0$. $B_{2n}$ is the least constant with $\max_{S^{d-1}}|f_{2k}|\le B_{2n}\max_{S^{d-1}}|f|$ for all such $f$ in all dimensions. The Gegenbauer coefficients $\lambda_i(\phi)$ of a univariate polynomial $\phi$ are its coefficients against the orthogonal polynomials $C_i$ for the weight $(1-t^2)^{(d-3)/2}$ on $[-1,1]$, equation (9). For $q$ of degree at most $\ell$, the kernel error is

$$\rho_{2n}(d,\ell)=\min_{\deg q\le\ell,\ \lambda_0(q^2)=1}\ \sum_{k=1}^n\big|\lambda_{2k}(q^2)^{-1}-1\big|.$$

Formalization targets

Goal: Theorem 2 (p. 3)

For every $n$ there are constants $C_n,C'_n$ depending only on $n$ such that, for all $d,k,\ell$ and every $k\times k$ matrix polynomial $F$, homogeneous of degree $2n$ with $n\le d$, symmetric at every $x$, with $0\preceq F(x)\preceq I$ on $S^{d-1}$:

$$\ell\ge C_nd\ \Longrightarrow\ F+C'_n\Big(\frac d\ell\Big)^2I\ \text{is }\ell\text{-sos on }S^{d-1}.$$

The goal fixes only the shape $(d/\ell)^2$ and the regime $\ell\ge C_nd$, and leaves the constants open.

Milestones

They follow the paper's proof, in attack order:

1. Harmonic projection: Lemma 16 (Reznick's bound on $\Delta^kf$), Proposition 5 ($B_{2n}$ is independent of $d$, with $B_2\le2$, $B_4\le9$), the explicit value (34), and Proposition 17 (matrices, spectral norm).
2. Kernels: the Funk–Hecke formula (8), Remark 1, and the first part of Theorem 6: $F+\frac{B_{2n}}2\sum_k|\lambda_{2k}^{-1}-1|\,I$ is $\ell$-sos for every admissible $q$.
3. The kernel error: $C_i'(1)/C_i(1)=i(i+d-2)/(d-1)$, Proposition 18 (tangent line at $1$), Proposition 8 (spectra of Toeplitz matrices of linear functions), the value of $h'(1)$ and the eigenvalue comparison from the proof of Proposition 7, Proposition 9 ($\rho\le\tilde\rho/(1-\tilde\rho)$), and the second part of Theorem 6:

$$\rho_{2n}(d,\ell)\le C_n\Big(\frac d\ell\Big)^2\qquad(\ell\ge C'_nd).$$

4. Corollary: Theorem 1, $1\le\frac{p_\ell-p_{\min}}{p_{\max}-p_{\min}}\le1+(C_nd/\ell)^2$ for $\ell\ge C_nd$.

Significance

Theorem 2 says how the level must grow with the dimension: $\ell=\Theta(d/\sqrt\varepsilon)$ suffices for relative error $\varepsilon$, where Reznick's analysis needs $\ell=\Theta(d/\varepsilon)$. Theorem 10 of the paper shows that, for $n=1$, the kernel error of this technique really is of order $(d/\ell)^2$. Independence of the matrix size gives certificates for polynomials that are bihomogeneous of degree $(2n,2)$ on $S^{k-1}\times S^{d-1}$. The paper's Theorem 15 uses this, together with the DPS duality of the companion mission, to bound the convergence of the DPS hierarchy for separability. Fang–Fawzi, pp. 3, 10, 14

The theorem is proved in the 2019 preprint and was published in Mathematical Programming in 2021. No machine-checked proof of it or of its ingredients is known. Proving it formally takes reusable infrastructure: degree-bounded matrix SOS on the sphere, harmonic decomposition of homogeneous polynomials, Gegenbauer polynomials with their coefficients and the Funk–Hecke formula, and spectra of Jacobi matrices of orthogonal polynomials. The milestones also correct the printed text, as listed under Formalization scope.

Difficulty

Positive semidefiniteness of $F+\delta I$ at each point of the sphere does not give a factorization with factors of prescribed degree, and Reznick's kernel $\langle x,y\rangle^{2\ell}$ only reaches error $d/\ell$. Two estimates must be uniform at once. First, harmonic projection of a degree-$2n$ form must be bounded in sup norm independently of $d$; the $L^2$ bound is easy, and the sup-norm bound is the content of Proposition 5. Second, the kernel error $\rho_{2n}(d,\ell)$ must be bounded throughout the regime $\ell\ge C_nd$, which comes down to the location of the largest zero of a Gegenbauer polynomial. The printed bounds on that zero and on $\lambda_{\max}$ in Proposition 7 are false in small dimensions, so the paper's explicit constants cannot be relied on.

Formalization scope

• Objects. $\mathbb R^d$ is Fin d → ℝ (0-based coordinates), and $S^{d-1}$ is the equation $\sum_ix_i^2=1$, not the sup-norm sphere. Matrix polynomials are matrices over MvPolynomial (Fin d) ℝ, evaluated entrywise, and homogeneity is entrywise.
• $\ell$-sos. A finite family of $k\times k$ factors, every entry of total degree at most $\ell$, with equality on the sphere only. Without the degree bound the level disappears; with equality on all of $\mathbb R^d$ Theorem 2 becomes false. Neither change is a faithful reading.
• Constants. In the goal the constants are chosen before $d$, $k$, $\ell$ and $F$. No assumption $d\ge2$ is added: the cases $d=0,1$ are true and elementary.
• Standing assumption $d\ge2$. Every milestone that uses the Gegenbauer objects assumes it, as §2–3 do: the weight $(1-t^2)^{(d-3)/2}$, $\omega_{d-1}/\omega_d$ and the divisions by $d-1$ need it. Gegenbauer polynomials are normalized by $C_i(1)$ and defined by their three-term recurrence. $\sigma$ is the normalized surface measure built from Mathlib's Measure.toSphere.
• $B_{2n}$. It is not defined (it would be a real infimum). Statements quantify over every constant $B$ with the defining property, and $B_{2n}$ is one of them.
• $\rho_{2n}$. It takes values in $[0,\infty]$, with $|\lambda^{-1}-1|=\infty$ at $\lambda=0$ and $\infty$ on an empty feasible set. Its sum runs over $k=1,\dots,n$, following (12), (13) and (16); (10) prints $2n$, a slip. Its minimum is over $\deg q\le\ell$, as in (13). The first part of Theorem 6 is posed per polynomial $q$, which is what (12) proves and implies the printed form.
• Other conventions. Proposition 17's spectral norm is written as $\max_{\|y\|=1}|y^{\mathsf T}Ay|$, and homogeneity of $F$ is explicit there. Theorem 1 is stated cross-multiplied, so that it is meaningful when $p$ is constant on the sphere. Its level value is extended real to record infeasibility; the theorem asserts a finite attained value and a degree-bounded SOS certificate.
• Not posed. Proposition 7 ($\lambda_{\max}(\mathcal T[h])\ge1-\frac{7n}{12}\frac{d^2}{\ell^2}$) fails, for example, at $d=2$, $n=1$, $\ell=10$. The zero bound it quotes and the explicit constants at the end of p. 9 are not posed either; the true first inequality of its proof is.

Proofs of any milestone are welcome. So are reusable developments of Gegenbauer polynomials, spherical harmonics, the Funk–Hecke formula, Jacobi matrices, and Carathéodory-type finite quadratures that turn an integral of squares into a finite sum of squares.

Selected references

• K. Fang, H. Fawzi, The sum-of-squares hierarchy on the sphere, and applications in quantum information theory, arXiv preprint, 2019. https://arxiv.org/abs/1908.05155v1
• B. Reznick, Uniform denominators in Hilbert's seventeenth problem, Mathematische Zeitschrift 220(1), 75–97, 1995. https://doi.org/10.1007/BF02572604
• A. C. Doherty, S. Wehner, Convergence of SDP hierarchies for polynomial optimization on the hypersphere, arXiv preprint, 2012. https://arxiv.org/abs/1210.5048
• E. de Klerk, M. Laurent, Convergence analysis of a Lasserre hierarchy of upper bounds for polynomial minimization on the sphere, arXiv preprint, 2019. https://arxiv.org/abs/1904.08828
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization 11(3), 796–817, 2001. https://doi.org/10.1137/S1052623400366802

Motivation

A quantum algorithm for a system of linear equations must turn operations it can implement into an approximation of the inverse of the system matrix. For a Hermitian matrix, time evolution $e^{-iAt}$ is such an operation. Childs, Kothari and Somma use a Fourier expansion of the scalar reciprocal $1/x$ to express an approximation to $A^{-1}$ as a finite linear combination of these evolutions. Their paper reports an exponential improvement in the dependence on the requested precision over earlier linear-systems methods. The scalar approximation in Lemma 11 is the mathematical input to their Fourier algorithm and to the query and gate analyses in Theorem 3. This mission isolates that approximation and the Gaussian estimates stated around it. Theorem 3's complexity claims themselves are outside the present formalization. Childs, Kothari and Somma, §3, pp. 10–14.

Setting

Fix a condition number $\kappa\ge1$. The scalar spectral domain is

$$D_\kappa=[-1,-1/\kappa]\cup[1/\kappa,1].$$

It contains the real eigenvalues permitted after the paper's normalization and excludes zero, where the reciprocal is undefined. For an accuracy $\varepsilon>0$, two functions are $\varepsilon$-close on $D_\kappa$ when their difference has magnitude at most $\varepsilon$ at every point of that domain. A complex-valued approximant is compared with $1/x$ as a complex number. The paper gives this domain and closeness convention before the Fourier construction. Childs, Kothari and Somma, pp. 9–10.

The intermediate function $g_{y_J,z_K}(x)$ is a truncated Gaussian Fourier integral. It integrates $z e^{-z^2/2}e^{-ixyz}$ over $-z_K\le z\le z_K$ and then over $0\le y\le y_J$, multiplying by $i/\sqrt{2\pi}$. The finite approximant $h_{J,K,\Delta_y,\Delta_z}(x)$ is a Gaussian Fourier double sum with the same normalization and phase. Its samples are $y_j=j\Delta_y$ for $j=0,\ldots,J-1$ and $z_k=k\Delta_z$ for $k=-K,\ldots,K$; each term carries both mesh widths. Thus $J,K$ count the retained samples, while $\Delta_y,\Delta_z$ control their spacing. The sign in the phase and the factor $i$ are part of the definitions. Childs, Kothari and Somma, (18), p. 10, and (21), p. 11.

Formalization targets

Truncation

Lemma 12 says that for cutoffs of scale

$$y_J=\Theta\!\bigl(\kappa\sqrt{\log(\kappa/\varepsilon)}\bigr), \qquad z_K=\Theta\!\bigl(\sqrt{\log(\kappa/\varepsilon)}\bigr),$$

the function $g_{y_J,z_K}$ is $\varepsilon$-close to $1/x$ on $D_\kappa$. The proposal includes the paper's explicit error bound (27) and its Gaussian tail bound (28), as well as the Gaussian Poisson-summation identity of Lemma 13. These are separate reusable targets, not replacements for the approximation theorem. Childs, Kothari and Somma, Lemmas 12–13 and (27)–(28), pp. 11–12.

Finite Fourier sum

The goal is Lemma 11:

$$\left|h_{J,K,\Delta_y,\Delta_z}(x)-\frac1x\right|\le\varepsilon \quad\text{for every }x\in D_\kappa,$$

where

$$J=\Theta\!\left(\frac\kappa\varepsilon\log\frac\kappa\varepsilon\right),\quad K=\Theta\!\left(\kappa\log\frac\kappa\varepsilon\right),\quad \Delta_y=\Theta\!\left(\frac\varepsilon{\sqrt{\log(\kappa/\varepsilon)}}\right),\quad \Delta_z=\Theta\!\left(\frac1{\kappa\sqrt{\log(\kappa/\varepsilon)}}\right).$$

The $\Theta$ statements impose upper and lower bounds with absolute constants, uniformly across $\kappa$ and $\varepsilon$. The requested approximation error is exactly $\varepsilon$, matching the lemma's claim. The four scales specify both the size of the finite expansion and its mesh. Childs, Kothari and Somma, Lemma 11, p. 10.

Significance

The finite sum provides the paper's Fourier route from scalar reciprocal approximation to a linear combination of time-evolution operators. Its sample counts and spacings are the quantities that enter the algorithm's implementation costs. A result that only asserted approximation after arbitrarily many samples would not express the bound used there. The truncated integral and Poisson identity also remain useful for other Gaussian quadrature and Fourier-sampling arguments. Childs, Kothari and Somma, §§3.1–3.2, pp. 11–14.

The paper proves these claims on paper. This proposal asks for machine-checked Lean proofs of the scalar statements, including the complex normalization, the finite and infinite sum conventions, and the uniform scale bounds. It does not assert that the quantum algorithm, its Hamiltonian simulation subroutines, or its query and gate complexity theorems have been formalized.

Difficulty

The infinite Gaussian Fourier representation alone does not specify a finite implementable expansion. Restricting both integrals introduces two truncation errors, while replacing them by samples adds discretization and periodic-aliasing effects. These errors have to be controlled simultaneously with $J$, $K$, $\Delta_y$, and $\Delta_z$ at the scales stated in Lemma 11. Merely taking the mesh arbitrarily fine gives approximation without the theorem's finite-size bounds. The proof also uses a complex Fourier phase although its target is real, and its infinite sums must have their ordinary convergent meaning. Childs, Kothari and Somma, proof of Lemma 11, pp. 13–14.

Formalization scope

The Lean development uses $\mathbb R$ for $x,\kappa,\varepsilon$ and the cutoff and mesh parameters, $\mathbb C$ for $g$ and $h$, and the complex norm for closeness. Finite sums use exactly $0\le j<J$ and $-K\le k\le K$; the integral for $g$ is iterated and has nonnegative upper cutoffs. The optional identity (20) is also an iterated integral, with the $z$ integral evaluated before the $y$ integral. Infinite sums in Lemma 13 are over $\mathbb Z$. The Gaussian integrals and series in the statements are convergent, so Lean's totalized integral and sum conventions do not supply artificial zero values.

The paper's condition-number convention is recorded as $\kappa\ge1$ and Corollary 10's operating range as $0<\varepsilon<1/2$. Those conditions keep $D_\kappa$ nonempty and $\log(\kappa/\varepsilon)$ positive. The unnumbered reciprocal-exponential bound from p. 13 has $x\ne0$ explicitly, because the printed fractions have no value at zero. The $\Theta$ bounds quantify their constants before the problem parameters. In particular, choices with unbounded sample counts or vanishing mesh widths cannot satisfy the goal solely by brute-force approximation.

A complete development needs reusable Gaussian integration and tail estimates, complex exponential identities, summability of Gaussian integer series, and Poisson summation in Mathlib's analytic setting. Contributions that establish these general facts, the stated milestones, or Lemma 11 with its original bounds all fit this scope. This mission uses the reviewed shared definition of $D_\kappa$. Childs, Kothari and Somma, pp. 9–14.

Selected references

• A. M. Childs, R. Kothari and R. D. Somma, Quantum algorithm for systems of linear equations with exponentially improved dependence on precision, SIAM Journal on Computing 46(6), 2017; arXiv:1511.02306v2.

Motivation

Fourier analysis of functions on the discrete cube $\{-1,1\}^n$ is the main tool behind tight inapproximability results under the Unique Games Conjecture. In the MAX-CUT reduction of Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 2007), soundness rests on the Majority Is Stablest theorem: among bounded functions in which no coordinate has large influence, the majority function is asymptotically the most noise stable. That theorem was a conjecture when the paper was written and was proved by Mossel, O'Donnell and Oleszkiewicz (Annals of Math. 2010) using an invariance principle.

Section 6.2 of the paper records special cases of Majority Is Stablest that have short, self-contained proofs. Theorem 6 is the case where the noise parameter $\rho$ tends to $0$. There the noise stability is dominated by the Fourier weight at level 1, and the statement says that a bounded function with small influences has level-one weight at most $2/\pi$, up to an explicit error linear in the largest influence. Bounds on the level-one weight also appear in Talagrand's work on correlation of monotone sets (Combinatorica 1996), which the paper compares against (its Theorem 18), and the level-one inequality is a standard chapter of the analysis of Boolean functions (O'Donnell 2014).

Setting

Points of the discrete cube $\{-1,1\}^n$ are sign vectors $x=(x_1,\dots,x_n)$; following the paper, the bit TRUE is read as $-1$ and FALSE as $1$. The cube carries the uniform probability measure, so $\mathbf E[g]=2^{-n}\sum_x g(x)$, and real functions form an inner product space with $\langle f,g\rangle=\mathbf E[fg]$.

For $S\subseteq[n]$ the parity $\chi_S(x)=\prod_{i\in S}x_i$; the parities form an orthonormal basis, and the Fourier coefficient of $f$ at $S$ is $\hat f(S)=\langle f,\chi_S\rangle$. The weight of $f$ at level 1 is

$$W^1(f)=\sum_{|S|=1}\hat f(S)^2=\sum_{i=1}^n\hat f(\{i\})^2 .$$

The influence of coordinate $i$ on $f$ (Definition 2) is

$$\mathrm{Inf}_i(f)=\mathop{\mathbf E}_{x_1,\dots,x_{i-1},x_{i+1},\dots,x_n}\big[\mathrm{Var}_{x_i}[f]\big],$$

the expected variance of $f$ when all coordinates but $x_i$ are fixed at random and $x_i$ is a uniform sign. The linear part of $f$ is $\ell(x)=\sum_i\hat f(\{i\})x_i$, and $\|g\|_1=\mathbf E|g|$, $\|g\|_2=\sqrt{\mathbf E[g^2]}$, $\|g\|_\infty=\max_x|g(x)|$.

Throughout, $C=2\big(1-\sqrt{2/\pi}\big)\approx 0.404$.

Formalization targets

Goal: Theorem 6 (p. 12)

For every $n$, every $f:\{-1,1\}^n\to[-1,1]$ and every $\delta\ge 0$ with $\mathrm{Inf}_i(f)\le\delta$ for all $i$,

$$\sum_{|S|=1}\hat f(S)^2\;\le\;\frac{2}{\pi}+C\delta .$$

The constant $C$ is explicit, and the goal states it exactly as printed.

Milestones (proof of Theorem 6, p. 25, and Proposition 7.2, p. 16)

1. For $f$ with values in $[-1,1]$: $\sum_{|S|=1}\hat f(S)^2=\|\ell\|_2^2=\langle f,\ell\rangle\le\|f\|_\infty\|\ell\|_1\le\|\ell\|_1$.
2. The König–Schütt–Tomczak-Jaegermann bound: if $|a_i|\le\delta$ for all $i$ and $\ell=\sum_i a_ix_i$, then

$$\|\ell\|_1\le\sqrt{2/\pi}\,\|\ell\|_2+\tfrac C2\,\delta .$$

3. The quadratic step: for $X,\delta\ge0$, $X^2\le\sqrt{2/\pi}\,X+\tfrac C2\delta$ implies $X\le\sqrt{1/2\pi}+\sqrt{1/2\pi+C\delta/2}$ and $X^2\le 2/\pi+C\delta$.
4. Proposition 7.2: $\mathrm{Inf}_i(f)=\sum_{S\ni i}\hat f(S)^2$.

Significance

The result. The constant $2/\pi$ is sharp: majority on $n$ variables has influences of order $n^{-1/2}$ and level-one weight tending to $2/\pi$, which is $(\mathbf E|Z|)^2$ for a standard Gaussian $Z$. Theorem 6 thus identifies the extremal level-one weight of low-influence bounded functions and gives a rate linear in the maximal influence. It is the $\rho\to0$ instance of Majority Is Stablest, obtained without the invariance principle, and level-one bounds of this type are used in hardness reductions and in the study of noise sensitivity.

Formalizing it. The milestones together give a complete formal route from bounded functions to the stated bound, except for one step discussed below. They also produce a reusable layer of Boolean Fourier analysis: Fourier coefficients, level weights, influences in their variance form and the Fourier formula for influences. Mathlib contains no development of influences or level weights on the cube, and the platform has none either; the König–Schütt–Tomczak-Jaegermann inequality, a sharp quantitative central limit bound for Rademacher sums (J. Reine Angew. Math. 1999), has no machine-checked proof.

Status. The published proof's first step, $|\hat f(\{i\})|\le\mathrm{Inf}_i(f)$, is valid for Boolean-valued $f$ but not for $[-1,1]$-valued $f$; for $[-1,1]$-valued $f$ the statement is posed as printed. For $f=c\,x_1$ with $0<c<1$ one has $\hat f(\{1\})=c>c^2=\mathrm{Inf}_1(f)$, and the argument as written then yields only $2/\pi+C\sqrt\delta$. Numerical search over small cubes has found no function violating the printed bound. A proof of the goal for bounded $f$, or a counterexample, is therefore a genuine contribution.

Difficulty

The obvious argument replaces $\ell$ by a Gaussian with the same variance and uses $\mathbf E|Z|=\sqrt{2/\pi}$. A central limit theorem with an error term is needed, and generic Berry–Esseen bounds give an additive error with a constant far from $C/2$; the exact constant $1-\sqrt{2/\pi}$ requires the sharp Rademacher-sum inequality, whose proof is a delicate analysis of $\mathbf E|\sum_ia_ix_i|$ as a function of the coefficients. The second obstacle is the passage from influences to coefficients. For bounded $f$ only $\hat f(\{i\})^2\le\mathrm{Inf}_i(f)$ holds, so a bound on influences controls coefficients only at scale $\sqrt\delta$; feeding that into the chain loses the linear dependence on $\delta$. Recovering the printed rate for non-Boolean $f$ needs an idea beyond the published proof.

Formalization scope

A point of the cube is Fin n → Bool, mapped to a sign by pm with pm true = -1 and pm false = 1. Expectations are normalised finite sums, so no measure theory is involved. A function $f:\{-1,1\}^n\to[-1,1]$ is a real function with the hypothesis ∀ x, |f x| ≤ 1. The influence is defined as on the page, as the average over the cube of $\big((f(x^{i\leftarrow1})-f(x^{i\leftarrow-1}))/2\big)^2$, which is the variance in $x_i$; it is not defined by its Fourier formula, which is a milestone. The level-one weight is $\sum_i\hat f(\{i\})^2$. The constant $C$ is written out as 2 * (1 - Real.sqrt (2 / Real.pi)); an existentially quantified constant would be a weaker theorem. The case $n=0$ is allowed.

Two hypotheses are added and disclosed: $\delta\ge0$ in Theorem 6 and in the König–Schütt–Tomczak-Jaegermann bound. For $n\ge1$ each follows from the other hypotheses; for $n=0$ the influence (resp. coefficient) hypothesis is empty and $\delta\ge0$ is what the page assumes.

A trivializing formalization would drop the range hypothesis (then scaled dictators refute the bound and the statement is false), define influence through Fourier coefficients (which makes Proposition 7.2 definitional), or weaken the hypothesis of the goal to a bound on the coefficients $|\hat f(\{i\})|\le\delta$; none of these is used here. In particular, the goal is not strengthened to Boolean-valued $f$, where the published proof applies verbatim.

Contributions welcome: proofs of Parseval-type identities for the linear part, of Proposition 7.2, of the elementary quadratic step, of the König–Schütt–Tomczak-Jaegermann inequality, and of the goal itself. The cube layer is reusable for any later formalization of Boolean function analysis.

Selected references

• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal Inapproximability Results for MAX-CUT and Other 2-Variable CSPs?, SIAM J. Comput. 37(1), 2007. https://doi.org/10.1137/S0097539705447372
• E. Mossel, R. O'Donnell, K. Oleszkiewicz, Noise stability of functions with low influences: invariance and optimality, Annals of Mathematics 171(1), 2010. https://doi.org/10.4007/annals.2010.171.295
• H. König, C. Schütt, N. Tomczak-Jaegermann, Projection constants of symmetric spaces and variants of Khintchine's inequality, J. Reine Angew. Math. 511, 1999. https://doi.org/10.1515/crll.1999.511.1
• M. Talagrand, How much are increasing sets positively correlated?, Combinatorica 16(2), 1996. https://doi.org/10.1007/BF01844850
• R. O'Donnell, Analysis of Boolean Functions, Cambridge University Press, 2014. https://arxiv.org/abs/2105.10386

Motivation

Regev's paper (J. ACM 56(6), Article 34, 2009) introduces the learning with errors (LWE) problem and shows that solving it is at least as hard, for quantum algorithms, as approximating standard worst-case lattice problems such as the shortest independent vectors problem (SIVP) and GapSVP. LWE is the basis of most lattice-based public-key cryptography, including the post-quantum schemes standardized since.

The reduction runs through a sampling problem: produce samples of the discrete Gaussian distribution $D_{L,r}$ on a lattice $L$. The last step converts such a sampler into a solver for SIVP, which asks for $n$ short linearly independent lattice vectors. That conversion rests on one geometric fact about $D_{L,r}$, Lemma 3.15 of the paper (p. 34:31): when the width $r$ is at least $\sqrt2$ times the smoothing parameter of $L$, a sample is not trapped in any proper subspace. The lemma first appeared, with only a proof sketch, in the preliminary version of Micciancio and Regev's work on worst-case to average-case reductions (SIAM J. Comput. 2007); Regev's article gives the full proof. This mission formalizes that lemma. The paper's main theorem, a quantum reduction (Theorem 3.1), is outside this series.

Setting

Work in $\mathbb{R}^n$, $n \ge 1$, with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$.

• A lattice $L \subset \mathbb{R}^n$ is the set of integer combinations of $n$ linearly independent vectors. Its dual is $L^* = \{y \in \mathbb{R}^n : \langle x, y\rangle \in \mathbb{Z}\ \forall x \in L\}$, and $\det(L)$ is the volume of a fundamental domain; $\det(L^*) = 1/\det(L)$.
• The Gaussian function of width $s > 0$ is $\rho_s(x) = \exp(-\pi\|x\|^2/s^2)$ (Eq. (4)); for a countable set $A$, $\rho_s(A) = \sum_{x \in A}\rho_s(x)$.
• The discrete Gaussian $D_{L,r}$ is the probability distribution on $L$ with mass $D_{L,r}(x) = \rho_r(x)/\rho_r(L)$ (Eq. (6)).
• For $\epsilon > 0$, the smoothing parameter $\eta_\epsilon(L)$ is the smallest $s > 0$ with $\rho_{1/s}(L^* \setminus \{0\}) \le \epsilon$ (Definition 2.10, p. 34:19).
• A subspace $H$ is a real linear subspace of $\mathbb{R}^n$; "dimension at most $n-1$" means $H$ is proper.

Formalization targets

Goal: Lemma 3.15 (p. 34:31)

For an $n$-dimensional lattice $L$, $0 < \epsilon \le \tfrac1{10}$, $r \ge \sqrt2\,\eta_\epsilon(L)$ and every subspace $H$ with $\dim H \le n - 1$,

$$\Pr_{x \sim D_{L,r}}[x \notin H] = \sum_{x \in L \setminus H} \frac{\rho_r(x)}{\rho_r(L)} \;\ge\; \frac{1}{10}.$$

The constants $\sqrt2$, $\tfrac1{10}$ and $\tfrac1{10}$ are the printed ones.

Milestones, in attack order

1. Lemma 2.14 (Poisson summation, p. 34:20), already proved on the platform: $f(L) = \det(L^*)\hat f(L^*)$, with $\hat f(w) = \int f(x)e^{-2\pi i\langle x, w\rangle}dx$.
2. The remark after Definition 2.10 (p. 34:19): $s \mapsto \rho_{1/s}(L^* \setminus \{0\})$ is continuous and strictly decreasing on $(0,\infty)$, tends to $\infty$ at $0$ and to $0$ at $\infty$, and $\epsilon \mapsto \eta_\epsilon(L)$ is its inverse.
3. The expectation chain (proof of Lemma 3.15, p. 34:31): for a unit vector $w$,

$$\mathop{\mathrm{Exp}}_{x\sim D_{L,r}}\bigl[e^{-\pi\langle w,x\rangle^2/r^2}\bigr] = \frac{\det(L^*)r^n}{\sqrt2\,\rho_r(L)}\sum_{y\in L^*}e^{-\pi r^2(\|y\|^2 - \langle w,y\rangle^2/2)} \le \frac{\det(L^*)r^n}{\sqrt2\,\rho_r(L)}\rho_{\sqrt2/r}(L^*) \le \frac{\det(L^*)r^n}{\sqrt2\,\rho_r(L)}(1+\epsilon).$$

4. The normalization bound (p. 34:31): $\rho_r(L) = \det(L^*)r^n\rho_{1/r}(L^*) \ge \det(L^*)r^n$ for every $r > 0$.
5. The conclusion of the proof (p. 34:31): the expectation is at most $\tfrac1{\sqrt2}(1+\epsilon) < 0.9$.

Significance

The result. Lemma 3.15 gives Corollary 3.16: $n^2$ independent samples of $D_{L,r}$ contain $n$ linearly independent vectors except with exponentially small probability. Since samples of $D_{L,r}$ have norm at most about $\sqrt n\, r$ with high probability, a sampler at width $r \approx \sqrt2\,\eta_\epsilon(L)$ therefore yields short independent vectors, which is how Regev's reduction reaches SIVP (§3.3). The same property is used in later work wherever discrete Gaussian samples must generate a full-rank set of lattice vectors.

Formalizing it. The lemma is proved in the paper; it has no machine-checked proof that we know of. The work this mission asks for is the formalization of the known proof: the Gaussian-sum analysis of a discrete Gaussian on a general lattice in Mathlib's ZLattice framework, built on the platform's proved Poisson summation formula for lattices. The remark after Definition 2.10 (well-definedness of the smoothing parameter) and the normalization bound $\rho_r(L) \ge \det(L^*)r^n$ are used across the whole paper (Lemmas 3.2, 3.12, Claims 3.8, 3.9) and are reusable beyond this mission.

Difficulty

The obvious argument fails at the first step: there is no direct way to bound the mass of $D_{L,r}$ on a hyperplane, because a lattice can place many short vectors in one hyperplane and the normalization $\rho_r(L)$ is not known in closed form. The paper's route replaces the indicator of $H$ by a Gaussian in the direction orthogonal to $H$ and moves to the dual lattice, where the smoothing hypothesis controls the sum. Formally this requires Poisson summation for an anisotropic Gaussian (a Gaussian with a non-scalar covariance), i.e. the Fourier transform of $x \mapsto \exp(-\pi(\|x\|^2 + \langle w,x\rangle^2)/r^2)$, which is not a stated Mathlib lemma, together with summability of Gaussian sums over lattices and the identification of the dual lattice used by the Poisson formula with the one in the paper. The smoothing remark needs continuity and strict monotonicity of a lattice theta series and its limits at $0$ and $\infty$.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure. A lattice is L : Submodule ℤ (EuclideanSpace ℝ (Fin n)) with [DiscreteTopology L] [IsZLattice ℝ L] (discrete, full rank), the same shape as the referenced Poisson summation item. $L^*$ is LinearMap.BilinForm.dualSubmodule (innerₗ _) L; $\det(L^*)$ is written $(\texttt{ZLattice.covolume } L)^{-1}$.
• All Gaussian sums are real tsums over the lattice or its dual; they are summable, so the values are the true sums. $D_{L,r}$ is a mass function on the points of $L$, and the probability of $x \notin H$ is the sum of the masses of the lattice points outside $H$.
• $\eta_\epsilon(L)$ is the real infimum of $\{s > 0 : \rho_{1/s}(L^* \setminus \{0\}) \le \epsilon\}$; that it is attained is milestone 2, not a definitional shortcut.
• Added hypotheses, all disclosed in the items: $n \ge 1$ in the goal (at $n = 0$ the natural-number subtraction $n - 1$ is $0$, the only subspace of dimension $0$ is the whole space $\mathbb{R}^0$, and the probability is $0$); $\epsilon > 0$ (Definition 2.10 is for $\epsilon > 0$; for $\epsilon \le 0$ the Lean infimum is over the empty set, equals $0$, and the hypothesis $r \ge \sqrt2\,\eta_\epsilon(L)$ would be vacuous); $r > 0$ (a Gaussian width; for $n \ge 1$ it follows from the other hypotheses).
• Rotation. The proof's "assume without loss of generality that $(1,0,\dots,0)$ is orthogonal to $H$" is formalized coordinate-free: milestones 3 and 5 are stated for an arbitrary unit vector $w$, with $x_1$ replaced by $\langle w, x\rangle$.
• Lemma 2.14 is printed "for any function $f$", the technical conditions omitted (p. 34:20). The referenced platform item states it for Schwartz functions $f$, in translated form; every function the proof applies it to is a Gaussian, hence Schwartz.
• Not a trivializing formalization: the probability is not stated through a Bochner integral or an unconstrained tsum, the smoothing hypothesis is not vacuous ($\epsilon > 0$), and the goal is the probability bound, not the expectation bound of milestone 3.
• Contributions welcome: Fourier transforms of anisotropic Gaussians on EuclideanSpace, summability and monotonicity of lattice theta series, and the smoothing remark, each reusable in the sibling missions of this series.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• D. Micciancio and O. Regev, Worst-Case to Average-Case Reductions Based on Gaussian Measures, SIAM Journal on Computing 37(1), 2007. https://doi.org/10.1137/S0097539705447360