logicCompletedRiemannZeta_one_sub
plain-language theorem explainer
The completed Riemann zeta function on recovered complex numbers satisfies the functional equation equating its value at s to its value at 1-s. Analysts assembling the Recognition Science analytic substrate would cite this when confirming transport of standard zeta identities. The proof is a one-line simplification that unfolds the logic wrapper and invokes the corresponding Mathlib identity on the transported argument.
Claim. For any recovered complex number $s$, the completed Riemann zeta function on recovered complexes satisfies $Z(1-s)=Z(s)$, where $Z$ is obtained by transporting the argument through the equivalence between recovered complexes and Mathlib's $ℂ$.
background
LogicComplex is the structure whose real and imaginary parts are recovered reals. The maps fromComplex and toComplex provide the explicit equivalence transporting between this structure and Mathlib's standard $ℂ$. The module establishes a compatibility layer that uses Mathlib's complex analysis as the analytic substrate, with every recovered-complex statement transported through toComplex rather than redeveloped from scratch.
proof idea
The proof is a one-line term-mode wrapper. It applies simp to unfold logicCompletedRiemannZeta and directly invoke the Mathlib lemma completedRiemannZeta_one_sub on the transported value 1 - toComplex s.
why it matters
This theorem supplies the completed_functional_equation field inside the analytic substrate certificate logicComplexAnalyticSubstrateCert. That certificate collects the transport properties required for Phase 2, ensuring zeta operations stay inside Mathlib's $ℂ$ substrate. It thereby confirms preservation of the standard functional equation under the recovery map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.