logicRiemannZeta
plain-language theorem explainer
The definition supplies the Riemann zeta function on recovered complex numbers by transporting each input to the standard complex line and invoking the classical zeta there. Number theorists working inside the Recognition framework cite it to import Mathlib analytic results without rebuilding contour integration or holomorphy. The implementation is a direct one-line composition with the embedding map.
Claim. For a recovered complex number $s$, define the logic Riemann zeta function by $smapsto zeta_C( iota(s) )$, where $iota$ is the embedding of the recovered complex into the standard complex numbers and $zeta_C$ is the Riemann zeta function on the standard complex line.
background
LogicComplex is the structure whose fields are a pair of recovered reals, one for the real part and one for the imaginary part. The transport map toComplex applies the real embedding to each component, yielding an element of Mathlib's complex type. The module establishes a compatibility layer that reuses Mathlib's analytic substrate for all zeta operations rather than redeveloping complex analysis inside the recovered logic. The upstream zeta abbreviation is the arithmetic zeta function on positive integers, which the transport makes available on recovered inputs.
proof idea
This is a one-line wrapper that applies the transport toComplex to the input and then invokes the standard Riemann zeta function.
why it matters
It supplies the zeta function required by the analytic substrate certificate, which records that every zeta evaluation occurs through the equivalence to Mathlib complexes. The same definition is used by the Euler-product limit theorem on recovered inputs and by the completed-zeta transport. It directly implements the phase-2 decision stated in the module documentation to avoid redefining holomorphy or contour integration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.