Why the Green realization matters

The Weil positivity criterion relates the zeros of the Riemann zeta function to an arithmetic quadratic form. The existing Connes mission now has a proved positivity-implies-RH goal. Stronger actual-zero quartet separation also controls the complete complementary coefficient energy. Neither result by itself identifies those scalar coefficients with the adjoint of a physical Dirichlet Green operator.

This mission addresses that identification. The underlying mathematics is the classical Hilbert-space realization of a positive Dirichlet operator, as treated in Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, applied to the original source functions and analytic multiplicities in the Connes–Weil development. It formalizes a known functional-analytic construction; it does not claim a proof of Weil positivity or unconditional RH. The exact goal is the assembly specified below, rather than a theorem quoted verbatim from Brezis or Connes.

The fixed physical space

Fix a positive radius $t$ and put $I_t=[-t,t]$, with restricted Lebesgue measure. A supported test is a smooth compactly supported complex function $g$ on the real line whose closed support lies strictly inside $(-t,t)$. The differential operator and its energy map are

$$L=-\frac{d^2}{dx^2}+\frac14,\qquad J_tu=(u',u/2).$$

The ambient space is the Hilbert direct sum of two copies of $L^2(I_t;\mathbb C)$, using the sum of squared norms, not the Banach product maximum norm. Define the physical carrier $H_t$ to be the closure of the complex linear span of $J_tg$ for all supported tests. Thus its metric is fixed by

$$\|J_tu\|^2=\int_{-t}^{t}(|u'|^2+|u|^2/4)\,dx.$$

This carrier is defined independently of the zeta-zero set. It is the energy-image completion of the Dirichlet test space; the source-side $H^{-1}_L$ interpretation is through Riesz representation, not by identifying the positive Sobolev norm of $g$ with the source norm of $g$.

For an $L^2$ source $f$, the source lift is the orthogonal projection of $(0,2f)$ onto $H_t$. The factor two fixes the pairing convention: its inner product against $J_tu$ represents $\int\overline u f$. The induced map on functions uses their $L^2$ classes. Its total definition sends non-$L^2$ functions to zero; all actual sources and tests used in the target must explicitly satisfy the required $L^2$ conditions, so this fallback cannot discharge the target.

The actual Green columns

Let $Z$ be exactly the set of zeros $\rho$ of the actual Riemann zeta function with $0<\operatorname{Re}\rho<1$. Let $m_\rho$ be their natural analytic multiplicity. No surrogate zero configuration or simple-zero convention is used. Write

$$\gamma_\rho=-i(1-\overline\rho-1/2),\quad f_\rho(x)=\exp(x(-i\gamma_\rho)),\quad q_\rho=(1/4+\gamma_\rho^2)^{-1}.$$

The original Green column is the existing function

$$F_{t,\rho}(x)=q_\rho f_\rho(x)-q_\rho f_\rho(t)\frac{\sinh((t+x)/2)}{\sinh t}-q_\rho f_\rho(-t)\frac{\sinh((t-x)/2)}{\sinh t}.$$

Its energy is the existing Dirichlet integral $E_{t,\rho}=\int_{-t}^t(|F'_{t,\rho}|^2+|F_{t,\rho}|^2/4)$. The reflected ordinate is retained because the Hilbert inner product is conjugate-linear in its first argument. The ported native definitions have been checked for definitional equality against the repository definitions.

Formalization targets

The goal, for every $t>0$, is the following conjunction. First, the source lift from $L^2(I_t)$ has dense range in $H_t$. This asserts density, not surjectivity. Second, every actual Green column has the required $L^2$ regularity and belongs to the prescribed energy completion, and

$$\operatorname{embed}_t(f_\rho)=J_tF_{t,\rho},\qquad \|\operatorname{embed}_t(f_\rho)\|^2=E_{t,\rho}.$$

Third, for every supported test $g$, the source $Lg$ is square integrable, the Green product is integrable, and

$$\langle\operatorname{embed}_t(f_\rho),\operatorname{embed}_t(Lg)\rangle=\int_{-t}^t\overline{F_{t,\rho}(x)}\,Lg(x)\,dx.$$

Finally, the full actual-zero weighted energy is summable. For $v_\rho=\sqrt{m_\rho}\operatorname{embed}_t(f_\rho)$, construct the bounded synthesis $S_t:\ell^2(Z;\mathbb C)\to H_t$ with these exact columns. Every synthesis series must be summable, and

$$S_tu=\sum_\rho u_\rho v_\rho,\quad (S_t^*h)_\rho=\langle v_\rho,h\rangle,\quad \|S_t^*h\|^2=\sum_\rho|\langle v_\rho,h\rangle|^2,\quad \|S_t\|^2\le\sum_\rho m_\rho E_{t,\rho}.$$

Require uniqueness among bounded maps on this same coefficient carrier with these same basis columns. None of these norm, projection, density, pairing, or summability conclusions appears as a hypothesis of the goal.

Certified completion

The published reciprocal-square theorem supplies the actual-zero majorant underlying the native energy bound. The published bounded-synthesis theorem supplies the generic operator construction and adjoint identities. They are included as references with their existing identities, not re-created.

The aggregate goal and all seven original mission milestones are now Proved on P2M, with zero open leaves. The independent native development also proves original-constructor physical selected-quartet separation, preserving the exact columns, packet coefficients, complete positive zero family, analytic multiplicities and half-sum/half-difference actor normalization. The realization hypotheses have been discharged for the specified carrier at each positive support window. Neither this construction nor conditional positivity-implies-RH establishes Weil positivity or unconditional RH.

Mathematical content of the certified realization

An explicit smooth column vanishing at the endpoints is not, solely by those facts, an element of the closure of tests supported strictly inside the interval. The certified proofs establish that boundary-density statement in the chosen energy topology and identify the Riesz projection with the explicit Green column. Source-lift density uses the value component to distinguish vectors in the closed derivative graph. No physical column-norm or pairing assertion is assumed.

Formalization scope

All definitions, target statements and accepted proofs are checked against Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The additive repository model also compiles with the existing Lean 4.34.0 development. The approved mission retains its shared definition bundle, aggregate goal and seven original proved milestones. Subsequent accepted supporting library lemmas are linked separately, with their exact published hypotheses and conclusions.

Each support radius has its specified carrier $H_t$. Subsequent native results construct the original test-preserving isometries for nested positive support windows and transfer their actual source columns and syntheses. These are constructed inclusions, rather than identifications with a single fixed physical carrier. Downstream packet transfer retains the same-radius basis-column custody. The goal makes no claim that every prescribed window contains a negative Weil witness. The globally constructed separating test may choose its support radius after amplification. The original finite-packet inner regularization norm limits and outer right-hand support norm limits are proved natively, in that order. Subsequent certified reductions classify actual-quartet good windows and express the original fixed-window half-bound as all-accuracy finite certificates. These results do not prove the arithmetic lower inequality. Identification with the prescribed arithmetic/provenance packet endpoint and the arithmetic endpoint lower bound with original neutral-shell custody and persistence remain open for ZP-WEIL-MARKER-TRANSFER / RH-ZERO-PROV-2. The selected-coefficient certificate theorem retains the complete actual-positive tail; it establishes an equivalence, not certificate nonnegativity.

Mission boundary and milestone history

The Textbook category applies to this mission's original known functional-analytic construction. Its realization-and-synthesis goal is complete. The existing downstream milestone list and dependency graph are retained as an archive of certified extensions; milestone completion does not mean that every linked result is a premise of the original goal or that RH has been established. Future supporting definitions and lemmas remain shared library nodes unless they warrant a substantial, source-grounded checkpoint.

The unresolved arithmetic lower bound is being organized in a separate OpenProblem draft, Connes–Weil arithmetic lower bound: cofinal actual-quartet certificates. Its target requires arbitrarily large actual-quartet windows with all-accuracy nonnegative selected certificates and the complete omitted positive tail controlled at the same accuracy. The existing cofinal quartet criterion and finite selected-certificate criterion are proved reductions. The new draft goal itself is unproved and is equivalent to RH in the existing development.

Selected references

• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Springer, 2011. DOI. Background on Hilbert representation, Sobolev completions and Dirichlet problems.
• A. Connes, Trace formula in noncommutative Geometry and the zeros of the Riemann zeta function, Selecta Mathematica 5, 1999. arXiv. Context for the positivity criterion; the canonical Green model here is an explicit subsequent formalization target.
• monocap-tech/weil, existing native definitions in DirichletResolvent.lean and DirichletEnergy.lean. Canonical model and goal specification are supplied explicitly in this proposal. The complete independently checked Green-frontier source snapshot has SHA256 ce194a69770846a9027a274e581de56b507be219c393d080a06259e175cbe798; this is a source custody record, not a claim that the archive was attached to P2M.