logicComplexAnalyticSubstrateCert
plain-language theorem explainer
The analytic substrate compatibility certificate for Phase 2 constructs the record confirming that zeta operations on recovered complex numbers transport to standard complex analysis via the carrier equivalence. It is referenced by Mellin transform constructions to validate the substrate choice. The definition assembles the structure from the carrier equivalence together with reflexivity on the transport maps and prior results on the Euler product and functional equation.
Claim. The certificate asserts an equivalence between the logic-derived complex numbers and the standard complex numbers such that the Riemann zeta function on logic complexes equals the standard zeta function after transport to the complex plane, the completed zeta satisfies the same transport, the Euler product limit holds when the real part exceeds 1, and the functional equation is preserved under the substitution sending each complex number to one minus itself.
background
The module creates a compatibility layer so recovered complex numbers can employ standard analytic tools. The local setting is the Phase 2 decision to use the standard complex numbers as the analytic substrate and transport statements through the map to the standard complex numbers rather than redeveloping complex analysis. The structure records that zeta operations occur in the standard complex numbers through the recovered-complex equivalence. It includes the carrier equivalence, transport equalities for the zeta and completed zeta functions, the Euler product tendsto statement, and the functional equation. Upstream results supply the carrier equivalence, which maps via the to-standard-complex map and its inverse with the required inverses, the theorem establishing the Euler product on recovered inputs, and the theorem for the completed zeta functional equation by transport.
proof idea
The definition constructs the certificate by assigning the carrier equivalence field to the equivalence between recovered and standard complex numbers, setting the zeta transport and completed zeta transport fields to the constant reflexivity function, assigning the Euler product field to the theorem on the Euler product tendsto for recovered inputs, and assigning the functional equation field to the theorem on the completed zeta functional equation by transport.
why it matters
This certificate is required as the analytic substrate field in the Mellin bridge construction for recovered complexes, which equips admissible kernels with Mellin reflection symmetry. It implements the explicit Phase 2 decision to avoid a separate complex analysis stack. The construction supports the foundation for analytic number theory results within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.