logicCompletedRiemannZeta_fromComplex
plain-language theorem explainer
The theorem equates the logic-form completed Riemann zeta on a transported complex input with the standard completed zeta function. Analysts deriving zeta identities inside the Recognition framework cite it to justify mixing recovered-complex statements with Mathlib analytic tools. The proof is a one-line simplification that unfolds the wrapper definition of logicCompletedRiemannZeta.
Claim. For every $s$ in the complex numbers, the completed Riemann zeta function read on the recovered complex obtained by embedding $s$ equals the standard completed Riemann zeta evaluated at $s$.
background
The module supplies a thin compatibility layer so that recovered-complex statements can invoke Mathlib's analytic substrate without redefining holomorphy or contour integration. LogicComplex stores real and imaginary parts via the fromReal embedding. The map fromComplex sends a Mathlib complex to LogicComplex by applying fromReal componentwise. The definition logicCompletedRiemannZeta then converts its LogicComplex argument back via toComplex before calling the standard completedRiemannZeta.
proof idea
The proof is a one-line term-mode simplification that unfolds the definition of logicCompletedRiemannZeta. The resulting expression completedRiemannZeta (toComplex (fromComplex s)) reduces to the right-hand side by the round-trip identity already registered as a simp lemma in the transport layer.
why it matters
The result completes the transport bridge for the completed zeta function, allowing Recognition statements to inherit Mathlib's analytic lemmas without duplication. It sits inside the LogicComplexCompat layer that Phase 2 explicitly chose to keep the analytic substrate external. No downstream uses are recorded yet, so its role in explicit Euler-product or functional-equation derivations remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.