Motivation

The source defines a two-variable integral on strictly positive-definite real matrices. Its numerator is the absolute bilinear form of A minus B on two unit vectors, while the denominator uses the quadratic forms of A and B. The desired inequality says that componentwise matrix addition is nonexpansive for this quantity, with the larger of the two input distances controlling the output. The surface measure normalization is immaterial because the same constant multiplies every distance.

This mission turns CUHK-Shenzhen AI Math Problem 1, Positive definite matrix integral inequality, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

For every positive dimension and every four positive-definite matrices A, B, C, and D, prove d(A+B,C+D) is at most max(d(A,C),d(B,D)). The first milestone fixes dimension one, where the sphere and every matrix entry can be analyzed explicitly.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in matrix analysis, positive definite matrices, integral inequality. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.

Difficulty

The absolute value prevents a direct cancellation argument, and the denominators couple each integration variable to a different matrix. Positive definiteness gives pointwise positivity but does not immediately compare the ratios after addition. A successful proof must find a convexity, change-of-measure, or projective-metric mechanism that survives the double integral.

Suggested attack route

Promising routes include reducing by congruence to normalized matrices, studying the scalar inequality on each pair of directions, and interpreting the denominator as a density change on the sphere. The dimension-one case should reveal the sharp scalar inequality. Numerical experiments in dimensions two and three may identify equality cases, but the Lean proof must ultimately derive every bound from positivity and measurable integration.

Formalization scope

The Lean model uses finite matrices, Mathlib positive definiteness, the canonical sphere measure obtained from polar decomposition, and an explicit iterated integral. It does not assume symmetry through an unchecked flag: positive definiteness is the Mathlib predicate. Integrability obligations and zero-denominator issues must be proved from positive definiteness.

The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.

Milestones

Establish the dimension-one specialization, including any exact evaluation of the two-point sphere integral needed by the proof.

The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.

Timeline and literature status

The CUHK-Shenzhen AI Math Problems page added this problem on May 28, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

• Original CUHK-Shenzhen problem

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.

Why smooth-region boundary diffusions matter

Diffusion models in a bounded region need a rule for what happens when a path reaches the boundary. Two standard mechanisms are absorption, where the boundary kills the generator contribution, and oblique reflection, where a prescribed vector field pushes the process back into the region. Ethier and Kurtz treat these mechanisms as neighboring variants of the same uniformly elliptic model in Chapter 8, Section 1 of Markov Processes: Characterization and Convergence. The distinction is structural: the interior differential operator is shared, but its admissible generator graph changes with the boundary condition. This mission formalizes Theorems 1.4 and 1.5, retaining oblique reflection as the capstone and absorbed diffusion as the required related result.

The setting

Let $\Omega\subset\mathbb R^d$ be bounded, open, and connected, with $d\ge 2$. Its boundary is locally represented in orthogonal coordinates as the graph of a scalar function. The formal predicate C²,μ boundary regularity requires one positive chart radius valid at every boundary point, a connected local boundary patch, and a graphing function whose second partial derivatives satisfy the source's componentwise Hölder oscillation condition. The exponent obeys $0<\mu\le 1$.

The diffusion coefficients are a symmetric positive-semidefinite matrix field $a(x)$ and a drift field $b(x)$. Their entries satisfy the same local componentwise Hölder convention. Uniform ellipticity means that one $\varepsilon>0$ satisfies

$$\varepsilon\le \sum_{i,j}\theta_i a_{ij}(x)\theta_j$$

for every $x\in\Omega$ and every unit vector $\theta$. For smooth $f$, the interior operator is

$$Gf(x)=\frac12\sum_{i,j}a_{ij}(x)\,\partial_{ij}f(x) +Df(x)[b(x)].$$

Functions live on the compact closure $\overline\Omega$ as bounded continuous functions. Their ambient extensions are differentiated only at interior points. The second coordinate of each graph is itself continuous on the closure, so it records the boundary trace of $Gf$ rather than assigning an arbitrary value after differentiation.

Formalization targets

Goal: obliquely reflected diffusion generation

Theorem 1.5 adds a reflection field $c$ whose components have C¹,μ boundary regularity. An outward unit normal $n(x)$ is oriented by a local defining function that is negative precisely inside $\Omega$. Uniform obliqueness is the global lower bound

$$\varepsilon\le c(x)\cdot n(x),\qquad x\in\partial\Omega,$$

for one positive $\varepsilon$. The reflected graph requires a continuous derivative trace $J$ that agrees with $Df$ in the interior and satisfies

$$J_x(c(x))=0,\qquad x\in\partial\Omega.$$

The target asserts that the uniform closure of this graph is single-valued and is exactly the full generator of a positive strongly continuous contraction semigroup preserving the constant function one. The generator condition is a biconditional derivative limit, so it identifies the complete domain rather than only a convenient operator restriction.

Related target: absorbed diffusion generation

Theorem 1.4 keeps the same smooth-region and ellipticity assumptions but uses the absorbed graph. Its continuous operator trace satisfies $Gf=0$ on the boundary. It has the same full generation conclusion: graph single-valuedness, a positive strongly continuous contraction semigroup, preservation of one, and exact identification of the generator. The absorbed zero trace is not imported into the reflected theorem, and the oblique derivative condition is not imposed on the absorbed graph.

Significance

These results connect a local elliptic expression and a geometric boundary condition to a global Markov evolution on continuous functions over the closed region. The conclusions contain more than existence of a semigroup: they determine the whole infinitesimal generator, ensure positivity and contraction, and retain the conservative convention used by Ethier and Kurtz. The paired statements make the effect of the boundary mechanism explicit while holding the interior model fixed.

The formal contribution is a machine-checkable statement layer, not a proof of the source theorems. It records the componentwise Hölder convention, uniform boundary charts, ellipticity, normal orientation, continuous derivative trace, the two distinct generator graphs, and every semigroup clause. These definitions can support later work on reflected processes, elliptic boundary problems, and martingale formulations without rebuilding the geometric conventions.

Where the difficulty lies

The main difficulty is simultaneous control of interior regularity, boundary geometry, and the closed generator domain. Pointwise obliqueness is insufficient: the source requires a uniform positive lower bound over the whole compact boundary. Likewise, merely writing $Df(c)=0$ for an arbitrary ambient extension would not supply a well-defined boundary derivative. The graph therefore carries a continuous derivative trace agreeing with the interior derivative. Replacing the biconditional generator equality by a one-way inclusion, or silently imposing the absorbed zero trace on the reflected graph, would weaken or change the source result.

Formalization scope and conventions

The state space is EuclideanSpace ℝ (Fin (n + 1)) with 2 ≤ n + 1. Connectedness supplies nonemptiness. Matrix positive semidefiniteness supplies symmetry and nonnegative quadratic forms; a separate hypothesis gives strict uniform ellipticity. Local oscillation bounds apply within connected components of small intersections and do not compare different components.

The absorbed and reflected graphs use bounded continuous functions on closure Ω. The arbitrary zero extension outside the closure is never differentiated at a boundary point. The reflected boundary equation uses a continuous field of linear derivative maps, while the absorbed equation uses the continuous second graph coordinate. No vacuous region, pointwise-only ellipticity or obliqueness, weakened generator inclusion, proof-only theorem dependency, or synthetic theorem combining the two boundary mechanisms is admitted.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Section 1, Theorems 1.4–1.5 and equations (1.13)–(1.20). Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 1 for strongly continuous contraction semigroups and generators, and Chapter 4 for the conservative Feller convention. Wiley DOI

Motivation

Linear Cauchy–Riemann operators are the linearizations of the nonlinear Cauchy–Riemann equation for pseudoholomorphic curves. On the cylinder $\mathbb{R}\times S^1$ with the trivial bundle they take the form

$$D_S=\partial_s+J_0\,\partial_t+S(s,t):W^{1,p}(\mathbb{R}\times S^1,\mathbb{R}^{2n})\to L^p(\mathbb{R}\times S^1,\mathbb{R}^{2n}),$$

where $S(s,\cdot)$ converges to loops $S^\pm$ of symmetric matrices as $s\to\pm\infty$. These are the operators of Floer homology, of symplectic field theory and of contact homology. The dimension of their moduli spaces is the Fredholm index of $D_S$, and the Riemann–Roch formula with punctures computes it from the Conley–Zehnder indices of the asymptotic operators $A^\pm=-J_0\partial_t-S^\pm(t)$:

$$\operatorname{ind}D_S=\mu_{CZ}(A^+)-\mu_{CZ}(A^-).$$

This mission formalizes this formula, together with the Fredholm property of $D_S$, following C. Wendl, Lectures on Symplectic Field Theory, Lectures 3–5, in the case of the cylinder (the sphere with one positive and one negative puncture). Mathlib has the notion of a Fredholm operator but no Sobolev spaces on cylinders, no Cauchy–Riemann operators and no Conley–Zehnder index.

Setting

• Cylinder. $S^1=\mathbb{R}/\mathbb{Z}$. Maps on $\mathbb{R}\times S^1$ are maps $u(s,t)$ on $\mathbb{R}^2$ with $u(s,t+1)=u(s,t)$, and $L^p(\mathbb{R}\times S^1)$ is $L^p$ of the strip $\mathbb{R}\times[0,1)$ with Lebesgue measure. $\mathbb{R}^{2n}=\mathbb{C}^n$ with $J_0=\begin{pmatrix}0&-1\\1&0\end{pmatrix}$, multiplication by $i$.
• Sobolev space. $W^{1,p}(\mathbb{R}\times S^1,\mathbb{R}^{2n})$ is the closure of the smooth maps that vanish for large $|s|$ under the norm $\|u\|_p+\|\partial_su\|_p+\|\partial_tu\|_p$.
• Asymptotic operators. For a loop $S_\infty$ of symmetric matrices, $A=-J_0\partial_t-S_\infty(t)$. Its fundamental solution $\Psi$ solves $\Psi'=J_0S_\infty\Psi$, $\Psi(0)=\mathrm{Id}$. $A$ is nondegenerate if $1$ is not an eigenvalue of $\Psi(1)$, and $\mu_{CZ}(A)$ is the Conley–Zehnder index of the symplectic path $\Psi|_{[0,1]}$.
• Cauchy–Riemann operators. $S:\mathbb{R}\times S^1\to\mathbb{R}^{2n\times2n}$ is continuous and $S(s,\cdot)\to S^\pm$ uniformly as $s\to\pm\infty$. $D_S$ acts on $W^{1,p}$; its index is $\dim\ker D_S-\dim\operatorname{coker}D_S$.

Formalization targets

Goal: the index formula on the cylinder

If $1<p<\infty$ and the asymptotic operators $A^\pm$ are nondegenerate, then $D_S:W^{1,p}\to L^p$ is Fredholm and $\operatorname{ind}D_S=\mu_{CZ}(A^+)-\mu_{CZ}(A^-)$ (Wendl, Theorem 5.4 with Theorem 4.3, for the cylinder).

Milestones

1. Translation-invariant operators. For a nondegenerate loop $S_\infty$, $\partial_s+J_0\partial_t+S_\infty(t):W^{1,p}\to L^p$ is an isomorphism (Theorem 4.11).
2. Global regularity. An $L^p$ weak solution of $D_S\eta=f\in L^p$ lies in $W^{1,p}$ (Proposition 4.6).
3. Local estimate. $\|\eta\|_{W^{1,p}}\le c\|D_S\eta\|_p+c\|\eta\|_p$ for $\eta$ supported in $[-R,R]\times S^1$ (Proposition 4.8).
4. Estimate on the ends. $\|\eta\|_{W^{1,p}}\le c\|D_S\eta\|_p$ for $\eta$ supported far out in an end with nondegenerate asymptotic operator (Proposition 4.9).
5. An abstract estimate. If $\|x\|\le c\|Tx\|+c\|Kx\|$ with $K$ compact, then $\ker T$ is finite-dimensional and $T$ has closed range (Lemma 4.12).
6. Global estimate. $\|\eta\|_{W^{1,p}}\le c\|D_S\eta\|_p+c\|\eta\|_{L^p([-R,R]\times S^1)}$ (Lemma 4.13).
7. Compactness on finite cylinders. Bounded sequences in $W^{1,p}$ have subsequences converging in $L^p([-R,R]\times S^1)$ (Wendl, p. 74).
8. Semi-Fredholm property of $D_S$ (Corollary 4.14).
9. Cokernel and formal adjoint. $\dim\operatorname{coker}D_S$ is finite and equals the kernel dimension of the Cauchy–Riemann operator $D_{\bar S}$ on $W^{1,q}$, $\bar S=-CS^{\mathsf T}C$, $1/p+1/q=1$, with $C$ complex conjugation (Lemma 4.17, Proposition 4.18, Theorem 4.20).
10. Fredholm property of $D_S$ (Theorem 4.3).
11. Independence of $p$ of the kernel dimension and of the index (Theorem 4.3).
12. Classification of nondegenerate asymptotic operators. Two nondegenerate loops have the same Conley–Zehnder index if and only if they are joined by a path of nondegenerate loops (Theorem 3.34).
13. Conjugation. $\mu_{CZ}(-J_0\partial_t+CS_\infty C)=-\mu_{CZ}(-J_0\partial_t-S_\infty)$ (Lemma 5.8).
14. Model operators. $\eta\mapsto-J_0\dot\eta-\pi k\eta-\sigma e^{2\pi ikt}\bar\eta$ on loops in $\mathbb{C}$ is nondegenerate with Conley–Zehnder index $k$, for $k\in\mathbb{Z}$ and $\sigma>0$ (Lemma 5.29).
15. A plane equation without $L^2$ solutions. $\bar\partial f+\bar z\bar f=0$ has no nonzero smooth solution in $L^2(\mathbb{C})$ (Proposition 5.20).
16. A plane equation with Gaussian solutions. The smooth $L^2$ solutions of $\bar\partial f+z\bar f=0$ are the real multiples of $e^{-|z|^2/2}$ (Proposition 5.21).
17. Large antilinear perturbations. For a function $\beta$ on the cylinder with normalized zeros, $D_S+\sigma\beta\bar{\ \cdot\ }$ is onto with kernel of dimension $\#Z^+$ when all zeros are positive, and injective with cokernel of dimension $\#Z^-$ when all zeros are negative, for all large $\sigma$ (Proposition 5.27).
18. Antilinear deformations of asymptotic operators. If each asymptotic operator has the Conley–Zehnder index of an operator $-J_0\partial_t-S'^\pm$ whose deformations $-J_0\partial_t-S'^\pm-\sigma\beta_\pm\bar{\ \cdot\ }$, $\sigma\ge0$, are all nondegenerate, then $\operatorname{ind}D_S=\operatorname{wind}\beta_+-\operatorname{wind}\beta_-$ (Lemma 5.28).

Significance

The result. The index formula is the dimension formula for moduli spaces of pseudoholomorphic cylinders: Floer trajectories in Hamiltonian Floer homology and holomorphic cylinders in symplectizations. It fixes the grading of these theories, and its sign conventions are those of the Conley–Zehnder index of the asymptotic orbits.

Formalizing it. The mission builds Sobolev spaces on the cylinder, the Fredholm theory of Cauchy–Riemann operators with cylindrical ends, and the Conley–Zehnder index of asymptotic operators. These are the analytic foundations of Floer theory and symplectic field theory and are reusable for transversality arguments and for the indices of other operators. Milestone 5 is a general statement about Banach spaces.

Difficulty

The operators act between infinite-dimensional spaces of functions on a non-compact domain, so finiteness of kernel and cokernel is a global statement that sees the behaviour at both ends. The Sobolev space is defined as a closure, and the operator acts on its elements through their weak derivatives. The Conley–Zehnder index is defined through a continuous argument of a normalized complex determinant along a path of symplectic matrices, extended to a normal form; the conventions (sign of $J_0$, orientation of the cylinder, which end is positive) all enter the final formula. Several milestones are uniform estimates in which the constant is chosen before the function.

Formalization scope

• Namespace CauchyRiemannIndex. The definition module CauchyRiemannIndex_Setting defines the cylinder measure, W1p, crKernel, crRange, crIndex, IsFredholmCR, asymptotic operators through IsFundamentalSolution, IsNondegenerate and asymptoticCZIndex, and the Conley–Zehnder index czIndex of a symplectic path. The mission is standalone; czIndex and its auxiliary definitions repeat those of the ConleyZehnder mission word for word.
• Spaces. $\mathbb{R}^{2n}$ is EuclideanSpace ℝ (Fin n ⊕ Fin n), matrices are Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ, and $J_0$ is Matrix.J. Maps on the cylinder are maps ℝ × ℝ → ℝ²ⁿ, periodic in the second variable, and $L^p$ is taken on the strip $\mathbb{R}\times[0,1)$. $W^{1,p}$ is a closed subspace of Lp × Lp × Lp, consisting of triples $(u,\partial_su,\partial_tu)$.
• Exponents. $p$ is in ℝ≥0∞ with $1<p$ and $p\ne\infty$. Norms of smooth maps are eLpNorm in ℝ≥0∞; constants are in ℝ≥0.
• Indices. The Fredholm index is finrank ker - finrank (Lp ⧸ range) in ℤ; statements that use it also assert that both are finite-dimensional.
• Smoothness. Smoothness is ContDiff ℝ ∞ ($C^\infty$, not analytic). The coefficient $S$ is only assumed continuous, with uniform convergence at the ends.

Contributions welcome: general lemmas on Sobolev spaces of periodic functions, on Fredholm operators between Banach spaces, and on the Conley–Zehnder index.

Selected references

• C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lectures 3–5. https://arxiv.org/abs/1612.01009
• J. Gutt, Generalized Conley–Zehnder index, Ann. Fac. Sci. Toulouse Math. (6) 23 (2014), 907–932, arXiv:1307.7239. https://arxiv.org/abs/1307.7239
• D. Salamon, Lectures on Floer homology, in Symplectic Geometry and Topology, IAS/Park City Math. Ser. 7, AMS (1999), 143–229.
• M. Schwarz, Cohomology operations from S¹-cobordisms in Floer homology, PhD thesis, ETH Zürich (1995).

Motivation

In quantum mechanics the spectrum of a Hamiltonian splits into two parts that behave very differently under perturbation. Isolated eigenvalues of finite multiplicity (bound states) move, split or disappear when the operator is changed even slightly; the rest of the spectrum, which carries scattering states and accumulation points of eigenvalues, is far more rigid. Weyl's theorem makes this rigidity precise: if two self-adjoint operators have resolvents that differ by a compact operator, their essential spectra coincide. It is the standard first step in locating the spectrum of a Schrödinger operator $-\Delta + V$: one shows that $V$ is a relatively compact perturbation of $-\Delta$, concludes $\sigma_{ess}(-\Delta + V) = \sigma_{ess}(-\Delta) = [0,\infty)$, and is left with the discrete eigenvalues below zero.

The result goes back to H. Weyl's 1909 work on compact perturbations of bounded self-adjoint operators; the resolvent formulation for unbounded operators is the one used in modern texts such as Reed–Simon (Vol. IV, Sec. XIII.4) and Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), Section 6.4, which this mission follows.

Setting

Let $\mathfrak H$ be a complex Hilbert space and $A$ a linear operator with domain $\mathfrak D(A) \subseteq \mathfrak H$. For $z \in \mathbb C$, the resolvent $R_A(z) = (A - z)^{-1}$ exists when $A - z$ maps $\mathfrak D(A)$ bijectively onto $\mathfrak H$ with a bounded inverse. The resolvent set $\rho(A)$ is the set of such $z$, and the spectrum is $\sigma(A) = \mathbb C \setminus \rho(A)$.

The discrete spectrum $\sigma_d(A)$ is the set of eigenvalues $z$ of $A$ that are isolated points of $\sigma(A)$ and whose eigenspace $\operatorname{Ker}(A - z)$ is finite dimensional. The essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$.

A sequence $\psi_n \in \mathfrak D(A)$ with $\|\psi_n\| = 1$, $\langle \varphi, \psi_n \rangle \to 0$ for every $\varphi$ (weak convergence to zero) and $\|(A - z)\psi_n\| \to 0$ is a singular Weyl sequence for $A$ at $z$.

An operator is compact if it maps bounded sets to relatively compact sets; $\mathfrak C(\mathfrak H)$ denotes the compact operators. An operator $K$ is relatively compact with respect to $A$ if $\mathfrak D(A) \subseteq \mathfrak D(K)$ and $K R_A(z) \in \mathfrak C(\mathfrak H)$ for one $z \in \rho(A)$. $B$ is $A$ bounded if $\mathfrak D(A) \subseteq \mathfrak D(B)$ and $\|B\psi\| \le a\|A\psi\| + b\|\psi\|$ on $\mathfrak D(A)$; the infimum of admissible $a$ is the $A$-bound. A symmetric operator $A$ has defect indices $d_\pm(A) = \dim \operatorname{Ran}(A \pm i)^\perp$.

Formalization targets

Goal: Weyl's theorem (Theorem 6.19)

For self-adjoint $A$ and $B$,

$$\exists\, z \in \rho(A) \cap \rho(B):\ R_A(z) - R_B(z) \in \mathfrak C(\mathfrak H) \quad\Longrightarrow\quad \sigma_{ess}(A) = \sigma_{ess}(B).$$

Milestones

• Weyl criterion (Lemma 6.17). For self-adjoint $A$: $z \in \sigma_{ess}(A)$ if and only if a singular Weyl sequence at $z$ exists; if so, it can be chosen orthonormal.
• Compact perturbations (Lemma 6.18). For self-adjoint $A$ and compact self-adjoint $K$, $\sigma_{ess}(A + K) = \sigma_{ess}(A)$, and

$$\sigma_{ess}(A) = \bigcap_{K \in \mathfrak C(\mathfrak H),\, K^* = K} \sigma(A + K).$$

• Independence of $z$ (Lemma 6.21, first part). If $R_A(z) - R_B(z)$ is compact for one $z \in \rho(A) \cap \rho(B)$, it is compact for all such $z$.
• Self-adjoint extensions (Theorem 6.20). If $A$ is symmetric with $d_+(A) = d_-(A) < \infty$, all self-adjoint extensions of $A$ have the same essential spectrum.
• Relative compactness is infinitesimal (Lemma 6.22). For self-adjoint $A$, a relatively compact $K$ has $A$-bound $0$.
• Stability of relative compactness (Lemma 6.23). If $A$ is self-adjoint, $B$ symmetric with $A$-bound less than one, and $K$ relatively compact with respect to $A$, then $K$ is relatively compact with respect to $A + B$.

Significance

The result. Weyl's theorem reduces the determination of the essential spectrum of a perturbed operator to that of a simpler reference operator. Combined with Lemma 6.22 and the Kato–Rellich theorem, it yields $\sigma_{ess}(A + K) = \sigma_{ess}(A)$ for every relatively compact symmetric $K$; Lemma 6.23 extends this to perturbations of the form $B + K$. These are the inputs to the HVZ theorem for $N$-body systems, to the spectral analysis of one-particle Schrödinger operators with decaying potentials, and, via Theorem 6.20, to the observation that boundary conditions at a limit-circle endpoint do not affect the essential spectrum of a Sturm–Liouville operator. The Weyl criterion is independently useful: it is how points are shown to lie in $\sigma_{ess}$ in concrete examples.

Formalizing it. The results are classical and proved in every text on the subject. None of them is formalized: Mathlib has compact operators and the adjoint of a densely defined LinearPMap, but no resolvent set or spectrum for unbounded operators, no discrete or essential spectrum and no relative compactness. This mission asks for formal proofs of Teschl's statements and, with them, a reusable layer of definitions (resolvent of a LinearPMap, $\sigma_d$, $\sigma_{ess}$, singular Weyl sequences, relative compactness) on which later chapters (free Schrödinger operator, HVZ theorem) can build.

Difficulty

The obvious route to all of these statements goes through the spectral theorem: Teschl's proof of the Weyl criterion uses spectral projections $P_A((\lambda - \varepsilon, \lambda + \varepsilon))$ and spectral measures $\mu_{\psi_n}$, and his characterization (6.27)–(6.28) of $\sigma_{ess}$ by ranks of spectral projections presupposes the functional calculus. Mathlib has no spectral theorem for unbounded self-adjoint operators, so this route requires either building it or finding arguments that avoid it. The definition of $\sigma_{ess}$ used here is deliberately the PVM-free one of p. 145, which makes the statements expressible now but moves the difficulty into the proofs: showing that a point of $\sigma(A) \setminus \sigma_d(A)$ carries a singular Weyl sequence requires controlling approximate eigenvectors near a non-isolated spectral point or an eigenvalue of infinite multiplicity without projections.

A second difficulty is domain bookkeeping. $A + K$, $A + B$, $K R_A(z)$ and $R_{A+B}(z)$ all involve unbounded operators with different domains, and identities such as the second resolvent formula $K R_{A+B}(z) = K R_A(z)(\mathbb I - B R_{A+B}(z))$ must be established on the correct domains. Theorem 6.20 requires relating the resolvents of two self-adjoint extensions through the finite-dimensional defect spaces.

Formalization scope

The Hilbert space is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since no statement of the section needs it. Unbounded operators are Mathlib LinearPMaps H →ₗ.[ℂ] H, self-adjointness is Mathlib's IsSelfAdjoint (which implies a dense domain), and symmetric operators are densely defined by definition, as in the book. The resolvent is the bounded two-sided inverse of $A - z$ of p. 73 (IsResolventAt), and $\rho(A)$, $\sigma(A)$ are defined from it; Mathlib's Banach-algebra spectrum is not used. "For one $z \in \rho(A) \cap \rho(B)$" is an existential over $z$ and the two resolvents. Compactness is Mathlib's IsCompactOperator, which on a Hilbert space agrees with the book's norm closure of finite rank operators. $A + K$ for bounded $K$ is K +ᵥ A (domain $\mathfrak D(A)$); $A + B$ for unbounded $B$ is the LinearPMap sum with domain $\mathfrak D(A) \cap \mathfrak D(B)$. The $A$-bound is valued in $[0,\infty]$ and is $\infty$ for an operator that is not $A$ bounded. The defect indices are "equal and finite" when both defect spaces are finite dimensional with equal finrank.

No projection-valued measure or functional calculus is taken as data, and none is needed: every statement is phrased without $f(A)$. For this reason the second half of Lemma 6.21, $f(A) - f(B) \in \mathfrak C(\mathfrak H)$ for $f \in C_\infty(\mathbb R)$, and the form-compactness results Lemma 6.26 and Corollary 6.27 of Section 6.5 are not part of the mission.

A trivializing formalization is ruled out: the discrete spectrum requires all three of "eigenvalue", "isolated in $\sigma(A)$" and "finite-dimensional eigenspace", so $\sigma_{ess}$ is neither empty nor all of $\sigma(A)$ by definition, and the resolvent hypothesis of Weyl's theorem is an existential over genuine resolvents, never a junk value outside $\rho(A)$.

A complete development needs the resolvent identities for LinearPMaps, the relation between self-adjointness and real spectrum, weak convergence of bounded sequences, and the fact that compact operators map weakly null sequences to norm-null ones. The definitions of resolvent, $\sigma_{ess}$, relative compactness and $A$-bound are shared with other chapters of this series and are intended for reuse. Contributions of general lemmas on LinearPMap resolvents are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Section 6.4. https://doi.org/10.1090/gsm/099
• H. Weyl, Über beschränkte quadratische Formen, deren Differenz vollstetig ist, Rendiconti del Circolo Matematico di Palermo 27 (1909), 373–392. https://doi.org/10.1007/BF03019655
• M. Reed and B. Simon, Methods of Modern Mathematical Physics IV: Analysis of Operators, Academic Press, 1978, Section XIII.4.
• T. Kato, Perturbation Theory for Linear Operators, 2nd ed., Springer, 1980, Section IV.5. https://doi.org/10.1007/978-3-642-66282-9

Motivation

Given a real matrix $A=(a_{ij})\in\mathbb R^{m\times n}$, consider maximizing the bilinear form $\sum_{i,j}a_{ij}x_iy_j$ over sign vectors $x\in\{\pm1\}^m$, $y\in\{\pm1\}^n$. This discrete optimum, written $\mathrm{OPT}(A)$, is closely tied to the cut norm of a matrix and is NP-hard to compute. Relaxing each sign to a unit vector and each product to an inner product gives the semidefinite value $\mathrm{SDP}(A)$, computable in polynomial time. Grothendieck's inequality (Grothendieck, 1953) states that the relaxation overshoots by at most a universal factor: there is a finite $K$, independent of $A$, of $m,n$, and of the dimension of the vectors, with $\mathrm{SDP}(A)\le K\cdot\mathrm{OPT}(A)$ for every $A$. The Grothendieck constant $K_G$ is the least such $K$ — equivalently, the worst-case integrality gap of the canonical semidefinite relaxation of this bilinear problem.

The constant is not a curiosity of one optimization problem. It originated in functional analysis, where it is central to the geometry of Banach spaces and to harmonic analysis; it governs the approximation ratio available for cut norms; and, in quantum information, it measures the maximal advantage of quantum over classical correlations in Bell-type experiments. Its exact value has been open since 1953.

A timeline of the bounds:

• 1953, Grothendieck. Existence of a finite $K$, together with the lower bound $K_G\ge\pi/2=1.5707\ldots$
• 1977, Krivine. $K_G\le\pi/\bigl(2\log(1+\sqrt2)\bigr)=1.7822\ldots$, obtained by analyzing hyperplane rounding, and conjectured to be optimal.
• 1984/1991, Davie and Reeds (independently). $K_G\ge1.6769\ldots$, from an explicit high-dimensional Gaussian hard instance.
• 2011, Braverman–Makarychev–Makarychev–Naor. Krivine's conjecture is false: $K_G<\pi/(2\log(1+\sqrt2))$ strictly, with no quantitative gap.
• 2014, Naor–Regev. Mixtures of Krivine schemes are asymptotically optimal: rounding schemes of this one family approach the true value of $K_G$.
• 2026, Heilman; Jones–Malavolta. The first improvements on Davie–Reeds, by $10^{-26}$ and $10^{-12}$ respectively; and the first explicit numerical improvements on Krivine's bound, of order $10^{-5}$ (Heilman; Li–Saha–Xue et al.).
• 2026, Saha–Li–Xue–Chaudhuri–Klivans–Kothari–Meka. The bounds this mission targets:

$$\frac{6\pi}{11}\ \le\ K_G\ \le\ \frac{\pi}{2\log(1+\sqrt2)}-3.47\times10^{-4},$$

i.e. $1.7135\ldots\le K_G\le1.7818\ldots$, which fixes the tenths digit of $K_G$ at $7$.

Setting

Fix $m,n\in\mathbb N$ and $A\in\mathbb R^{m\times n}$.

$$\mathrm{OPT}(A):=\max_{x\in\{\pm1\}^m,\;y\in\{\pm1\}^n}\sum_{i,j}a_{ij}x_iy_j,\qquad \mathrm{SDP}(A):=\sup_{d\in\mathbb N}\ \sup_{u_i,v_j\in S^{d-1}}\sum_{i,j}a_{ij}\langle u_i,v_j\rangle .$$

Here $u_1,\dots,u_m$ and $v_1,\dots,v_n$ are unit vectors of a common but arbitrary finite dimension $d$. Since a sign is a unit vector in dimension one, $\mathrm{OPT}(A)\le\mathrm{SDP}(A)$. Call $K$ a Grothendieck bound if $\mathrm{SDP}(A)\le K\cdot\mathrm{OPT}(A)$ for every $m$, $n$ and $A$, and set $K_G:=\inf\{K: K\text{ is a Grothendieck bound}\}$.

Upper bounds on $K_G$ come from rounding algorithms. A Krivine scheme of dimension $k$ is a pair of partitions of $\mathbb R^k$ into a $+1$ region and a $-1$ region, encoded by measurable odd functions $f,g:\mathbb R^k\to\{\pm1\}$: the algorithm maps each SDP vector to a Gaussian point in $\mathbb R^k$, correlated according to the inner products, and reads off the label of the region the point lands in. Taking $f=g=\operatorname{sgn}(z_1)$ recovers random hyperplane rounding. The quality of a scheme is carried by its normalized correlation function

$$H(t):=\frac{\pi}{2}\,\mathbb E\bigl[f(X)g(Y)\bigr],$$

where $X,Y$ are standard Gaussian vectors in $\mathbb R^k$ with $\mathbb E[X_iY_i]=t$ for every coordinate $i$. For the half-space partition $H(t)=\arcsin t$, whose analysis gives Krivine's bound. Writing the odd expansion $H(t)=b_1t+b_3t^3+\cdots$, the hyperplane scheme sits at $(b_1,b_3)=(1,\tfrac16)$.

Formalization targets

Goal

$$\frac{6\pi}{11}\ \le\ K_G\ \le\ \frac{\pi}{2\log(1+\sqrt2)}-3.47\times10^{-4}$$

This is the two-sided bound the source paper states as the outcome of its Theorems 2.1 and 2.2. It is the weakest statement that carries both of the paper's contributions at once; each side is also a milestone in its own right, so partial progress is recorded even if only one direction closes.

Milestones

The milestone list runs from the classical background to the two new bounds: $\mathrm{OPT}\le\mathrm{SDP}$; the existence of a finite Grothendieck bound; $K_G\ge\pi/2$; Krivine's $K_G\le\pi/(2\log(1+\sqrt2))$; the affine coefficient constraint $b_3\ge2b_1-\tfrac{11}{6}$ valid for every Krivine scheme (Theorem 2.2, equation (1)); the transfer of a member of the affine family into a lower bound on $K_G$ (Appendix A); the lower bound $K_G\ge6\pi/11$ (Theorem 2.2); and the cubic–quintic upper bound (Theorem 2.1).

Significance

The two target bounds narrow an interval that had been essentially static for four decades: before 2026 the state of the art was $1.6769\ldots\le K_G\le1.7822\ldots$, wide enough that the tenths digit was unknown. The lower bound is also methodologically new. Every previous lower bound was obtained by exhibiting a hard instance; this one instead proves a ceiling on the performance of every rounding scheme in the Krivine family and converts that ceiling, through the Naor–Regev optimality theorem, into a bound on the constant. The affine constraint $b_3\ge2b_1-\tfrac{11}{6}$ is the transportable core of that argument: being affine in the coefficients, it survives mixing schemes and passing to limits, which is exactly what the reduction to $K_G$ requires.

On the formalization side, nothing here is machine-checked today. The upper bound (Theorem 2.1) is certified by interval arithmetic in the companion paper, and the lower bound's central one-dimensional inequality likewise rests on a computer-assisted certificate; reproducing either inside Lean means building a rigorous numeric layer on top of the analytic argument. Ahead of that, the mission needs a formal definition of $K_G$ itself and of the Krivine-scheme apparatus, neither of which exists in Mathlib — these are reusable well beyond this mission, since Grothendieck's inequality feeds cut-norm approximation and Bell-inequality bounds. Contributions of intermediate lemmas about $\mathrm{OPT}$, $\mathrm{SDP}$, Gaussian correlation identities, and Hermite expansions are welcome even when the headline bounds stay open.

Difficulty

The obvious route to a lower bound is to write down a matrix and compute. That route is what Davie and Reeds exhausted; improving it has produced gains of order $10^{-12}$ at best, because the hard instances are high-dimensional Gaussian objects whose $\mathrm{OPT}$ is itself hard to bound tightly. The route taken here avoids instances entirely, and its difficulty lies elsewhere: a constraint on a single scheme is worthless unless it survives averaging over schemes and passing to limits of schemes of growing dimension, since only then does the Naor–Regev optimality theorem convert it into a statement about $K_G$. Constraints that are nonlinear in the scheme do not survive that passage, which is why the target inequality is affine in $(b_1,b_3)$. For the upper bound, the difficulty is that the improvement is genuinely asymptotic: it comes from a limit of schemes of growing dimension rather than any fixed low-dimensional partition, and the final margin of $3.47\times10^{-4}$ is certified numerically rather than in closed form.

Formalization scope

$\mathrm{OPT}(A)$ and $\mathrm{SDP}(A)$ are defined as suprema of explicitly described sets of reals, over matrices indexed by Fin m and Fin n with real entries; the sign vectors are real-valued functions constrained to take the values $1$ and $-1$, and the relaxation quantifies over unit vectors of EuclideanSpace ℝ (Fin d) for an existentially quantified $d$, so no dimension bound is built in. The empty-index cases $m=0$ or $n=0$ are included and give value $0$ on both sides. $K_G$ is the infimum of the set of Grothendieck bounds; that set is nonempty precisely by Grothendieck's inequality, which is itself a milestone, and it is bounded below, so the infimum is not a junk value.

A Krivine scheme is a structure carrying two measurable $\pm1$-valued functions on Fin k → ℝ, each odd almost everywhere. Almost-everywhere oddness is forced: no $\pm1$-valued function satisfies $f(-0)=-f(0)$ at the origin, so a pointwise requirement would make the structure empty and every statement about schemes vacuous. With the null-set relaxation the half-space partition is a scheme in every dimension $k\ge1$, and the definition file constructs it, pinning down non-vacuity; dimension $k=0$ admits no scheme. The correlation function is the explicit double Gaussian integral against the correlated-pair density, scaled by $\pi/2$, and the coefficients $b_1,b_3$ are read off as $H'(0)$ and $H'''(0)/6$ — where $H$ fails to be three times differentiable at $0$ these are the ambient junk value $0$, which a solver should keep in mind when reading the coefficient milestones.

No trivializing reading is available for the goal: it pins $K_G$ between two explicit numerical constants, so it can be satisfied neither vacuously nor by a degenerate convention. Solvers should be aware that the source paper states its two theorems in abridged form and refers to its companion paper for the full proofs, and that the further bounds reported there — the stronger lower rungs $27\pi/49$ and $51\pi/92$, and the upper values $1.781801841033$ and $1.7813319810625639$ — are explicitly described as system-tested but not author-verified; they are deliberately outside this mission's milestone list.

Selected references

• A. Grothendieck, Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79.
• J.-L. Krivine, Sur la constante de Grothendieck, C. R. Acad. Sci. Paris (1977).
• M. Braverman, K. Makarychev, Y. Makarychev, A. Naor, The Grothendieck constant is strictly smaller than Krivine's bound, FOCS 2011, 453–462. https://doi.org/10.1109/FOCS.2011.77
• A. Naor, O. Regev, Krivine schemes are optimal, Proc. Amer. Math. Soc. 142 (2014), 4315–4320. https://doi.org/10.1090/S0002-9939-2014-12145-3
• N. Alon, A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), 787–803. https://doi.org/10.1137/S0097539704441629
• A. Li, R. Saha, A. Xue, S. Chaudhuri, A. Klivans, P. K. Kothari, R. Meka, Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human–AI Mathematical Collaboration, arXiv:2608.11195v3, 2026. https://arxiv.org/abs/2608.11195
• R. Saha, A. Li, A. Xue, S. Chaudhuri, A. Klivans, P. K. Kothari, R. Meka, New upper and lower bounds for the Grothendieck constant, 2026 (companion paper containing the full proofs).

Motivation

Many statistical problems — nonparametric regression, density estimation, dimension reduction, testing — are naturally posed as optimization over a space of functions rather than a finite-dimensional parameter vector. Hilbert spaces provide the right generality: they carry an inner product and a norm, so notions of projection, orthogonality and least-squares fitting all make sense, exactly as in ordinary Euclidean space, even though the "vectors" are now functions. Reproducing kernel Hilbert spaces (RKHSs) are the particular class of function-valued Hilbert spaces that make this program computationally tractable: they are generated by a single bivariate kernel function, and every RKHS computation reduces to evaluating that kernel, never to manipulating an infinite-dimensional object directly (the "kernel trick"). Wainwright's High-Dimensional Statistics (2019), Chapter 12, develops the foundational correspondence between kernels and Hilbert spaces that makes this possible, and this mission formalizes its two central theorems.

Setting

A Hilbert space is a complete inner product space (Definitions 12.1–12.2); this mission uses Mathlib's own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace typeclasses for this notion throughout. A linear functional $L:H\to\mathbb R$ is bounded if $|L(f)|\le M\|f\|_H$ for some $M<\infty$ and all $f\in H$; the Riesz representation theorem (Theorem 12.5) says every such functional is $L(f)=\langle f,g\rangle_H$ for a unique $g\in H$.

A bivariate function $K:X\times X\to\mathbb R$ is a positive semidefinite (PSD) kernel (Definition 12.6) if it is symmetric and every finite Gram matrix $(K(x_i,x_j))_{i,j=1}^n$ is positive semidefinite — the natural generalization of a PSD matrix to a (possibly infinite) index set $X$, with no topological structure on $X$ required. A reproducing kernel Hilbert space (RKHS) for a kernel $K$ is a Hilbert space $H$ of functions on $X$ such that, for every $x\in X$, the function $K(\cdot,x)$ belongs to $H$ and

$$\langle f, K(\cdot,x)\rangle_H = f(x) \qquad \text{for all } f\in H \tag{12.3}$$

— the reproducing property. Equivalently (Definition 12.12), $H$ is an RKHS exactly when every evaluation functional $f\mapsto f(x)$ is bounded on $H$.

Formalization targets

Goal (Theorem 12.11, the Moore-Aronszajn theorem)

Given any PSD kernel function $K$ on any set $X$, there is a Hilbert space $H$ (embedded into functions on $X$) in which $K$ satisfies the reproducing property (12.3) — and this Hilbert space is unique: any two Hilbert spaces with this property for the same $K$ are linearly isometric via an isometry intertwining their embeddings into functions on $X$.

Milestones

• Theorem 12.5 (Riesz representation). Every bounded linear functional on a Hilbert space $H$ has a unique representer $g\in H$: $L(f)=\langle f,g\rangle_H$ for all $f$. Used inside the proof of Theorem 12.13 to produce the representer $R_x$ of each evaluation functional.
• Theorem 12.13 (the converse correspondence). Given any Hilbert space $H$ of functions on $X$ in which every evaluation functional is bounded, there is a unique PSD kernel $K$ satisfying the reproducing property for $H$ — completing the Moore-Aronszajn equivalence between PSD kernels and Hilbert spaces with bounded evaluation functionals.
• Theorem 12.20 (Mercer's theorem). Under compactness of $X$, continuity of $K$, and the Hilbert-Schmidt condition $\int_{X\times X}K^2\,dP\,dP<\infty$, the integral operator $T_K(f)(x)=\int_XK(x,z)f(z)\,dP(z)$ has an orthonormal eigenbasis $(\varphi_j)$ of $L^2(X;P)$ with non-negative eigenvalues $(\mu_j)$, and $K(x,z)=\sum_j\mu_j\varphi_j(x)\varphi_j(z)$, with the series converging absolutely and uniformly.

Significance

Theorem 12.11 is the theorem that makes the entire RKHS apparatus well-posed: every time a statistician writes down a kernel — linear, polynomial, Gaussian — Theorem 12.11 guarantees that a canonical Hilbert space of functions exists in which that kernel reproduces, so that optimizing over "the RKHS associated with $K$" is a well-defined problem, not merely a suggestive shorthand. Theorem 12.13's converse shows the correspondence is exact — the class of kernel-generated Hilbert spaces is exactly the class of function spaces with bounded evaluation, the class relevant to any statistical application that samples a function at finitely many points. Together, these two results are the foundation the book's own later chapters build directly on: Chapter 13's nonparametric least-squares oracle inequality, and Chapter 14's kernel density estimation, both work by optimizing over an RKHS and are only well-posed because of this correspondence. Mercer's theorem, in turn, is what connects the RKHS viewpoint back to the earlier feature-map viewpoint of Chapter 12.2.2 (Eq. 12.2): the eigenfunctions $(\sqrt{\mu_j}\varphi_j)_j$ give an explicit feature map into $\ell^2(\mathbb N)$ realizing $K$, and its expansion is what later underlies the book's discussion of kernel PCA and of RKHS balls as ellipsoids in $\ell^2(\mathbb N)$-coordinates.

Difficulty

The formalization difficulty is concentrated in getting the type of the existence-and- uniqueness claim right, not in any single hypothesis. A Hilbert space is not naturally a subtype of a fixed ambient space in Lean, so "the Hilbert space $H$" of Theorem 12.11 is formalized as an abstract type together with its own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace instances, connected to "a space of functions on $X$" via an injective linear embedding into $X\to\mathbb R$ — and uniqueness must then be stated as an isometric equivalence between any two witnessing Hilbert spaces that respects this embedding, the faithful rendering of the book's own proof, which literally shows two candidate Hilbert spaces are equal as sets of functions. A second subtlety is keeping Theorem 12.11's hypotheses (a bare PSD kernel, no topology on $X$) cleanly separated from Mercer's theorem's additional compactness, continuity and measure-theoretic apparatus — the two theorems are frequently conflated informally, but the book is explicit that Theorem 12.11 needs none of Mercer's structure.

Formalization scope

$X$ is an unconstrained Type* for Theorem 12.5, 12.11 and 12.13 — no topology, matching the book's own generality. Mercer's theorem (Theorem 12.20) additionally requires [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] and a finite measure P, matching its own compactness/continuity/measure-theoretic hypotheses exactly, never applied outside that scope. The integral operator $T_K$ of Eq. (12.11a) is presented as an abstract linear map on Lp ℝ 2 P tied to the defining integral formula via an explicit hypothesis, rather than constructed as a def, since constructing it as a genuine well-defined operator (needing integrability and a.e.-measurability arguments) is proof content, not definitional content, and this mission's definitions file is sorry-free by convention. Mercer's orthonormal-basis index type is existentially quantified over a countable ι (∃ (ι : Type) (_ : Countable ι), ...) rather than fixed to ℕ, since L²(X;P) can be finite-dimensional for finite X (Example 12.18/12.21), where no infinite orthonormal basis exists; the uniform-convergence conjunct is correspondingly quantified over every bijection e : ℕ ≃ ι (vacuous when ι is finite, a genuine order-independent claim when ι is countably infinite). A trivializing formalization of this chapter would state only existence in Theorem 12.11 and drop uniqueness (explicitly warned against by this chapter's own brief), or state Mercer's convergence merely pointwise or in $L^2$ rather than absolutely and uniformly; this mission avoids both. Out of scope: the constructive proof detail of Theorem 12.11 (the explicit span-and-complete construction is proof content, not part of the statement), the chapter's worked kernel examples (linear, polynomial, Gaussian kernels, Examples 12.7–12.9), and the further consequences of Mercer's theorem (Corollary 12.26 on RKHS-ball ellipsoids, the feature-map connection of Eq. 12.14) — all natural follow-on work for a future mission on kernel-based nonparametric regression (Chapter 13, mission 13-nonparametric-ls), which restates whatever RKHS objects it needs locally rather than importing this mission's draft, per this book's series-wide convention.

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 12. DOI: 10.1017/9781108627771.
• Aronszajn, N. "Theory of reproducing kernels." Transactions of the American Mathematical Society, 68(3), 1950, 337–404.
• Mercer, J. "Functions of positive and negative type, and their connection with the theory of integral equations." Philosophical Transactions of the Royal Society A, 209, 1909, 415–446.

The Hlawka inequality for Schatten $p$-norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge32$, also holds for every real $p\ge16$. This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-32 mission already covers every $p\ge32$, the new work is the range from 16 to 32.

The cutoff came down from 256 to 32 across eleven missions. The first phase (256 to 62) used a confinement estimate, exhausted at $p=61$. The second phase (62 to 32) used a new technique that broke through the confinement barrier. Whether it extends to 16 is not known; 16 asks for sixteen more units below the current best.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. The campaign conjectures the formula for all $p\ge2$. Any proof for a cutoff of 16 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh's Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 62.
• The accepted real coordinate bound for every real p ≥ 62.
• The accepted diagonal Schatten norm identity.

Motivation

The invariant subspace problem asks whether every bounded linear operator on an infinite-dimensional separable complex Hilbert space leaves some non-trivial closed subspace invariant. It is listed as a high-importance open problem in analysis in the Open Problem Garden (entry) and is widely regarded as one of the most famous open problems in functional analysis. Invariant subspaces are the infinite-dimensional replacement for eigenvectors: in finite dimensions every complex matrix has an eigenvector, and the structure theory of matrices (triangular and Jordan forms) is built from chains of invariant subspaces. Whether any such structure is available for an arbitrary bounded operator on Hilbert space is exactly what the problem asks.

Timeline

• 1930s (von Neumann, unpublished). Compact operators on Hilbert space have non-trivial closed invariant subspaces.
• 1954 (Aronszajn–Smith). The compact case on arbitrary Banach spaces (doi:10.2307/1969637).
• 1966 (Bernstein–Robinson; Halmos). Polynomially compact operators on Hilbert space.
• 1973 (Lomonosov). Every non-zero compact operator has a non-trivial closed hyperinvariant subspace; consequently every operator commuting with a non-zero compact operator has a non-trivial closed invariant subspace (doi:10.1007/BF01080698).
• 1975 announced / 1987 published (Enflo). A bounded operator on a separable Banach space with no non-trivial closed invariant subspace (doi:10.1007/BF02392260).
• 1985 (Read). Such an operator on the classical space $\ell^1$ (doi:10.1112/blms/17.4.305).
• 2011 (Argyros–Haydon). An infinite-dimensional Banach space on which every operator is a scalar plus a compact operator, so that every operator on it has a non-trivial closed invariant subspace (arXiv:0903.3921).

The Hilbert-space question remains open.

Setting

Let $\mathbb{K}$ be $\mathbb{R}$ or $\mathbb{C}$, let $E$ be a normed space over $\mathbb{K}$, and let $T\colon E\to E$ be a bounded linear operator. A linear subspace $S\subseteq E$ is invariant under $T$ if $T(S)\subseteq S$. It is a non-trivial closed invariant subspace if moreover $S$ is closed in the norm topology and $\{0\}\neq S\neq E$. A closed subspace $S$ with $\{0\}\neq S\neq E$ is a non-trivial closed hyperinvariant subspace of $T$ if $A(S)\subseteq S$ for every bounded operator $A$ with $AT=TA$.

A Hilbert space $H$ is a complete complex inner product space; it is separable if it has a countable dense subset. An operator $K$ is compact if it maps bounded sets to relatively compact sets, and $T$ is normal if $T^*T=TT^*$. In the Lean development these notions are IsInvariantSubspace, IsNontrivialClosedInvariantSubspace, HasNontrivialClosedInvariantSubspace and HasNontrivialClosedHyperinvariantSubspace (namespace InvariantSubspaceProblem), together with Mathlib's IsCompactOperator and IsStarNormal.

Formalization targets

Goal: the invariant subspace problem

$$\forall\, H \text{ separable, } \dim H=\infty,\ \forall\, T\in\mathcal{B}(H):\quad \exists\, S\subseteq H \text{ closed},\ \{0\}\neq S\neq H,\ T(S)\subseteq S .$$

The source poses a yes/no question; the goal states the affirmative answer, and a formal proof of its negation equally settles the problem.

Milestones (known results)

1. Finite-dimensional case: every operator on a complex space of dimension $\ge 2$ has a non-trivial invariant subspace.
2. Non-separable case: every operator on a non-separable complex normed space has a non-trivial closed invariant subspace.
3. Normal operators on a complex Hilbert space of dimension $\ge 2$.
4. Aronszajn–Smith: compact operators on infinite-dimensional real or complex Banach spaces.
5. Lomonosov: non-zero compact operators have non-trivial closed hyperinvariant subspaces.
6. Lomonosov: operators commuting with a non-zero compact operator.
7. Enflo: a separable infinite-dimensional complex Banach space with an operator having no non-trivial closed invariant subspace.
8. Read: such an operator on $\ell^1$.
9. Argyros–Haydon: a separable infinite-dimensional real Banach space on which every operator is $\lambda I+K$ with $K$ compact.
10. Argyros–Haydon: a separable infinite-dimensional real Banach space on which every operator has a non-trivial closed invariant subspace.

Significance

The result itself. A positive answer would give every bounded operator on Hilbert space a non-trivial piece of structure and would be the first step towards triangular-form type theorems for general operators. A negative answer would, after Enflo and Read, show that even the Hilbert-space geometry does not force invariant subspaces. Either answer resolves a question that has organised much of operator theory since the 1930s.

Formalizing it. The goal is open; no proof, formal or informal, is known. The milestones are proved results whose formal proofs would build reusable infrastructure absent from Mathlib: the Aronszajn–Smith and Lomonosov theorems (the latter through Schauder's fixed point theorem), invariant subspaces from the spectral theorem for normal operators, and the large explicit constructions of Enflo, Read and Argyros–Haydon. None of these results is formalized in Mathlib at the time of writing.

Difficulty

The obvious approach, taking the closed linear span of an orbit $\{x, Tx, T^2x,\dots\}$, fails exactly when every non-zero vector is cyclic, which is the situation that has to be ruled out; for separable spaces nothing prevents this a priori. Spectral methods fail because an operator can have a one-point spectrum and no eigenvectors (quasinilpotent operators). Methods that work on Hilbert space must use the inner-product structure in an essential way, since Enflo's and Read's examples show that the statement is false on some Banach spaces. Lomonosov's technique needs a non-zero compact operator in the commutant, which a general operator need not have.

Formalization scope

Hilbert spaces are Mathlib types H with [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is TopologicalSpace.SeparableSpace H and infinite dimension is ¬ FiniteDimensional ℂ H. Operators are continuous linear maps H →L[ℂ] H. Scalars are complex in the goal. Subspaces are Submodules, and closedness is required explicitly: without it the statement is trivially true in infinite dimensions (the algebraic span of an orbit is a proper invariant subspace), and a published platform statement that omits closedness should not be confused with this problem. Existential milestones quantify over spaces in Type.

Useful infrastructure includes: Schauder's fixed point theorem, Riesz theory of compact operators, the spectral theorem for normal operators, and $\ell^1$ machinery for Read's construction. Contributions of reusable lemmas, partial results (for instance further classes of operators known to have invariant subspaces), and proof sketches for the milestones are welcome.

Selected references

• Open Problem Garden, Invariant subspace problem, posted by T. Chow, 2009. http://www.openproblemgarden.org/op/invariant_subspace_problem
• N. Aronszajn, K. T. Smith, Invariant subspaces of completely continuous operators, Ann. of Math. 60 (1954) 345–350. https://doi.org/10.2307/1969637
• V. I. Lomonosov, Invariant subspaces for the family of operators which commute with a completely continuous operator, Funct. Anal. Appl. 7 (1973) 213–214. https://doi.org/10.1007/BF01080698
• P. Enflo, On the invariant subspace problem for Banach spaces, Acta Math. 158 (1987) 213–313. https://doi.org/10.1007/BF02392260
• C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$, Bull. London Math. Soc. 17 (1985) 305–317. https://doi.org/10.1112/blms/17.4.305
• S. A. Argyros, R. G. Haydon, A hereditarily indecomposable $\mathcal{L}_\infty$-space that solves the scalar-plus-compact problem, Acta Math. 206 (2011) 1–54. https://arxiv.org/abs/0903.3921
• H. Radjavi, P. Rosenthal, The invariant subspace problem, Math. Intelligencer 4 (1982) 33–37.
• B. S. Yadav, The present state and heritages of the invariant subspace problem, Milan J. Math. 73 (2005) 289–316.

Why an arithmetic lower bound is needed

The Riemann hypothesis asks whether every nontrivial zero of the actual Riemann zeta function has real part one half. The Connes formalization has a certified implication from positivity of the Weil distribution to RH. That implication supplies a criterion; its positivity hypothesis still needs a proof. The Green realization formalization supplies an independently certified physical carrier, actual-zero columns and bounded synthesis operators. Their construction does not establish the arithmetic inequality.

This open problem isolates a finite-certificate formulation of that inequality. The goal is new research within the existing formal development, not a theorem asserted by the cited papers. It is an RH-equivalent target. A proof of the reductions below is already available; a proof of the target itself is not.

The relevant historical distinction is explicit: Riemann stated the zero-location hypothesis in 1859; Connes' 1999 paper relates trace-formula and positivity questions to the zeros; the present Lean development certifies the conditional positivity criterion and the Green realization. None of these citations is offered as an unconditional proof of the new arithmetic certificate bound.

Actual zeros and the fixed physical carrier

Let $Z$ be the subtype of complex numbers $\rho$ satisfying $\zeta(\rho)=0$ and $0<\operatorname{Re}\rho<1$. Multiplicities are the existing natural analytic multiplicities. Reflection is $\rho\mapsto1-\overline\rho$, and conjugation is $\rho\mapsto\overline\rho$. For each actual zero, let $S_\rho$ be its finite reflection/conjugation orbit, called its quartet. Repeated orbit elements are removed by the finite-set construction, so the term does not assert four distinct zeros.

At a positive support radius $T$, the physical carrier $H_T$ is the existing closed Dirichlet energy-image completion on $[-T,T]$. Its energy convention is the integral of $|u'|^2+|u|^2/4$. Source lifts, Green columns and their pair normalization retain their published definitions. The original admissible tests are smooth compactly supported functions; the carrier is not defined from an arbitrary replacement zero family.

Write $p_{T,\tau}$ for the original positive column of an actual zero $\tau$, with the original reflected-pair and multiplicity normalization. Their complete squared-norm sum is certified summable at each positive radius. For a finite set $F\subset Z$, $P_F$ is the published synthesis of exactly these positive columns into $H_T$. Let $N_S$ be the original selected negative synthesis on the coefficient space for the unchanged quartet $S=S_\rho$.

Formalization target

For a positive accuracy $\delta$, define the already-published operators

$$B_F=P_F^*P_F+\delta I_F,\qquad C_{F,S}=P_F^*N_S,$$

and the selected coefficient correction

$$D_S(T,F,\delta)=\delta I_S-N_S^*N_S+C_{F,S}^*B_F^{-1}C_{F,S}.$$

The positive regularization makes $B_F$ strictly positive, including dependent or repeated columns. Its ring inverse is certified to be a genuine inverse for positive $\delta$.

The goal is

$$\forall\rho\in Z\;\forall b\in\mathbb R\;\exists T>\max(b,0)\;\forall\delta>0\;\exists F\subset Z\text{ finite}:$$ $$S_\rho\subseteq F,\quad F\text{ is reflection-closed},\quad \sum_{\tau\notin F}\|p_{T,\tau}\|^2<\delta,\quad D_{S_\rho}(T,F,\delta)\succeq0.$$

Here $T>\max(b,0)$ abbreviates the two strict inequalities in the Lean statement. The window is chosen before accuracy. The finite cutoff can depend on accuracy, but the selected negative quartet remains unchanged. The same accuracy occurs in the complete omitted tail and the correction operator.

What this target would establish

The certified fixed-window theorem identifies all-accuracy finite certificates with the original Picard marker being at least half the identity. The certified cofinal quartet criterion identifies arbitrarily large such quartet windows with Mathlib's Riemann hypothesis. Their composition has also been checked independently in the native Lean environment against the exact goal statement.

These two reductions are the principal milestones, alongside the existing literature-form positivity implication. Shared definitions and supporting theorems remain reusable library nodes. Certification of a reduction is distinct from establishing the nonnegative correction demanded by the goal. The goal is currently unproved and carries no RH or desired-positivity hypothesis.

The remaining difficulty

Finite tail cutoffs exist by summability, and regularized coefficient inverses exist by strict positivity. Those facts leave the sign of $D_S$ undetermined. An arithmetic representation of the full Weil operator alone also leaves that sign undetermined. The selected negative packet and the unselected negative background are different parts of the original signed operator; replacing one by the other changes the obligation.

The arithmetic transfer audit ZP-WEIL-MARKER-TRANSFER / RH-ZERO-PROV-2 records this distinction. Endpoint estimates or neutral-shell arguments contribute only when they supply the original lower bound with the required window and accuracy quantifiers. A bound at one boundary, an accuracy-dependent choice of window, or an estimate with a positive residual error floor does not supply the displayed target. No easier status is implied by its finite coefficient representation.

Formalization scope

The proposal uses Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474, with the published original quartet and selected-correction definitions. A separate native audit uses the existing Lean 4.34.0 repository environment. Complex Hilbert inner products are conjugate-linear in the first argument. Operator nonnegativity uses the existing continuous-linear-map order. Infinite tails are unordered sums on the actual-zero complement.

No simple-zero assumption, independence of columns, unregularized Gram inverse, replacement carrier, changed coefficient metric or silently restricted zero family is permitted. Quartets include zeros on the critical line; an empty actual-zero subtype would make the universal target vacuous, exactly as specified by the existing actual-zero indexing. New auxiliary definitions belong in shared definition bundles, and reusable algebraic lemmas belong in the library. The existing Green milestone history and dependency graph are retained.

Selected references

• B. Riemann, Ueber die Anzahl der Primzahlen unter einer gegebenen Grösse, Monatsberichte der Berliner Akademie, 1859. Original paper and translations.
• A. Connes, Trace formula in noncommutative Geometry and the zeros of the Riemann zeta function, Selecta Mathematica 5, 1999. arXiv:math/9811068. Source of the conditional positivity/RH context, not the new certificate inequality.
• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Springer, 2011. DOI. Functional-analytic background for the certified carrier.
• Published Lean results: cofinal quartet criterion, fixed-window selected certificates, and selected-correction definitions.
• monocap-tech/provenance, RH-ZERO-PROV-2 arithmetic-transfer checkpoint, 2026. Its stated status is representation complete, lower-bound theorem open, RH not proved.

Literature and source audit

The exact cofinal-quartet finite-certificate goal remains open. An independent Lean audit verifies its equivalence to Mathlib RiemannHypothesis by composing the two certified milestone reductions. The window is chosen before every positive regularization parameter; the selected actual-zero quartet is fixed, and the same parameter controls the full positive tail and selected correction. Tail summability and existence of inverses alone do not establish the required sign.

The foreign graph export ConnesRZ.weil_positivity_implies_RH matches the native ConnesRZClosed.weil_positivity_implies_RH: the older native ConnesRZ theorem takes explicitFormula as an input, discharged in Closed. The foreign record has a staged source qualification; it has not been edited.

Arithmetic transfer checkpoint: monocap-tech/provenance 178c83225b2300506ff622899d08ec3c987137d5, rh/checkpoints/RH_ZERO_PROV_2_EULER_WEIL_MARKER_TRANSFER_20260920.md, SHA256 0bb48b950f09220f7b2f193c16b45b15add0333906f919f8b50ca915f77a1a0d. Retained local Git bytes were verified; public availability is unverified. Critical-window location, the prescribed ordered-limit interface, and arithmetic endpoint/neutral-shell control remain open. RH is not established.

Motivation

Sampling from a distribution described relative to a Gaussian reference law is common in Bayesian inverse problems, where an unknown function or initial condition is inferred from noisy observations. Such a distribution is naturally infinite dimensional before it is approximated on a computer. A numerical method must therefore behave reliably as the approximation dimension grows. Hairer, Stuart and Vollmer study this question for Metropolis–Hastings chains and prove that the preconditioned Crank–Nicolson (pCN) chain admits a Wasserstein mixing bound with an iteration count independent of the projection dimension Hairer, Stuart and Vollmer (2014). This mission formalizes their globally Lipschitz case, Theorem 2.12.

The central practical concern is concrete: refining a discretization should improve the target approximation without forcing the number of Markov steps needed for a fixed contraction to grow with the number of coordinates. A bound on each finite dimensional chain separately would not settle that concern, because its constants could deteriorate with dimension. The theorem requires one set of constants for the infinite dimensional chain and every finite dimensional projection.

Setting

Let $H$ be a separable real Hilbert space. Its Gaussian reference measure $\gamma$ has mean zero and a covariance eigenbasis $e_1,e_2,\ldots$. The subspace $K_m$ is the span of the first $m$ eigenvectors, and $\gamma_m$ is the law of the orthogonal projection of a $\gamma$-distributed vector onto $K_m$. The potential $\Phi:H\to\mathbb R$ determines the target measures

$$\mu(dx)=M e^{-\Phi(x)}\gamma(dx),\qquad \mu_m(dx)=M_m e^{-\Phi(x)}\gamma_m(dx),$$

where $M$ and $M_m$ normalize each measure. The paper's finite dimensional chain has state space $K_m$, rather than the whole space $H$ with unused coordinates Hairer, Stuart and Vollmer (2014), (1.1)–(1.2).

At step size $0<\delta\le1/2$, the pCN proposal from $x$ is $y=\sqrt{1-2\delta}\,x+\sqrt{2\delta}\,\xi$, with $\xi$ drawn from $\gamma$ or $\gamma_m$ as appropriate. The move is accepted with probability $1\wedge e^{\Phi(x)-\Phi(y)}$; rejection leaves the state at $x$. Write $P$ and $P_m$ for these transition kernels Hairer, Stuart and Vollmer (2014), (1.3), (1.5)–(1.6).

The potential is globally Lipschitz, $e^{-\Phi}$ is $\gamma$-integrable, and the acceptance probability has a positive lower bound in specified balls centered at $\sqrt{1-2\delta}\,x$ outside a bounded region. These are Assumptions 2.10 and 2.11 Hairer, Stuart and Vollmer (2014), p. 12. The allowed ball radius is either a positive constant or $r_0\|x\|^a$ with $r_0>0$ and $1/2<a<1$.

Formalization targets

Uniform Wasserstein contraction

For $\varepsilon>0$, set $d_\varepsilon(x,y)=1\wedge\|x-y\|/\varepsilon$. Choose the Lyapunov function $V(x)=\|x\|^i$, where $i\ge1$, or, in the growing-radius case, $V(x)=e^{v\|x\|}$ with $v>0$. The weighted cost is $\widetilde d(x,y)=\sqrt{d_\varepsilon(x,y)(1+V(x)+V(y))}$, and $W_{\widetilde d}$ is its infimum over couplings.

Theorem 2.12 asserts that $\mu$ and each $\mu_m$ are the unique invariant probability measures of $P$ and $P_m$. It also asserts that, for every sufficiently small $\varepsilon$, there is one integer $\widetilde n$ satisfying both bounds for all probability measures on the respective spaces and for every $m$ Hairer, Stuart and Vollmer (2014), p. 12:

$$W_{\widetilde d}(\nu_1P^{\widetilde n},\nu_2P^{\widetilde n})\le\tfrac12 W_{\widetilde d}(\nu_1,\nu_2),$$ $$W_{\widetilde d_m}(\nu_1P_m^{\widetilde n},\nu_2P_m^{\widetilde n})\le\tfrac12 W_{\widetilde d_m}(\nu_1,\nu_2).$$

Here $\widetilde d_m$ is the same formula restricted to $K_m$. The milestone list includes the uniform Lyapunov, contraction and smallness claims and the cited weak Harris theorem; the Gaussian projection comparison of Lemma 3.1 is a further stated lemma of the mission. Fernique's Gaussian exponential-moment result is linked to its existing published formalization.

Significance

The result bounds the number of pCN iterations needed for a fixed Wasserstein contraction uniformly over the finite dimensional approximations. It also identifies the intended target as the only invariant probability measure, so the contraction describes convergence toward the measure used by the inverse problem. The weighted Wasserstein cost permits this statement on an unbounded Hilbert space, where an ordinary total variation small-set argument would impose a different kind of regularity Hairer, Stuart and Vollmer (2014), §§2.2–2.3.

The paper proved Theorem 2.12 in 2014. The remaining work here is a machine-checked development of the pCN kernels, Gaussian projections, Wasserstein estimates, and weak Harris application. A formalized Fernique theorem already exists in the platform library; the pCN estimates and Theorem 2.12 are open draft statements in this proposal. They will be reusable in the locally Lipschitz pCN regime and in analyses of other Metropolis kernels that satisfy the same abstract contraction conditions.

Difficulty

The pCN proposal contracts the starting points, but the accept–reject step can break that direct coupling: one chain may accept a proposal while the other rejects it. A bound on the proposal distance alone therefore does not imply a bound on the transition laws. The probability of that mismatched decision must be controlled near each pair of starting points, while the acceptance lower bound must remain uniform on the projected spaces. Large starting points also require a Lyapunov estimate to enter the bounded region used by the weak Harris theorem Hairer, Stuart and Vollmer (2014), §§3.1.1–3.1.3.

Formalization scope

The Lean development represents $H$ as a complete separable real inner product space with Borel measurable structure, $\gamma$ as a centered Gaussian probability measure, and the chosen Hilbert basis as diagonalizing its covariance. Second countability is stated explicitly for the measurable pCN construction; for a separable metric space it follows from the standing setting. The projected law is the pushforward by the orthogonal projection onto $K_m$, a reading of the Karhunen–Loève formula in the paper. A measurable map is essential here: Mathlib's pushforward returns zero for a nonmeasurable map.

The target is Mathlib's normalized tilted measure. The theorem explicitly concludes that both the infinite dimensional and projected targets are probability measures, so the possible junk zero from a nonintegrable tilt cannot satisfy the result. Wasserstein costs and Lyapunov expectations use extended nonnegative integrals. This avoids the junk zero of a nonintegrable Bochner integral and the junk values of a real infimum. Couplings are measures with the prescribed marginals. The acceptance kernel uses the paper's $1\wedge e^{\Phi(x)-\Phi(y)}$, including the first proposal and its rejection probability.

“Sufficiently small $\varepsilon$” means $\exists\varepsilon_0>0\,\forall\varepsilon\in(0,\varepsilon_0]$. The iteration count is chosen before $m$ and before the input probability measures. Positive radius, positive power exponent and positive exponential coefficient exclude empty acceptance balls and the constant Lyapunov function. The $m=0$ projection is retained as the zero dimensional subspace. Contributions that establish the Gaussian comparison, the three pCN estimates, or the abstract weak Harris statement are within scope.

Selected references

• M. Hairer, A. M. Stuart and S. J. Vollmer, Spectral gaps for a Metropolis–Hastings algorithm in infinite dimensions, Annals of Applied Probability 24(6), 2014, 2455–2490. arXiv:1112.1392v4, DOI:10.1214/13-AAP982.