-
CriticalLine.lean, Reality.lean, and ZeroTopology.lean connect actual
zeta zeros to a continuous real xi function. Failure to have zeros above
every height implies a strict eventual sign.
-
Theta.lean, ThetaCusp.lean, ThetaDecay.lean, and ThetaPath.lean
establish the theta identities, bounds, and decay of the actual cusp path
faster than each natural power of the boundary distance.
-
ExponentialFourier.lean and ThetaTransform.lean identify completed zeta
with the Fourier transform of the corrected theta kernel. The pole terms
are evaluated explicitly.
-
ThetaKernelBounds.lean and ThetaContour.lean prove strip bounds,
horizontal integrability, the contour shift, and exponential decay of
completed zeta. HardyWeight.lean obtains absolute convergence of each
interior weighted integral.
-
ThetaInversion.lean proves the exact cosh-transform identity by Fourier
inversion on a shifted line.
-
FiniteDifference.lean, FiniteDifferenceFlat.lean, and
FiniteDifferenceIntegral.lean prove cosine cancellation, positivity,
cusp difference limits, and interchange of iterated differences with the
actual zeta integral.
-
HardyDifferenceLimit.lean proves the full normalized difference integral
tends to zero. FiniteDifferenceCompact.lean proves convergence on each
compact interval by a continuous extension of the normalized kernel.
-
TailComparison.lean compares a positive tail interval with the initial
interval. Its compact limits contradict geometric growth using
MomentAlgebra.not_geometric_domination.
-
Hardy.lean applies this contradiction to both possible signs, proves
zerosAboveEveryHeight, and derives the exact frozen infinitude statement.