logicComplexAnalyticSubstrateCert
plain-language theorem explainer
The declaration builds the Phase 2 certificate that all zeta-function operations on recovered complex numbers are performed inside Mathlib's ℂ via the carrier equivalence. Researchers invoking Mellin transforms or analytic continuation over the logic-derived complexes cite it to justify reuse of standard results. The construction is a direct record instantiation that delegates transport to reflexivity and two prior transport theorems.
Claim. The certificate structure is instantiated so that the carrier map is the equivalence LogicComplex ≃ ℂ, the Riemann zeta on recovered inputs equals the standard zeta after transport, the completed zeta satisfies the same, the Euler product holds for Re(s) > 1, and the completed functional equation is preserved under the map.
background
The LogicComplexCompat module supplies a compatibility layer that treats Mathlib's ℂ as the analytic substrate rather than rebuilding holomorphy or contour integration. Recovered complex numbers are identified with ℂ by the equivalence equivComplex whose toFun is toComplex and whose inverses are witnessed by fromComplex_toComplex and toComplex_fromComplex. The structure LogicComplexAnalyticSubstrateCert packages four fields: the carrier equivalence together with transport equalities for the logic Riemann zeta, the completed zeta, the Euler product, and the functional equation.
proof idea
The definition constructs the record by setting carrier_equiv to equivComplex. The two transport fields are filled by reflexivity because logicRiemannZeta and logicCompletedRiemannZeta are defined by direct transport through toComplex. The euler_product field receives the theorem logicRiemannZeta_eulerProduct_tendsto and the completed_functional_equation field receives logicCompletedRiemannZeta_one_sub.
why it matters
The certificate is consumed by recoveredComplexMellinBridge_of_admissible, which equips any MellinAdmissibleKernel with reflection symmetry over the recovered complex substrate. It completes the explicit Phase 2 decision stated in the module documentation to transport statements rather than redevelop analytic machinery. The step sits between the logic-derived zeta definitions and downstream Mellin-transform work inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.