logicRiemannZeta_fromComplex
Equivalence between the recovered Riemann zeta on LogicComplex inputs and the standard zeta holds via the embedding fromComplex. Number theorists using the Recognition Science complex substrate cite this to transfer known zeta identities without rederiving analytic results. The proof is a one-line simp wrapper that unfolds the definition of the recovered zeta.
claimFor any complex number $s$, the Riemann zeta function read on recovered complex inputs satisfies $ζ_{logic}(ι(s)) = ζ(s)$, where $ι$ embeds standard complexes into the recovered line by componentwise transport of real and imaginary parts and $ζ_{logic}$ is the standard zeta composed with the projection back to Mathlib complexes.
background
The module supplies a compatibility layer that lets statements about recovered complexes (LogicComplex) use Mathlib's ℂ as the analytic substrate. The map fromComplex sends a standard complex z to the recovered line by applying fromReal separately to its real and imaginary parts. The recovered zeta is then defined by composing the standard riemannZeta with the inverse projection toComplex, so that every recovered-complex zeta statement reduces to an ordinary one.
proof idea
The proof is a one-line wrapper that applies simp to the definition of logicRiemannZeta, which directly unfolds the recovered zeta to the standard riemannZeta applied after the projection toComplex.
why it matters in Recognition Science
The result closes the transport gap between the logic-derived complex line and standard complex analysis, allowing zeta identities to be invoked inside Recognition Science foundation statements. It implements the Phase 2 decision to reuse Mathlib's analytic substrate rather than rebuild contour integration or holomorphy. No downstream uses appear yet, but the declaration supports any later zeta-based claims in the completed-zeta ledger or Euler-product work.
scope and limits
- Does not prove analytic continuation or the functional equation on the recovered side.
- Does not address holomorphy or contour integration for other functions.
- Does not supply new numerical evaluations or zero locations.
formal statement (Lean)
36@[simp] theorem logicRiemannZeta_fromComplex (s : ℂ) :
37 logicRiemannZeta (fromComplex s) = riemannZeta s := by
proof body
One-line wrapper that applies simp.
38 simp [logicRiemannZeta]
39