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

Existence theory for elliptic, parabolic and nonlinear PDEs mostly runs through one argument: build approximate solutions, bound them in a Sobolev norm, extract a convergent subsequence, and pass to the limit. The extraction step needs a compact embedding: a bound on derivatives must buy convergence of the functions themselves in a weaker norm. On a bounded domain this is the Rellich–Kondrachov theorem. It is what makes the resolvent of the Dirichlet Laplacian compact, and so gives the Fredholm alternative and the discrete spectrum of elliptic operators on bounded domains. The companion topics of the same section, extension and trace, are how Sobolev functions are moved between a domain and all of space, and how they are given boundary values.

This mission follows Chapter 3 (§3.9–3.10) and Theorem 1.15 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014).

Timeline. Rellich proved the compactness of $H^1_0 \hookrightarrow L^2$ on bounded domains in 1930. Kondrachov extended it to $W^{1,p}$ and exponents below the Sobolev exponent in 1945. The $L^p$ compactness criterion used in the notes goes back to Kolmogorov (1931) and M. Riesz (1933); a modern account with a history is Hanche-Olsen and Holden 2010. Gagliardo characterized the traces of $W^{1,p}$ in 1957.

Setting

Throughout, $\mathbb{R}^n$ carries Lebesgue measure, and functions are real-valued. For an open set $\Omega \subseteq \mathbb{R}^n$, a test function $\phi \in C_c^\infty(\Omega)$ is smooth with compact support inside $\Omega$. A locally integrable $g$ is the weak derivative $\partial^\alpha f$ of a locally integrable $f$ if $\int_\Omega g\phi = (-1)^{|\alpha|}\int_\Omega f\,\partial^\alpha\phi$ for every test function $\phi$. Here $\alpha \in \mathbb{N}_0^n$ is a multi-index of order $|\alpha| = \sum_i \alpha_i$.

For $k \in \mathbb{N}$ and $1 \le p \le \infty$, the Sobolev space $W^{k,p}(\Omega)$ consists of the $f$ whose weak derivatives $\partial^\alpha f$, $|\alpha| \le k$, exist and lie in $L^p(\Omega)$. For $p < \infty$ its norm is

$$\|f\|_{W^{k,p}(\Omega)} = \Big(\sum_{|\alpha|\le k} \int_\Omega |\partial^\alpha f|^p\,dx\Big)^{1/p},$$

and for $p = \infty$ it is the maximum of the essential suprema. The space $W^{k,p}_0(\Omega)$ is the closure of $C_c^\infty(\Omega)$ in this norm. For $1 \le p < n$ the Sobolev conjugate is $p^* = np/(n-p)$.

The upper half-space is $\mathbb{R}^n_+ = \{x = (x', x_n) : x_n > 0\}$, with closure $\overline{\mathbb{R}}^n_+$ and boundary $\partial\mathbb{R}^n_+ = \{(x', 0)\} \cong \mathbb{R}^{n-1}$. The space $C_c^\infty(\overline{\mathbb{R}}^n_+)$ consists of the functions that are smooth up to the boundary and vanish outside a compact set. Unlike $C_c^\infty(\mathbb{R}^n_+)$, they need not vanish on $\partial\mathbb{R}^n_+$.

A subset of a metric space is precompact if its closure is compact. $C_0(\mathbb{R}^n)$ is the space of continuous functions vanishing at infinity, with the sup norm.

In Lean the weak derivative is HasWeakDeriv (with weakDeriv and weakGradNorm) in the series' shared namespace HunterPDE.Shared; the other objects are MemW k p Ω f, sobolevNorm k p Ω f, MemW0 k p Ω f, sobolevConjugate, upperHalfSpace m, IsSmoothCompactClosedHalfSpace and boundaryPoint, in the namespace HunterPDE.Compactness.

Formalization targets

Goal: Rellich–Kondrachov (Theorem 3.45)

Let $\Omega$ be a bounded open set in $\mathbb{R}^n$, $1 \le p < n$ and $1 \le q < p^*$. If $\mathcal{F} \subseteq W^{1,p}_0(\Omega)$ satisfies $\|f\|_{W^{1,p}(\Omega)} \le M$ for all $f \in \mathcal{F}$, then

$$\{\, f\mathbf{1}_\Omega : f \in \mathcal{F} \,\} \ \text{is precompact in } L^q(\mathbb{R}^n).$$

Milestones

• Theorem 1.15 (Kolmogorov–Riesz). For $1 \le p < \infty$, a set $\mathcal{F} \subseteq L^p(\mathbb{R}^n)$ is precompact if and only if it is bounded, tight ($\sup_{f}\|f\|_{L^p(|x|>R)} \to 0$ as $R \to \infty$), and $L^p$-equicontinuous:

$$\forall \varepsilon > 0\ \exists \delta > 0:\ |h| < \delta \implies \|f(\cdot + h) - f\|_{L^p(\mathbb{R}^n)} < \varepsilon \quad \forall f \in \mathcal{F}.$$

• Theorem 3.41 (extension). There is a bounded linear $E : W^{1,p}(\mathbb{R}^n_+) \to W^{1,p}(\mathbb{R}^n)$ with $Ef = f$ a.e. on $\mathbb{R}^n_+$ and $\|Ef\|_{W^{1,p}(\mathbb{R}^n)} \le C(n,p)\,\|f\|_{W^{1,p}(\mathbb{R}^n_+)}$.
• Theorem 3.42 (density). $C_c^\infty(\overline{\mathbb{R}}^n_+)$ is dense in $W^{k,p}(\mathbb{R}^n_+)$ for $1 \le p < \infty$.
• Theorem 3.44 (trace). For $1 \le p < \infty$ there is a bounded linear $T : W^{1,p}(\mathbb{R}^n_+) \to L^p(\mathbb{R}^{n-1})$ with $(Tf)(x') = f(x', 0)$ on $C_c^\infty(\overline{\mathbb{R}}^n_+)$ and $\|Tf\|_{L^p} \le C(p)\,\|f\|_{W^{1,p}(\mathbb{R}^n_+)}$, whose kernel is exactly $W^{1,p}_0(\mathbb{R}^n_+)$.
• Theorem 3.48 ($p > n$). For $\Omega$ bounded and $n < p < \infty$, a family with $\operatorname{supp} f \Subset \Omega$ and $\|Df\|_{L^p} \le C$ is precompact in $C_0(\mathbb{R}^n)$.

The goal is stated qualitatively (precompactness), with no constants, so it does not depend on any particular form of the Sobolev inequality.

Significance

The result itself. Rellich–Kondrachov is the source of compactness in the $L^2$ theory of elliptic equations. With it, the solution operator of a coercive elliptic problem on a bounded domain is compact. That yields the Fredholm alternative, the discreteness of the Dirichlet spectrum, and existence results for semilinear problems via compactness and fixed-point arguments. The trace theorem makes the boundary condition "$u = 0$ on $\partial\Omega$" meaningful for Sobolev functions, and identifies $W^{1,p}_0$ as the space in which Dirichlet problems are posed. The extension theorem transfers whole-space results to domains. Theorem 3.48 gives the uniform-norm counterpart above the critical exponent.

Formalizing it. All results here are classical and proved. The notes prove 3.45, 3.48 and the forward direction of 3.44. They describe 3.41 and 3.42 in a sentence each, and cite 1.15 without proof. Mathlib has the Lebesgue spaces Lp, Arzelà–Ascoli for bounded continuous functions, and mollification. It has no weak derivatives, no Sobolev spaces on domains, no trace, no extension operators and no Kolmogorov–Riesz criterion. A complete development would supply the first machine-checked versions of these in the notes' form, and a formal $W^{1,p}_0$ compactness theorem usable by the elliptic chapters of the same series.

Difficulty

The obvious route to the goal is: approximate by test functions, extend by zero, and verify the three Kolmogorov–Riesz conditions. The first two follow from the Sobolev inequality and the boundedness of $\Omega$. The hard parts are elsewhere. First, the Kolmogorov–Riesz criterion is not in Mathlib, and its "if" direction needs a mollification and total-boundedness argument in $L^p(\mathbb{R}^n)$. Second, the $L^q$-equicontinuity for $q$ above $p$ needs an interpolation between an $L^1$ translation estimate and the critical Sobolev embedding into $L^{p^*}$, so the Gagliardo–Nirenberg–Sobolev inequality must be available for $W^{1,p}_0(\Omega)$, not only for smooth compactly supported functions. Third, weak derivatives are defined by integration against test functions, and every density step has to be carried through that definition. The exponent restriction $q < p^*$ is sharp (Example 3.47 in the notes), so no argument that ignores it can succeed.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume. Open sets are Ω : Set _ with IsOpen Ω, and bounded means Bornology.IsBounded Ω. Coordinates are 0-based (i : Fin n), and multi-indices are α : Fin n → ℕ.
• Functions are ℝⁿ → ℝ, and only their values on the relevant set matter. weakDeriv is a chosen representative, used only where a weak derivative is assumed to exist. sobolevNorm takes values in ℝ≥0∞.
• $W^{1,p}_0(\Omega)$ is the norm closure of $C_c^\infty(\Omega)$, not "zero trace". "Bounded in $W^{1,p}_0(\Omega)$" is a uniform bound on sobolevNorm 1 p Ω.
• In the goal, $\mathcal{F}$ is placed in $L^q(\mathbb{R}^n)$ by extension by zero (Ω.indicator f). The conclusion asserts both that each extension lies in $L^q$ and that the set of their classes in Mathlib's Lp ℝ q volume has compact closure. The hypothesis $q < p^*$ rules out $q = \infty$.
• Half-space results use dimension $n = m+1$ and the last coordinate Fin.last m. The boundary is $\mathbb{R}^m$ via $x' \mapsto (x',0)$. Extension and trace operators are maps on functions that are linear up to a.e. equality on $W^{1,p}(\mathbb{R}^n_+)$.
• Conventions read off the page: in Theorem 3.44 the trace constant is quantified before the dimension ("depending only on $p$"), and its final clause is taken with $k = 1$ (the printed "$W^{k,p}_0$" cannot mean $k \ge 2$, as the notes remark after the proof). Theorem 3.42 is stated for $1 \le p < \infty$, and Theorem 3.41 for $1 \le p \le \infty$. Theorem 3.48 assumes $n \ge 1$.
• A trivializing reading is ruled out: the goal's conclusion is compactness of the closure in $L^q(\mathbb{R}^n)$ of the zero extensions themselves, not of some other representative. The norm bound is on the genuine weak derivatives, which the hypotheses guarantee exist, not on a junk value.
• Reusable infrastructure: weak derivatives and Sobolev spaces on open sets, the Kolmogorov–Riesz criterion, and the half-space extension and trace operators. Contributions of any of these as standalone lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §1.5 and §3.9–3.10. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• H. Hanche-Olsen and H. Holden, The Kolmogorov–Riesz compactness theorem, Expositiones Mathematicae 28 (2010) 385–394. https://arxiv.org/abs/0906.4883
• L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, §5.5–5.7. https://doi.org/10.1090/gsm/019

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.

Motivation

Quantum mechanics represents the states of a system by unit vectors (normed rays) of a complex Hilbert space $\mathcal H$ and its observables by self-adjoint operators on $\mathcal H$. The most important observables — position, momentum, energy — are unbounded. A. Heathcote's paper Unbounded Operators and the Incompleteness of Quantum Mechanics (Philosophy of Science 57, 1990, 523–534) draws attention to a mathematical fact that is routinely glossed over in physical texts: an unbounded self-adjoint operator cannot be defined on all of $\mathcal H$, and there are concrete normalized wave functions on which the position and momentum operators do not act at all. The paper uses this to argue that the standard postulates of quantum mechanics are, in a precise sense, incomplete.

This mission isolates the mathematical content of that argument, which is a clean and checkable piece of functional analysis on $L^2(\mathbb R)$.

Setting

Let $\mathcal H$ be a complex Hilbert space. A (partially defined) linear operator $A$ has a domain $D(A)\subseteq\mathcal H$; it is bounded if there is $k\in\mathbb R$ with $\|A\psi\|\le k\|\psi\|$ for all $\psi\in D(A)$, and unbounded otherwise. It is self-adjoint if it equals its Hilbert adjoint, $A=A^*$, which includes $D(A)=D(A^*)$.

On $\mathcal H=L^2(\mathbb R)$:

1. The position operator acts by $(Q\psi)(x)=x\,\psi(x)$ on

$$D(Q)=\Big\{\psi\in L^2(\mathbb R): \int_{\mathbb R}x^2|\psi(x)|^2\,dx<\infty\Big\}\qquad\text{(eq. (3))}.$$

2. The momentum operator $P\psi=\hbar i^{-1}\,d\psi/dx$ has, in the paper's description, domain $D(P)$ consisting of the absolutely continuous functions in $L^2(\mathbb R)$.
3. Heathcote's wave function (eq. (4)) is

$$\psi(x)=\begin{cases}x^{-1}, & x\ge 1,\\ 0, & x<1.\end{cases}$$

Formalization targets

Goal

There is a unit vector of $L^2(\mathbb R)$, namely the class of $\psi$, lying in neither domain:

$$\exists\,\varphi\in L^2(\mathbb R):\quad \varphi=\psi\ \text{a.e.},\qquad \|\varphi\|=1,\qquad \varphi\notin D(Q),\qquad \varphi\notin D(P).$$

Milestones

1. Hellinger–Toeplitz (p. 2, footnote 1): a symmetric operator defined on all of a Hilbert space is bounded (an existing platform theorem).
2. Unbounded self-adjoint operators (p. 2, footnote 2): if $A=A^*$ is unbounded then $D(A)$ is dense and $D(A)\neq\mathcal H$.
3. Normalization (p. 5): $\psi\in L^2(\mathbb R)$ and $\int|\psi|^2=\int_1^\infty x^{-2}dx=1$.
4. Not in $D(Q)$ (p. 5): $\int x^2|\psi(x)|^2dx=\infty$.
5. Not in $D(P)$ (pp. 5–6): no a.e.-representative of $\psi$ is absolutely continuous on every compact interval.
6. Infinite position expectation (p. 9): $\int|x|\,|\psi(x)|^2dx=\int_1^\infty x^{-1}dx=\infty$.

Significance

The result. The goal shows that the two postulates "every normed ray is a state" and "observables are self-adjoint operators" force the existence of states on which the position operator (and, independently, the momentum operator) is undefined. Milestone 5 is what the paper uses to separate this phenomenon from the canonical commutation relations: the failure of $\psi\in D(Q)$ is not explained by $\psi$ being "sharp in momentum", because $\psi$ is not even in $D(P)$. Milestone 6 records the physical reading: the mean position of this normalized state is infinite.

Formalizing it. The individual facts are standard and elementary; none of them is new. What the mission produces is a machine-checked version of the paper's argument stated against the actual $L^2$ space and Mathlib's notion of unbounded operators and adjoints, with the domain conventions made explicit.

Difficulty

The calculus is easy; the subtleties are in the bookkeeping. Elements of $L^2(\mathbb R)$ are almost-everywhere classes, so "$\psi$ is discontinuous at $1$" does not by itself show $\psi\notin D(P)$: one must rule out every a.e.-modification of $\psi$ being absolutely continuous. Similarly, the Hellinger–Toeplitz argument gives $D(A)\neq\mathcal H$ but not density, which comes from the adjoint being a genuine operator.

Formalization scope

• Operators are Mathlib's partially defined linear maps H →ₗ.[ℂ] H; self-adjointness is IsSelfAdjoint with respect to the adjoint A†, over a complex complete inner product space.
• $L^2(\mathbb R)$ is Lp ℂ 2 volume on ℝ; $D(Q)$ and $D(P)$ are subsets of it. Integrals of non-negative quantities are Lebesgue integrals valued in $[0,\infty]$, so "$=\infty$" is literal and not a junk value.
• $D(P)$ follows the paper (absolutely continuous elements, i.e. having a representative absolutely continuous on every $[a,b]$) and omits the standard requirement $\psi'\in L^2$. This set contains the standard domain, so non-membership is a stronger statement.
• The paper's further claim that $\psi\notin D(H)$ for a Hamiltonian $H=P^2/2m+V$ is stated there without proof and for an unspecified potential $V$, and is not included.
• Trivialization is excluded: the goal pins $\varphi$ to the explicit function $\psi$ and requires $\|\varphi\|=1$.

Selected references

• A. Heathcote, Unbounded Operators and the Incompleteness of Quantum Mechanics, Philosophy of Science 57 (1990), 523–534.
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised ed., Academic Press, 1980.

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.