LogicComplexAnalyticSubstrateCert
plain-language theorem explainer
The certificate structure records an equivalence between recovered complex numbers and standard complexes together with transport identities for the Riemann zeta function, its completed form, Euler-product convergence when the real part exceeds one, and the completed functional equation. Analysts bridging logic constructions to classical analytic number theory cite the certificate when invoking standard zeta properties on recovered inputs. It is assembled as a direct record of the five compatibility conditions.
Claim. Let $L$ be the recovered complex line. A certificate consists of a bijection $L ≃ ℂ$ such that the logic Riemann zeta equals the standard Riemann zeta after transport, the completed logic zeta equals the standard completed zeta after transport, the Euler-product partial sums converge to the logic zeta whenever the transported real part exceeds one, and the completed logic zeta satisfies the functional equation under the map $s ↦ 1 - s$.
background
The module supplies a compatibility layer between recovered complex numbers (pairs of recovered reals) and Mathlib's ℂ. Transport maps convert between the two lines componentwise on real and imaginary parts. Logic Riemann zeta and completed zeta are obtained by composing the standard functions with the transport to the Mathlib line. This follows the explicit Phase 2 decision to retain Mathlib's analytic substrate rather than rebuild contour integration or holomorphy on the recovered line.
proof idea
The declaration is a structure definition that enumerates the five required fields: carrier equivalence, zeta transport identity, completed-zeta transport identity, Euler-product limit statement, and completed functional equation. No separate proof is attached; the structure serves as a container for these properties.
why it matters
The certificate is instantiated to supply the analytic substrate for the recovered-complex Mellin bridge and the theta-zeta bridge. It realizes the Phase 2 commitment to perform all analytic operations on the standard complex plane while preserving logic-derived zeta statements through transport. The construction supports passage from the forcing chain and self-reference axioms to analytic number theory without redeveloping complex analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.