XiOrderBound
plain-language theorem explainer
The declaration defines the proposition that the completed Riemann zeta function satisfies an exponential growth bound of order at most 1 outside a disk of finite radius. Analysts constructing the genus-one Hadamard factorization for this function would cite the statement as the missing order hypothesis. The definition is a direct existential assertion over positive constants C and K that encodes the classical growth estimate.
Claim. There exist positive real constants $C$ and $K$ such that for every complex $s$ with $||s||$ at least $K$, the modulus of the completed Riemann zeta function at $s$ is at most $e^{C ||s||}$.
background
The module HadamardGenusOne supplies the analytic substrate for genus-one Hadamard factorization of entire functions of order at most 1. It works with the elementary Weierstrass factor $E_1(z) = (1-z) e^z$ and proves per-factor norm bounds together with summability of corrections $E_1(z_n)-1$ whenever the squared moduli of the zeros are summable. The local setting is that Mathlib does not yet contain the Hadamard theorem for order-1 functions, so the module isolates the unconditionally provable pieces while flagging three open statements, of which the present definition is the first.
proof idea
The definition directly encodes the order bound as an existential claim over positive reals C and K together with the stated growth inequality on the completed Riemann zeta function. No lemmas or tactics are invoked; the body is a pure abbreviation of the classical analytic condition.
why it matters
This definition marks one of the three open prerequisites listed in the module documentation for completing the genus-one Hadamard factorization of the completed Riemann zeta function. It supplies the order hypothesis needed before the identification of the infinite product with the function up to an exponential factor can be stated. In the Recognition Science framework the bound supports the analytic continuation and functional equation steps that feed the phi-ladder and the T5-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.