logicCompletedRiemannZeta
plain-language theorem explainer
The declaration defines the completed Riemann zeta function on recovered complex numbers by transporting the input through toComplex and invoking the standard Mathlib completedRiemannZeta. Researchers bridging logic-derived complexes to analytic number theory in the Recognition Science setting would cite it when moving zeta identities onto the LogicComplex substrate. The definition is a direct one-line wrapper that performs the transport and delegates the analytic evaluation.
Claim. For a recovered complex number $s$, the completed Riemann zeta function is defined by $s' = $ toComplex$(s)$ followed by the standard completed zeta: $logicCompletedRiemannZeta(s) := completedRiemannZeta(s')$.
background
LogicComplex is the structure whose fields are a pair of LogicReal values (real and imaginary parts). The map toComplex converts each LogicReal component via toReal into the corresponding real and imaginary parts of a Mathlib ℂ value. This supplies the explicit transport required by the module's Phase 2 decision to treat Mathlib ℂ as the analytic substrate rather than redeveloping contour integration or holomorphy on a separate stack.
proof idea
One-line wrapper that applies toComplex to the LogicComplex argument and then calls completedRiemannZeta.
why it matters
The definition supplies the completed zeta on LogicComplex inputs and is invoked by downstream results including logicCompletedRiemannZeta_one_sub, logic_completed_zeta_functional_equation, and the LogicComplexAnalyticSubstrateCert structure. It completes the transport step needed for the theta/zeta Mellin bridge and the phase-4 certificates in ZetaFromTheta, ensuring all analytic zeta operations remain inside Mathlib ℂ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.