Paper deep dive
More than 83.69% of the zeros of the Riemann zeta function are distinct
Kristian Muri Knausgård
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:The lower asymptotic proportion of distinct nontrivial zeros of the Riemann zeta function, counted with multiplicity, is at least $0.8369928814\ldots$. The previous bound was $0.83625\ldots$. As in the proof of that bound, an unconditional version of Montgomery's pair-correlation theorem gives an asymptotic energy estimate. The new ingredient is a short matrix inequality with a free clipping parameter. It strengthens the lower bound for this energy in terms of the number of distinct zeros. The gain is a nonnegative correction from overlaps between different nearby zeros on the critical line, which is retained even when some of these zeros are double. The matrix inequality, the threshold lemma, the block dichotomy, the counting assembly and the exact arithmetic are proved formally in Lean 4. The constant relies on a computer-assisted local inequality from recent work that has not yet been refereed. That computation was re-run independently, and every imported input is listed. This paper is primarily an experiment in AI-assisted mathematical research (Section 4).
Tags
Links
- Source: https://arxiv.org/abs/2609.33043v1
- Canonical: https://arxiv.org/abs/2609.33043v1
Trouble viewing inline? Open PDF directly →
Full Text
24,358 characters extracted from source content.
Expand or collapse full text
More than 83.69%83.69\% of the zeros of the Riemann zeta function are distinct Kristian Muri Knausgård Email address: kristianmk@ieee.org Date: 26 September 2026 Abstract. The lower asymptotic proportion of distinct nontrivial zeros of the Riemann zeta function, counted with multiplicity, is at least 0.8369928814…0.8369928814…. The previous bound was 0.83625…0.83625…. As in the proof of that bound, an unconditional version of Montgomery’s pair-correlation theorem gives an asymptotic energy estimate. The new ingredient is a short matrix inequality with a free clipping parameter. It strengthens the lower bound for this energy in terms of the number of distinct zeros. The gain is a nonnegative correction from overlaps between different nearby zeros on the critical line, which is retained even when some of these zeros are double. The matrix inequality, the threshold lemma, the block dichotomy, the counting assembly and the exact arithmetic are proved formally in Lean 4. The constant relies on a computer-assisted local inequality from recent work that has not yet been refereed. That computation was re-run independently, and every imported input is listed. This paper is primarily an experiment in AI-assisted mathematical research (Section 4). 1. Introduction The Riemann zeta function has infinitely many nontrivial zeros ρ=σ+iγρ=σ+iγ with 0<σ<10<σ<1. It is conjectured that every zero is simple, meaning not repeated. Let N(T)N(T) count the zeros with 0<γ≤T0<γ≤ T, with multiplicity, and let Nd(T)N_d(T) count the distinct ones. If all zeros were simple, then Nd=N_d=N. Montgomery’s pair-correlation method [8] gives lower bounds for such proportions. An argument discovered by Claude (Anthropic) [4] and verified by Alpöge and Furman [1], together with a second proof by Lamzouri [6], shows unconditionally that lim infNd(T)/N(T)≥0.8362503518… N_d(T)/N(T)≥ 0.8362503518…. Wang [12] improved this by about 3⋅10−83· 10^-8. The purpose of this paper is to prove the following bound. Theorem 1. lim infT→∞Nd(T)N(T)≥q:=1626011929802919426831050000=0.83699288145242… _T→∞ N_d(T)N(T)\ ≥\ q:= 1626011929802919426831050000=0.83699288145242… The idea. Rescale the zeros so that their mean spacing is one: a zero ρ=12+iγρ= 12+iγ on the critical line gets the coordinate yρ=γlogT/(2π)y_ρ=γ T/(2π). Fix an even probability density f=η2f=η^2 on [−12,12][- 12, 12], and attach to this zero the wave packet Fyρ(u)=η(u)e2πiuyρ∈L2(−12,12).F_y_ρ(u)=η(u)\,e^2π iuy_ρ∈ L^2 (- 12, 12 ). These are unit vectors, and ⟨Fy,Fy′⟩=f^(y−y′) F_y,F_y = f(y-y ), where f^(x)=∫f(u)e−2πixuu f(x)= f(u)e^-2π ixu\,du. The overlap is 11 for coincident zeros, close to 11 for nearby zeros, and small for zeros far apart. Section 3 uses a smoothed version of these vectors, labelled there by zρ=−yρz_ρ=-y_ρ. Zeros off the critical line come in pairs placed symmetrically about the line. Each pair contributes a Hermitian term with at most one positive eigenvalue, so the construction needs no assumption about where the zeros lie. Summing the projections onto the vectors above and these pair terms, with multiplicity, gives an operator A with trA=NtrA=N. The energy E=trA2E=trA^2 is a pair sum over all zeros. For ordered pairs (ρ,ρ′)(ρ,ρ ) on the critical line, including ρ=ρ′ρ=ρ , the summands are f^(yρ−yρ′)2 f(y_ρ-y_ρ )^2, counted with multiplicity. The full identity, including off-line zeros, is given in Section 3. Montgomery’s pair-correlation theorem, in its unconditional form [3], computes this energy asymptotically: for the smoothed operator, E=(Cε+o(1))NE=(C_ +o(1))N with Cε→C=∫f2+∬|s−t|f(s)f(t)stC_ → C= f^2+ |s-t|f(s)f(t)\,ds\,dt, and C≤2−H<2C≤ 2-H<2 for the window used here (Proposition 5). A zero on the critical line of multiplicity ν contributes ν to the trace and ν2ν^2 to the diagonal part of the energy sum. A double zero contributes 44 to this diagonal part, whereas two distinct simple zeros contribute 22, with an additional mutual term 2f^(y−y′)22 f(y-y )^2 that is small when they are far apart. Both configurations contribute 22 to the trace. Linear algebra turns this into E≥3N−2NdE≥ 3N-2N_d, hence lim infT→∞Nd/N≥3−C2 _T→∞N_d/N≥ 3-C2. The Montgomery–Taylor window gives the previous bound this way. The window used here gives up about 2⋅10−52· 10^-5 of that baseline in exchange for a larger gain below. The improvement adds a nonnegative defect term to this inequality. The defect measures how far the Gram matrix U=(f^(yi−yj))U=( f(y_i-y_j)) of the distinct on-line zeros of multiplicity one or two is from the identity, and nearby zeros make it positive. The total spread of these points is at most N+o(N)N+o(N). A certified local inequality (Proposition 6) relates the spread to the squared overlaps: for any seven consecutive points, a weighted sum of their squared overlaps plus a multiple of their spread is at least a fixed positive constant. As a result, the defect is at least a fixed amount per point, minus a penalty proportional to how widely the points are spread. Recent simple-zero records [2, 11, 9, 10] use such a defect for simple zeros. Counting distinct zeros requires keeping the defect when double zeros are present too, and Theorem 2 does exactly that. 2. The matrix inequalities For Hermitian X and real f write trf(X)=∑if(λi(X))trf(X)= _if( _i(X)). Write X⪯YX Y when Y−XY-X is positive semidefinite. For real c and τ≥0τ≥ 0 let φc(x)=x2,x≤c,2cx−c2,x>c,Ψτ(x)=(x−1)2,x≤1+τ,2τ(x−1)−τ2,x>1+τ. _c(x)= casesx^2,&x≤ c,\\ 2cx-c^2,&x>c, cases _τ(x)= cases(x-1)^2,&x≤ 1+τ,\\ 2τ(x-1)-τ^2,&x>1+τ. cases Both functions are C1C^1 with nondecreasing derivative, hence convex on ℝR. Theorem 2 (Mixed-multiplicity Gram inequality). Let U be a Hermitian l×l× l matrix with unit diagonal, let D=diag(di)D=diag(d_i) with 1≤di≤21≤ d_i≤ 2, and let G=D1/2UD1/2G=D^1/2UD^1/2. If τ≥0τ≥ 0 and c≥max(1+τ, 2+τ/2)c≥ (1+τ,\,2+τ/2), then trφc(G)−trD2≥trΨτ(U).tr _c(G)-trD^2\ ≥\ tr _τ(U). Lemma 3. If G,BG,B are Hermitian and B⪯2cIB 2cI, then trφc(G)≥tr(BG)−14trB2tr _c(G) (BG)- 14trB^2. In control-theoretic terms, Lemma 3 is a dual certificate. Every matrix B that satisfies the linear matrix inequality B⪯2cIB 2cI yields a lower bound on trφc(G)tr _c(G), and the bound is attained at B=2min(G,cI)B=2 (G,cI). The proof of Theorem 2 exhibits one admissible B. Proof of Lemma 3. In an eigenbasis of G, tr(BG)=∑biiλitr(BG)=Σ b_i _i and trB2≥∑bii2trB^2≥Σ b_i^2, with bii≤2cb_i≤ 2c. It suffices to show bλ−14b2=λ2−(λ−b2)2≤φc(λ)bλ- 14b^2=λ^2-(λ- b2)^2≤ _c(λ) for b≤2cb≤ 2c. If λ≤cλ≤ c this is clear. If λ>cλ>c, then λ−b2≥λ−c>0λ- b2≥λ-c>0, and the claim follows. ∎ Proof of Theorem 2. Let C be U−IU-I with each eigenvalue μ replaced by min(μ,τ) (μ,τ), so that ⪯τIC τ I. Put M=D−1/2D−1/2M=D^-1/2CD^-1/2 and B=2D+2MB=2D+2M. Then B⪯2D+2τD−1⪯2cIB 2D+2τ D^-1 2cI. For the last step, d+τ/d+τ/d is convex on [1,2][1,2], so it is at most max(1+τ,2+τ/2)≤c (1+τ,2+τ/2)≤ c. Using Uii=1U_i=1 and cyclicity, tr(DG)=trD2tr(DG)=trD^2, tr(MG)=tr(U)tr(MG)=tr(CU) and tr(DM)=trtr(DM)=trC. Hence tr(BG)−14trB2−trD2=2tr((U−I))−trM2.tr(BG)- 14trB^2-trD^2=2tr (C(U-I) )-trM^2. Moreover trM2=∑|ij|2/(didj)≤tr2trM^2=Σ|C_ij|^2/(d_id_j) ^2. By Lemma 3, trφc(G)−trD2≥ 2tr((U−I))−tr2=∑μ(2μmin(μ,τ)−min(μ,τ)2),tr _c(G)-trD^2\ ≥\ 2tr (C(U-I) )-trC^2= _μ (2μ (μ,τ)- (μ,τ)^2 ), and each summand equals Ψτ(1+μ) _τ(1+μ). ∎ The counting argument also requires a threshold inequality of the kind used in [4, 1]. The following proof avoids eigenvalue interlacing. For Hermitian X let X±⪰0X_± 0 carry its positive and negative eigenvalues, so that X=X+−X−X=X_+-X_- and X+X−=0X_+X_-=0. Lemma 4. Let P⪰0P 0, let Q be Hermitian with at most b positive eigenvalues, let A=P+QA=P+Q, and let c be real. Then trA2≥2ctrA−2ctrP+trφc(P)−c2btrA^2≥ 2ctrA-2ctrP+tr _c(P)-c^2b. Proof. Write Z=Q−Z=Q_-, so that A=(P−Z)+Q+A=(P-Z)+Q_+. The cross term is 2tr((P−Z)Q+)=2tr(PQ+)≥02tr((P-Z)Q_+)=2tr(PQ_+)≥ 0, since ZQ+=0ZQ_+=0. Hence trA2≥tr(P−Z)2+trQ+2trA^2 (P-Z)^2+trQ_+^2. Also trQ+2≥2ctrQ+−c2btrQ_+^2≥ 2ctrQ_+-c^2b, because x2≥2cx−c2x^2≥ 2cx-c^2. It remains to show tr(P−Z)2+2ctrZ≥trφc(P)tr(P-Z)^2+2ctrZ _c(P). Since φc(p)=p2−(p−c)+2 _c(p)=p^2-(p-c)_+^2, this is trX+2−2tr(XZ)+trZ2≥0trX_+^2-2tr(XZ)+trZ^2≥ 0 with X=P−cIX=P-cI. Now tr(XZ)≤tr(X+Z)tr(XZ) (X_+Z) because tr(X−Z)≥0tr(X_-Z)≥ 0. So the left side is at least tr(X+−Z)2≥0tr(X_+-Z)^2≥ 0. ∎ 3. Proof of Theorem 1 The window. Following [11] (files design.py and kernel.py), put v(u)=cos(2u)+10−9∑j=16κjcos(2πju)(|u|≤12),f=v/∫−1/21/2v,v(u)= ( 2\,u)+10^-9 _j=1^6 _j (2π ju) (|u|≤ 12), f=v /\! _-1/2^1/2v, with (κj)=(3322500,−7609135,1190194,−731476,−1680572,1141360)( _j)=(3322500,-7609135,1190194,-731476,-1680572,1141360). Both v and f vanish outside I=[−12,12]I=[- 12, 12]. On I, v>0v>0 (its minimum there is about 0.750.75), and ∫v=2sin(1/2) v= 2 (1/ 2). Let K(x)=f^(x)=∫f(u)e−2πixuuK(x)= f(x)= f(u)e^-2π ixu\,du, so that K(0)=1K(0)=1 and K2=(v^/v^(0))2K^2=( v/ v(0))^2 is the verifier’s kernel. The operator. Let L=logTL= T and zρ=i(ρ−12)L/(2π)z_ρ=i(ρ- 12)L/(2π) for 0<γ≤T0<γ≤ T. On-line zeros give real zρz_ρ. An off-line zero pairs with 1−ρ¯1- ρ, which has the same multiplicity and the point z¯ρ z_ρ. The function f jumps at ±12± 12, so f∗f f is not twice differentiable, and the smoothing below is necessary. Since f f is smooth and positive on the interior of I, multiplying it by even smooth cutoffs that tend to I1_I and renormalising gives fε=ηε2f_ = _ ^2. Here ηε _ is real, even, smooth and supported inside I, ∫fε=1 f_ =1, dε=‖fε−f‖1→0d_ =\|f_ -f\|_1→ 0 and fε→f_ → f in L2L^2. Put Kε=f^εK_ = f_ and Fz(u)=ηε(u)e−2πiuzF_z(u)= _ (u)e^-2π iuz. With inner products conjugate-linear in the first slot, ⟨Fz,Fw⟩=Kε(w−z¯) F_z,F_w =K_ (w- z). The operator A=∑zνzFz⟨Fz¯,⋅⟩A= _z _zF_z F_ z,· , where νz _z is the multiplicity, is Hermitian. It satisfies trA=NtrA=N and trA2=∑z,wνzνwKε(z−w)2=:EεtrA^2= _z,w _z _wK_ (z-w)^2=:E_ , using that KεK_ is even. All operators act on the finite-dimensional span of the FzF_z. Proposition 5 (analytic input [3, Lemma 5]; computer-assisted bound [11]). Eε=(C(fε)+o(1))NE_ =(C(f_ )+o(1))N, where C(g)=∫g2+∬|s−t|g(s)g(t)C(g)= g^2+ |s-t|g(s)g(t). Moreover C(fε)→C(f)≤2−HC(f_ )→ C(f)≤ 2-H with H=33622852075000000000H= 33622852075000000000. The asymptotic is the unconditional Montgomery theorem [3, Lemma 5] (see also [6, 1]). It applies to real, even, integrable test functions supported in [−1,1][-1,1] and Lipschitz at 00, and it sums over all zeros, on or off the line, with multiplicity. It carries the weight w(ρ−ρ′)=4/(4−(ρ−ρ′)2)w(ρ-ρ )=4/(4-(ρ-ρ )^2). With Rε=fε∗fεR_ =f_ *f_ , (Rε−Rε′/(4L2))∧(x)=(1+π2x2L2)Kε(x)2. (R_ -R_ /(4L^2) ) (x)= (1+ π^2x^2L^2 )K_ (x)^2. At x=zρ−zρ′x=z_ρ-z_ρ the factor is 1−(ρ−ρ′)2/4=1/w(ρ−ρ′)1-(ρ-ρ )^2/4=1/w(ρ-ρ ). Both RεR_ and Rε′R_ are admissible fixed test functions. So applying the lemma to both removes the weight exactly. The Rε′R_ term contributes Oε(N/L2)O_ (N/L^2), and the total error is oε(N)o_ (N). The bound C(f)≤2−HC(f)≤ 2-H is a certified interval enclosure [11]. An independent 40-digit (non-interval) evaluation gives 2−C(f)=0.67245704141454428878…2-C(f)=0.67245704141454428878…, consistent with it. Splitting. Let n1,n2n_1,n_2 count the distinct on-line zeros of multiplicity 1,21,2. Let h count those of multiplicity ≥3≥ 3, and let k count off-line pairs. Then Nd=n1+n2+h+2kN_d=n_1+n_2+h+2k. Let P be the part of A coming from the l=n1+n2l=n_1+n_2 low-multiplicity points yjy_j. Then P=VDV∗P=VDV^* with Vej=FyjVe_j=F_y_j, and U=V∗VU=V^*V has Uij=Kε(yi−yj)U_ij=K_ (y_i-y_j). So P has the nonzero spectrum of G=D1/2UD1/2G=D^1/2UD^1/2. Since φc(0)=0 _c(0)=0, it follows that trφc(P)=trφc(G)tr _c(P)=tr _c(G). Also trP=n1+2n2trP=n_1+2n_2. In Q=A−PQ=A-P, each high point gives a positive rank-one term. Each off-line pair gives ν(vw∗+wv∗)=ν2((v+w)(v+w)∗−(v−w)(v−w)∗)ν(vw^*+wv^*)= ν2 ((v+w)(v+w)^*-(v-w)(v-w)^* ), with v=Fzv=F_z and w=Fz¯w=F_ z, which has at most one positive eigenvalue. Since n+(∑jQj)≤∑jn+(Qj)n_+( _jQ_j)≤ _jn_+(Q_j), Q has at most h+kh+k positive eigenvalues. Fix τ≥0τ≥ 0 and c≥max(1+τ,2+τ/2)c≥ (1+τ,2+τ/2), so that c≥2c≥ 2. Lemma 4 with b=h+kb=h+k and Theorem 2 give Eε≥ 2cN−(2c−1)n1−(4c−4)n2−c2(h+k)+trΨτ(U).E_ \ ≥\ 2cN-(2c-1)n_1-(4c-4)n_2-c^2(h+k)+tr _τ(U). Compare this with 3N−2Nd3N-2N_d. A high point of multiplicity j≥3j≥ 3 leaves (2c−3)j+2−c2≥rh:=6c−7−c2(2c-3)j+2-c^2≥ r_h:=6c-7-c^2, and an off-line pair of multiplicity j≥1j≥ 1 leaves (4c−6)j+4−c2≥rk:=4c−2−c2(4c-6)j+4-c^2≥ r_k:=4c-2-c^2. Hence (1) Eε≥ 3N−2Nd+trΨτ(U)+rhh+rkk.E_ \ ≥\ 3N-2N_d+tr _τ(U)+r_hh+r_kk. The local defect. Proposition 6 (imported, computer-assisted [11]). There are rational wij≥0w_ij≥ 0 with ∑iwi,i+r=2 _iw_i,i+r=2 for r=1,…,6r=1,…,6, such that for all real y0≤⋯≤y6y_0≤…≤ y_6, 12736(y6−y0)+∑0≤i<j≤6wijK(yj−yi)2≥δ:=891200000. 12736(y_6-y_0)+ _0≤ i<j≤ 6w_ijK(y_j-y_i)^2\ ≥\ δ:= 891200000. Take the Gram matrix UBU_B, built with K, of m consecutive points. It is positive semidefinite because f≥0f≥ 0. Summing Proposition 6 over the m−6m-6 windows gives weight at most 22 per pair. Since tr(UB−I)2=2∑i<jK(yj−yi)2tr(U_B-I)^2=2 _i<jK(y_j-y_i)^2, this gives tr(UB−I)2+12736W≥Δm:=(m−6)δtr(U_B-I)^2+ 12736W≥ _m:=(m-6)δ, where W is the total window length. If Δm≤τ2 _m≤τ^2, then trΨτ(UB)+12736W≥Δmtr _τ(U_B)+ 12736W≥ _m. Indeed, if every eigenvalue is at most 1+τ1+τ, then trΨτ(UB)=tr(UB−I)2tr _τ(U_B)=tr(U_B-I)^2. Otherwise one eigenvalue alone contributes at least τ2τ^2, and Ψτ≥0 _τ≥ 0. Replacing K by KεK_ changes each entry by at most dεd_ , so the block changes by at most mdεmd_ in norm. Both blocks are Gram matrices, so their eigenvalues lie in [0,∞)[0,∞), where Ψτ _τ is max(2,2τ) (2,2τ)-Lipschitz. By Weyl’s inequality, trΨτtr _τ changes by at most max(2,2τ)m2dε (2,2τ)m^2d_ . By convexity of Ψτ _τ (the pinching inequality trΨτ(X)≥∑BtrΨτ(XBB)tr _τ(X)≥ _Btr _τ(X_B)), trΨτ(U)tr _τ(U) dominates the sum over any partition into consecutive blocks. Average over the m shifted partitions: • the full blocks over all shifts number at least l−2ml-2m, so the Δm _m terms total at least Δm(l−2m)/m _m(l-2m)/m; • each window lies inside a block for at most m−6m-6 of the shifts, and each gap lies in at most 66 windows, so the W terms total at most 6(m−6)(yl−y1)/(2736m)6(m-6)(y_l-y_1)/(2736m). The result is (2) trΨτ(U)≥al−β(yl−y1)−Om,τ(dε)N−Om(1),a=Δm,β=6(m−6)2736m.tr _τ(U)\ ≥\ a\,l-β\,(y_l-y_1)-O_m,τ(d_ )\,N-O_m(1), a= _mm, β= 6(m-6)2736\,m. Here the spread yl−y1y_l-y_1 is defined to be 00 when l≤1l≤ 1. If no shift has a full block, (2) still holds: its right side is then at most 00 once the constant in Om(1)O_m(1) is taken at least 2Δm2 _m, and trΨτ(U)≥0tr _τ(U)≥ 0. Shifted-block pinching is from [2]. The window-in-block pressure count is from [10]; see also [11, 9]. What is new is the use of both on all distinct points of multiplicity one or two. Constants. Take τ=125τ= 125, c=175c= 175 and m=1298m=1298. Then Δm=28779350000<τ2=14425 _m= 28779350000<τ^2= 14425, a=261635900000a= 261635900000 and β=177788β= 177788. Also rh−a=108298375900000>0r_h-a= 108298375900000>0 and rk−2a=918372950000>0r_k-2a= 918372950000>0. Conclusion. The points yjy_j lie in an interval of length TL/2π=N+O(T)=N+o(N)TL/2π=N+O(T)=N+o(N), and l=Nd−h−2kl=N_d-h-2k. So (1), (2) and Proposition 5 give (2−a)Nd≥(3−C(fε)−β−Om,τ(dε))N+(rh−a)h+(rk−2a)k−o(N).(2-a)N_d\ ≥\ (3-C(f_ )-β-O_m,τ(d_ ) )N+(r_h-a)h+(r_k-2a)k-o(N). Let T→∞T→∞ and then ε→0 → 0. This gives lim infNd/N≥(1+H−β)/(2−a)=q N_d/N≥(1+H-β)/(2-a)=q in exact arithmetic. ∎ 4. Verification and nature of this work Formal proofs. The following are proved in Lean 4 with Mathlib [7]; the source is in the ancillary files: • Lemma 3; • Theorem 2, for all τ≥0τ≥ 0 and c≥max(1+τ,2+τ/2)c≥ (1+τ,2+τ/2); • Lemma 4, in both exact-count and “at most b” forms; • the block dichotomy; • the combination of Lemma 4 and Theorem 2 (the inequality preceding (1)); • the counting assembly leading to (2−a)Nd≥(1+H−β)N−(2-a)N_d≥(1+H-β)N-errors, from explicitly stated hypotheses; • all exact constants. Every theorem depends only on the axioms propext, Classical.choice and Quot.sound. The code contains no sorry. Not formalized: • the operator construction and its reduction to matrices: trP=n1+2n2trP=n_1+2n_2, trφc(P)=trφc(G)tr _c(P)=tr _c(G), and n+(Q)≤h+kn_+(Q)≤ h+k; • the energy asymptotic; • the certified local inequality; • the pinching and block averaging; • the smoothing K→KεK→ K_ . These enter the Lean statements only as explicit hypotheses. Computation. Proposition 6 comes from the Arb-based [5] verifier of [11], commit 1610b97. Its exhaustive search was re-run on separate hardware: 96 shards and 2,168,3702,168,370 interval nodes, all verified. Both table hashes and all pruning counts match the published run. The run record is in the ancillary files. The verifier code was not audited line by line. As noted upstream, this certificate has no tangent-free replay yet: 453,136453,136 of its nodes are certified by a convex-tangent pruner. The enclosure of C(f)C(f) is taken from [11], with the independent check stated above. Status. The analytic inputs [1, 6, 3] and the certificates [2, 11, 9, 10] are recent and mostly not yet refereed. Nature of this work. This paper is primarily an experiment in AI-assisted mathematical research. The arguments, the Lean formalization and much of the text were developed with substantial assistance from AI systems (OpenAI Codex and Anthropic Claude) under the author’s direction. The author defined and steered the research programme, reviewed all steps, and found the τ-generalisation together with OpenAI Codex. The author takes full responsibility for the content. References [1] L. Alpöge and R. Furman, More than two thirds of the zeta zeros are simple and on the critical line, arXiv:2608.13637, 2026. [2] ainta/zeta-simple-zeros, More than 67.3%67.3\% of the zeros of the Riemann zeta function are simple and lie on the critical line, commit 040c5e8, 2026, https://github.com/ainta/zeta-simple-zeros. [3] S. A. C. Baluyot, D. A. Goldston, A. I. Suriajaya and C. L. Turnage-Butterbaugh, An unconditional Montgomery theorem for pair correlation of zeros of the Riemann zeta-function, Acta Arith. 214 (2024), 357–376; arXiv:2306.04799. [4] Claude (Anthropic), More than two thirds of the zeros of the Riemann zeta function lie on the critical line, preprint, 2026, https://w-cdn.anthropic.com/564f962e60643842f5fcb4a17c9dbc8f608f1c37.pdf; Lean artifact in https://github.com/anthropics/formal-math (zeta23). [5] F. Johansson, Arb: efficient arbitrary-precision midpoint-radius interval arithmetic, IEEE Trans. Comput. 66 (2017), 1281–1292. [6] Y. Lamzouri, A new proof that more than 2/32/3 of the zeros of the Riemann zeta function are simple and on the critical line, arXiv:2609.02882, 2026. [7] The mathlib Community, The Lean mathematical library, CPP 2020, 367–381. [8] H. L. Montgomery, The pair correlation of zeros of the zeta function, Proc. Sympos. Pure Math. 24, AMS, 1973, 181–193. [9] Y. Shi, A two-certificate trace–energy deduction for simple zeros of the Riemann zeta function, 2026, https://doi.org/10.5281/zenodo.21926962; repository https://github.com/yuhangshi888/zeta-simple-zeros-673316977, commit 1aeda8e. [10] tawanerguo-cn/zeta-simple-zeros, A certified unconditional 67.3192911473%67.3192911473\% lower bound for simple zeros of the Riemann zeta function, research repository, commit 45149f6, 12 August 2026, https://github.com/tawanerguo-cn/zeta-simple-zeros. [11] trmdy/zeta-simple-zeros-673137, commit 1610b97, 2026, https://github.com/trmdy/zeta-simple-zeros-673137. The seven-term window comes from a multi-model AI session operated by T. Haugland. The certificate used here (pressure 1/27361/2736) is a follow-up retuning directed by V. Ojha with OpenAI Codex (docs/provenance.md). [12] B. Wang, Proportions of the non-trivial zeros of the Riemann zeta function, arXiv:2609.24167, 2026.