GPPVerify now has 881 Lean modules and builds with zero sorry and zero custom axioms. The work this round is the arithmetic and operator structure underneath the Riemann program: the Euler factor of each prime as a scattering channel, the finite geometry of divisors, and exact thresholds for where products over primes converge.
The strongest new pieces
In the centered coordinate z = s − ½ the two half-flips z ↦ −z and z ↦ z̄ generate the quartet {±δ ± iγ}, and RH is equivalent to the vanishing of the odd part of every zero, stated against Mathlib’s own Riemann Hypothesis.
Each Euler factor is a Poisson kernel and each prime is a Blaschke factor. The von Mangoldt current Σ (log p) p−m/2 cos(m t log p) is exactly half of the channel’s group delay above its free baseline log p.
The raw delay of a prime channel is strictly positive, while the vacuum-subtracted excess is positive at θ = 0 and negative at θ = π: positivity, then background subtraction, then an indefinite object.
The second-order determinant fails and the third-order one works at σ = ½. After removing the first k − 1 repetition harmonics the prime phase converges normally in the strip |Im T| < ½ − 1/k, which is |Im T| < 1/6 for k = 3.
The SU(1,1) transfer of a prime has discriminant (Tr G)² − 4 = 4/(p − 1), the finite-place mass-square. The thermofield covariance is ½G−2, orientation reversal preserves the class, the sewn pair has discriminant exactly 0, and p = 5 is the golden case.
Subgroup states of ℤ/Nℤ have Gram matrix gcd(d,e)/√(de). The finite Fourier transform exchanges vd and vN/d, the index-p overlap is p−1/2, and the Möbius parity vector is an eigenvector with eigenvalue ∏(1 − p−1/2).
On ℤ/pKℤ the Gram matrix of the nested subgroups is r|a−b| with r = p−1/2, and the Euler factor is the Green function of that chain. The centered divisor coordinate is reflected by Fourier duality, ℓ ↦ −ℓ.
∫₀^∞ xσ−1/(1 + x) dx = π / sin πσ; the zeta Gibbs ensemble has ε log N → Exp(1) at the level of Laplace transforms; and the Haar valuation law is normalized with mean 1/(p − 1).
What the kernel closed
These are theorems about why a route cannot work, and they are as useful as the positive results because each route is now explored once.
- The prime inner channels do not globalize. Every prime channel vanishes at the same point i/2, and the zeros 2π/log p + i/2 accumulate there, so no nonzero analytic function can carry all of them; the Blaschke sum over primes diverges.
- Static Bost–Connes projections are not a frame. The vector δ₁ − δ1+pK−1 is annihilated by every weighted sum of divisibility projections and their Fourier duals, for every choice of weights.
- Local contraction does not globalize. One coherent mode has odd/even ratio exactly |r| < 1, but two distinct modes have a strictly negative reflection determinant.
- No diagonal reweighting of the prime Hilbert space makes the primitive current a vector and the all-ones evaluation bounded at once.
- The raw critical character has a dual norm that contains a Mertens-strength Möbius sum, so asking for it to be small is another form of the target.
The RH frontier, unchanged and sharper
The finite criterion stands:
Every prime, taken alone, is passive and positive. The obstruction lives in the interference between primes and in the archimedean place, which is why the next constructions are global: a completion that acts before the infinite product is formed, not after.