24 Thread Weil-Semiboundedness
New thread (2026-08-23), opened from formalization_queue rather than a manuscript handoff: a ChatGPT-relayed research program attacking RH via a semibounded Weil criterion — RH \(\iff \) \(\exists \) finite \(C\ge 0\) with \(Q_W(v)\ge -C\| v\| _2^2\) for every compactly supported smooth \(v\) (Weil positivity is the \(C=0\) case), routed through Suzuki’s 2023/2026 Herglotz-function reformulation and the Krein–Langer screw-function correspondence. Four items landed in the queue at priority 0 (top), all in this thread; per standing protocol (attempt every ready item directly in Lean, no by-hand pre-proof gate, classify honestly, never axiomatize the desired conclusion) each was attempted this pass.
Abstract nested-infimum order theory, applicable to Suzuki’s localized Weil ground energy \(\lambda _a\) once it is supplied concretely: if a family of test-function sets \(S_a\) is nested and \(\lambda _a\) is the greatest lower bound of a ratio functional over \(S_a\), then (i) \(\lambda \) is antitone; (ii) a uniform global lower bound over \(\bigcup _a S_a\) is equivalent to \(\operatorname {range}\lambda \) being bounded below (phrased via BddBelow rather than a literal sInf, to avoid Real.sInf’s junk-value convention on sets unbounded below); (iii) antitone plus not bounded below forces \(\lambda _a\to -\infty \). Genuinely proves (formalization_queue item 1b12010b) exactly the order-theoretic content that item asked for, with no reference to what the ratio functional or test spaces concretely are.
Same abstract setting. The global ratio set \(R''\bigcup _a S_a\) and the family \(\operatorname {range}\lambda \) have the same lower bounds (), from which: \(L\) is the global greatest lower bound iff it is the greatest lower bound of the localized ground energies, the two sets are bounded below together, and — with nesting — \(\lambda _a\to L\). Sharpens Theorem 24.1(ii), which matched only the existence of a bound on each side: the two optimal constants are the same real number, reached as a limit, so localization loses nothing. Accompanied by the dichotomy : an antitone \(\lambda \) either diverges to \(-\infty \) or converges to \(\bigsqcap _a\lambda _a\), with no third case, so no downstream statement needs to assume convergence.
Honest boundary, this pass. Theorem 24.1 does not define \(Q_W\), the Weil quadratic form, \(\| \cdot \| _2\), or \(S_a=C_c^\infty (-a,a)\) — no such localized compactly-supported-test-function machinery exists in Mathlib, and building it is a separate, large undertaking untouched here. The other three priority-0 queue items were assessed, not completed:
Conditional convolution positivity implies screw-kernel positivity (item 50903a57): feasible in principle — Mathlib’s ContDiffBump.convolution_tendsto_right_of_continuous supplies exactly the “approximate identity converges to a continuous function’s value at a point” fact the queue item’s suggested proof needs — but the full construction (building the finite-support mean-zero mollified test function \(u_\varepsilon \) from a sum of point masses, expanding the assumed double integral into a finite sum of bilinear terms via Fubini, and taking \(\varepsilon \to 0\) termwise to recover \(G_h(t_i,t_j)\) exactly) is a genuinely large multi-lemma real-analysis construction, scoped but not attempted this pass rather than forced through partially.
Semibounded Weil criterion forces RH (item ed078a8f) and Finite Brownian compensation shifts the zeta Herglotz function by \(iC/2\) (item 93384c2c): both genuinely blocked. Both require Herglotz (Pick) function representation theory and the Krein–Langer correspondence between screw functions and Herglotz functions cited from Suzuki’s paper. Checked directly (grep -rli "herglotz|nevanlinna|krein.*langer|screw function" Mathlib/): the only Mathlib hit is Nevanlinna value-distribution theory (the Second Main Theorem counting-function sense), an unrelated subject from a different branch of complex analysis — there is no Herglotz/Pick integral-representation theory or Krein–Langer machinery in Mathlib at all. Formalizing either item first requires building that entire theory from scratch, which is not attempted here.
A further scan of the remaining ready queue (priorities 1–2, threads Weil-Parity, Suzuki-Herglotz, Prime-Schatten, Prime-Scattering, Prime-Fock) found the same two obstructions recurring: items naming Pick kernels or Herglotz reflection symmetry inherit the same missing-theory gap as above, and items in the Prime-Schatten/ Prime-Scattering/Prime-Fock threads (Schatten-class operator norms, regularized \(\det _3\) Fredholm determinants, bosonic Fock-space trace identities) are blocked on a second, independent gap: Mathlib has no Schatten-class, trace-class, or regularized/Fredholk determinant theory for Hilbert-space operators at all (checked directly, zero hits). None of these were force-completed with a watered-down or circular substitute. This is a real, useful negative finding, not a stall: two precise, named infrastructure gaps now block a large fraction of the open queue, and building either (Herglotz representation theory, or Schatten-class operator theory) would be a substantial standalone Mathlib-contribution-sized undertaking in its own right, worth flagging to Daniel as a strategic fork rather than attempting piecemeal.
Correction, same pass. The initial scan above assumed the entire Weil-Parity thread was blocked by the same missing Herglotz/Pick machinery, by pattern-matching on the thread name rather than reading each item’s body. That was wrong. Reading the six Weil-Parity queue items directly found that most are pure finite-dimensional linear algebra or topology — several explicitly say so in their own text (“pure linear algebra and should be sorry-free,” “pure finite-dimensional topology”). Two were formalized this pass once correctly assessed:
Item 0182d9cf. If continuous functions on a preconnected set never cross and one starts strictly below the other at some point, it stays strictly below everywhere — via IsPreconnected.intermediate_value₂: a crossing point would otherwise be forced between the two points.
Item 5e10a4f0. If a determinant-ratio identity \(B_{\det }(z)=f(z)\, A_{\det }(z)\) holds with both factors positive for \(z{\lt}\lambda _{\min }(A)\), then \(B_{\det }(z){\gt}0\) there — algebraically immediate once stated correctly, and (once \(B_{\det }\) is identified with \(z\mapsto \det (B-zI)\)) exactly “\(B\) has no eigenvalue below \(\lambda _{\min }(A)\).” A boundary/continuity refinement strengthens this to \(B_{\det }(\lambda _{\min }(A)){\gt}0\) too, given continuity and a no-common-eigenvalue hypothesis at \(\lambda _{\min }(A)\) itself — the item’s full “\(\lambda _{\min }(A){\lt}\lambda _{\min }(B)\)” claim.
Honest boundary, both. Neither file defines Hermitian matrices, their characteristic polynomials, or their eigenvalues, and neither connects the abstract ‘A_det‘/‘B_det‘/‘f‘ to actual Matrix.det of a Hermitian matrix pencil — that identification (“\(z\) is an eigenvalue of Hermitian \(M\) iff \(\det (M-zI)=0\)”) is standard and left as the connecting step for whichever future file applies these lemmas to the real parity blocks.
Item 9cc1e2f8, flagged since the sixth-pass write-up as the natural next target because it needs genuine monotonicity/IVT reasoning, not just block-matrix algebra. If \(g\) is continuous and strictly increasing on an open interval \((a,b)\), tends to \(-\infty \) approaching \(a\) from the right, and to \(+\infty \) approaching \(b\) from the left, then \(g\) has exactly one zero in \((a,b)\) — via IsPreconnected.intermediate_value_Iii for existence and StrictMonoOn.injOn for uniqueness. This is the fully general core behind “the secular equation \(f(z)=0\) has exactly one root in each gap \((\alpha _j,\alpha _{j+1})\),” stripped of the specific rational-function structure.
Honest boundary. Does not construct \(f(z)=\sum _j c_j/(\alpha _j-z)\) from the matrix data at all, and does not verify this specific \(f\) satisfies the three hypotheses on each interval \((\alpha _k,\alpha _{k+1})\) — the per-term Finset-sum monotonicity and limit bookkeeping (one pole term dominating, the rest bounded near the endpoints) is the remaining connecting step for a future pass.
Two of the remaining three were also closed the same session:
Item 68566b83. An integral over \([0,\infty )\) of an everywhere-positive integrable integrand is strictly positive — via MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae, reduced to the integrand’s support meeting \([0,\infty )\) in a set of positive (here infinite) Lebesgue measure. Once \(k(t)=\operatorname {Re}(\eta ^*e^{-tA}e_0)\) and the integral is identified with \(\operatorname {Re}(\eta ^*(A-zI)^{-1}e_0)\) (the item’s separate Laplace-resolvent identity, not attempted), this is exactly “cross-heat positivity forces cross-resolvent positivity.”
Item 4d97d8eb. A numerator with a finite limit divided by a denominator whose norm blows up tends to zero — the reusable fact behind “\(q^*(x_i)=q_i\)” for the barycentric Pick interpolant \(q^*(z)=B(z)/A(z)\), since \(B(z)-q_iA(z)\) stays finite at \(x_i\) (the \(k=i\) pole term cancels identically, \(q_i-q_i=0\)) while \(\| A(z)\| \to \infty \) there.
Honest boundary, both: neither defines the matrix exponential/resolvent or the Pick matrix \(R\)/barycentric functions \(A,B,q^*\) themselves; the derivative-matching claim \(q^{*\prime }(x_i)=d_i\) and the \(q^*(\infty )\) limit remain untouched. Only d1aec733 (positive commuting metric \(\Leftrightarrow \) residue positivity) is left ready — noted this pass as carrying a real subtlety (the forward/converse formulas for \(g_j\) use a plain square vs. a modulus-square of \(u_j^*e_0\), so \(g_j\) real is not immediate and needs care).
A second self-correction, same session. Re-checking the Suzuki-Herglotz thread’s items directly (rather than repeating the same by-thread-name mistake corrected above) found one more quick win:
Item dcebf59f. With \(A(z):=(z-i)I(z)\), \(B(z):=(z+i)I(-z)\) for an arbitrary function \(I:\mathbb {C}\to \mathbb {C}\), \(A(-z)=-B(z)\) and \(B(-z)=-A(z)\) follow purely algebraically from the definitions (no properties of \(I\), the operator \(T\), or the reflection \(R\) needed), hence \(W_0:=A+B\) is odd, \(W_\pi :=A-B\) is even, and \(\hat m(z):=-i\, W_0(z)/W_\pi (z)\) is odd. Costs nothing: the item’s own formulas already reduce this layer entirely to algebra once expressed through the same \(I\).
Honest boundary. Does not define \(T\), \(R\), \(v_+=T^{-1}e^x\), \(v_-=T^{-1}e^{-x}\), or \(I(z)=\int v_+(x)e^{izx}dx\), and does not touch the item’s final Herglotz/Livsic representation claim — confirmed blocked above.
Sharpening the last open Weil-Parity item. d1aec733 ("Positive commuting metric equivalent to residue positivity") had been flagged only as "carrying a subtlety." Made precise:
With \(c:=vw\), \(g:=v/w\) (the item’s own \(c_j\), \(g_j\) formulas for \(v=\eta ^*u_j\), \(w=u_j^*e_0\)), \(c=g w^2\) unconditionally — a plain complex square, not the modulus square \(|w|^2\) the item’s converse direction uses for the same quantity. The two agree only when \(w\) is real (witnessed concretely: \(w=i\) gives \(w^2=-1\ne 1=|i|^2\)).
Suzuki-Herglotz, item 1c684543: the shifted logarithmic-derivative transfer, new session. Flagged tractable at the end of the previous pass (plain complex-analysis order-of-vanishing, not Herglotz-dependent).
Item 1c684543. For holomorphic \(F\) and scalar \(\lambda \), put \(D_\lambda (s)=F'(s)-\lambda F(s)\), \(R_\lambda (s)=F(s)/D_\lambda (s)\). Writing a zero \(\rho \) of \(F\) of multiplicity \(m=k+1\ge 1\) as \(F(z)=(z-\rho )^{k+1}g(z)\) (\(g\) analytic, \(g(\rho )\ne 0\)): \(D_\lambda (z)=(z-\rho )^k w(z)\) with \(w(z):=(k+1)g(z)+(z-\rho )(g'(z)-\lambda g(z))\) (), and \(w(\rho )=(k+1)g(\rho )\ne 0\) (). Hence \(R_\lambda (z)/(z-\rho )\to 1/(k+1)\) as \(z\to \rho \) (\(z\ne \rho \)) — the item’s own stated asymptotic \(R_\lambda (s)=(s-\rho )/m+O((s-\rho )^2)\), i.e. a genuine simple zero at \(\rho \) for every finite \(\lambda \); and \(R_\lambda (z)\to 0\) as \(z\to \rho \) (), the "zeros of \(R_\lambda \) are (among) the zeros of \(F\)" half of the item’s conclusion.
Honest boundary. Does not instantiate \(F=\xi \) (Mathlib’s completedRiemannZeta) — a direct application once \(\xi \)’s zeros are known simple with the right local model, not attempted this pass. Does not prove the global "exactly the zeros of \(F\), no others" claim (needs \(D_\lambda \) controlled away from \(F\)’s zeros too, a separate global argument); what’s proved is the precise local fact at each individual zero, the item’s own named content ("the exact divisor fact").
Not a claim the underlying mathematics is wrong in its intended (presumably real-symmetric) setting — only that the queue item’s abstract phrasing is underspecified at exactly this point, worth flagging back to the research source rather than silently patched over or forced through.
Prime-Scattering, item be59ab82: the prime-contraction unitarity locus. On \(\ell ^2(\text{primes})\), the positive injective diagonal contraction \(Ae_p=p^{-1/2}e_p\); for \(\Delta =2s\), the Euler one-particle operator \(A^\Delta e_p=p^{-s}e_p\). The item’s central claim: \(A^{\Delta -1}\) is unitary iff \(\operatorname {Re}\Delta =1\) (equivalently \(\operatorname {Re}s=1/2\)).
For any prime \(p\) and \(\Delta \in \mathbb {C}\): \(|p^{-(\Delta -1)/2}|=1\) iff \(\operatorname {Re}\Delta =1\) — the full iff, both directions, at a single eigenvalue.
On \(\operatorname {Re}\Delta =1\), the diagonal operator for \(A^{\Delta -1}\) is unitary: exact \(\ell ^2\)-norm preservation () plus a genuine two-sided inverse via the conjugate weight, both compositions equal to the identity operator ().
Honest boundary. The operator-level statement is the "if" direction only — the genuine iff is proved at the eigenvalue level (Theorem 24.11); promoting the converse (unitary \(\Rightarrow \operatorname {Re}\Delta =1\)) to the operator itself needs an explicit single-support basis vector \(e_p\in \ell ^2(\text{primes})\), not built this pass. Polar decomposition \(A^\Delta =A^{\operatorname {Re}\Delta }\cdot A^{i\operatorname {Im}\Delta }\) is not formalized. The trace-class-region identity \(\det (I-A^{2s})=\prod _p(1-p^{-s})=\zeta (s)^{-1}\) and the optional Fock-space trace formula are not attempted — Mathlib has no Schatten-class/trace-class operator infrastructure at all (confirmed absent by direct search of the pinned Mathlib source), which blocks both outright.
Prime-Scattering, item 189645c2: BLOCKED. "Critical-line prime semigroup is exactly S3 but not S2 and det3 captures repetitions \(m\ge 3\)" needs Schatten-class membership and the regularized \(\det _3\) Fredholm determinant — the same gap above, confirmed a second time (a targeted search for Fredholm in the pinned Mathlib source returns exactly one hit, a bare TODO comment noting Fredholm operators do not exist yet).
Prime-Scattering, item 0452a4c4: the characteristic-function S-matrix. On \(\ell ^2(\text{primes})\), with \(Le_p=(\log p)e_p\), \(A=e^{-L/2}\), \(U_t=e^{-itL}\), defines \(S(t)=(U_t-A)(I-AU_t)^{-1}\), asking for the Sz.-Nagy/Foias Blaschke characteristic-factor formula at each prime.
For real \(a\) with \(|a|{\lt}1\) and \(w\in \mathbb {C}\) with \(|w|=1\), the Blaschke factor \((w-a)/(1-aw)\) has modulus exactly \(1\).
For every real \(t\): \(\left|\dfrac {p^{-it}-p^{-1/2}}{1-p^{-1/2-it}}\right|=1\) at every prime \(p\) (), and the diagonal operator built from this weight on \(\ell ^2(\text{primes})\) is unitary (reusing directly).
Honest boundary. \(R(t)=U_t^*S(t)\) and its Schatten-class membership (\(R(t)-I\in S3\)) are not formalized — blocked by the same Schatten-class gap as item 189645c2. The finite Euler "shadow determinant" identity \(\det R_P(t)=\zeta _P(1/2+it)/\zeta _P(1/2-it)\) is not attempted for the same reason. The literal operator constructions \(U_t\), \(A\), \(S(t)\) as \(e^{-L/2}\)/\(e^{-itL}\) are not built; only the item’s own closed-form diagonal weight is used directly.
Suzuki-Herglotz, item 2e8ff61e: the shifted-kernel reduction. On \(L^2_0(-a,a)\), \(K_a=(-\Delta _N)^{-1}\) has kernel \(N_a(x,y)=(x^2+y^2)/(4a)-|x-y|/2+a/6\). The item’s claim: for mean-zero \(u\), \(K_a u\) reduces to the shift-kernel convolution \(C_{-|\cdot |/2}u\) up to the mean-zero projection \(P_a\) — the \(x^2\) and \(a/6\) terms of \(N_a\) vanish against \(\int u=0\), and the \(y^2\) term is an \(x\)-independent constant removed by \(P_a\).
For \(u\) integrable on \((-a,a)\) with \(\int _{-a}^{a}u=0\):
i.e. the two integral operators differ by the single \(x\)-independent constant \(\int y^2/(4a)\cdot u(y)\, dy\) — exactly the item’s own claimed reduction, as a pointwise integral identity. Pure intervalIntegral linearity plus ring on the kernel’s algebraic decomposition; no functional-analytic machinery needed for this half.
Honest boundary. The operator-level statement (\(K_a\) built as the genuine inverse Neumann-Laplacian, \(P_a\) a literal orthogonal projection) is not constructed — only the kernel-integral algebra above, the identity’s real content. The item’s second half — \((|x|)''=2\delta _0\) giving \(\widehat{|x|}(z)=-2/z^2\), hence \(\hat{k}_\lambda (z)=z^{-2}[\xi '/\xi (1/2-iz)-\lambda ]\) — needs tempered-distribution theory (derivatives and Fourier transform on the dual of Schwartz space), confirmed absent from the pinned Mathlib source (only the Schwartz test-function space itself and the Fourier transform on Schwartz functions exist, not the dual distribution space). Not attempted; the full transfer identity \(S_{a,\lambda }=G_a-\lambda K_a=P_aC_{g+\lambda |\cdot |/2}P_a\) is therefore not assembled either.
Prime-Fisher/Hankel thread: unconditional strict positivity (ported from GPPVerify2). 25 files ported from GoldenPhysicsProject/GPPVerify2 (Codex’s parallel Lean repo) to bring this repo’s proved-result coverage up to par with it. Route: finite weighted polynomial Gram positivity \(\to \) a polynomial-summability layer for the arithmetic prime-gas measure \(\to \) an unconditional all-order strict Hankel/Gram positivity theorem, via a prime-power root-escape witness.
For every \(N\) and every nonzero real polynomial of degree \(\le N\), the weighted polynomial Gram sum over the arithmetic Fisher measure on \(\{ \log p^k\} \) is strictly positive, unconditionally — via the prime-power witness \(2,4,8,\dots ,2^{N+1}\): all carry von-Mangoldt weight \(\log 2\) at pairwise distinct log-support points \((k{+}1)\log 2\), so no nonzero degree-\(N\) polynomial can vanish on all \(N{+}1\) of them.
Alongside, a parallel zeta-Gibbs thermodynamic route proves strict Fisher-information/ heat-capacity monotonicity and a strict third-cumulant sign (, ), and a two/three/four-point finite covariance-determinant positivity chain ().
Honest boundary. Not ported this pass: the extension of this positivity to genuine countable, normalized probability measures (not just finite truncations). Its central lemma — a 5-moment discriminant identity across a triple finite sum — does not close under this repo’s pinned Mathlib (ring leaves an unsolved goal after full sum-distribution); confirmed this is not a porting artifact, as the identical proof fails to close from GPPVerify2’s own current source verbatim. Not attempted further rather than forced through with an unverified gap.