logicComplexAnalyticSubstrateCert
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove holomorphy or contour integration inside the recovered complex type.
- Does not derive new analytic identities beyond transport of existing ones.
- Does not address convergence of the Euler product outside Re(s) > 1.
- Does not extend the certificate to L-functions other than the Riemann zeta.
Lean usage
recoveredComplexMellinBridge_of_admissible kernel pkgformal statement (Lean)
84def logicComplexAnalyticSubstrateCert : LogicComplexAnalyticSubstrateCert where
85 carrier_equiv := equivComplex
proof body
Definition body.
86 zeta_transport := fun _ => rfl
87 completed_zeta_transport := fun _ => rfl
88 euler_product := logicRiemannZeta_eulerProduct_tendsto
89 completed_functional_equation := logicCompletedRiemannZeta_one_sub
90
91end
92
93end LogicComplexCompat
94end Foundation
95end IndisputableMonolith