LogicComplexAnalyticSubstrateCert
plain-language theorem explainer
LogicComplexAnalyticSubstrateCert records the bijection between LogicComplex and standard ℂ together with the induced transport of the Riemann zeta function, its completed form, the Euler-product limit for Re(s) > 1, and the completed functional equation. Researchers constructing Mellin or theta bridges in the Recognition Science number-theory layer cite this certificate to justify reuse of Mathlib analytic machinery. The structure is populated by a direct definition that assembles the transport maps with existing zeta identities and two named
Claim. Let LogicComplex denote the structure whose real and imaginary parts lie in the recovered reals. A certificate consists of a bijection carrier_equiv : LogicComplex ≃ ℂ such that the recovered Riemann zeta equals the classical zeta after transport to ℂ, the analogous identity holds for the completed zeta, the Euler-product partial sums converge to the zeta value whenever Re(s) > 1, and the completed zeta satisfies the functional equation under the map s ↦ 1 − s.
background
LogicComplex is the structure with fields re and im of type LogicReal. The maps toComplex and fromComplex supply the equivalence to Mathlib ℂ by applying toReal componentwise. The functions logicRiemannZeta and logicCompletedRiemannZeta are obtained by composing the standard riemannZeta and completedRiemannZeta with toComplex, as recorded in the sibling definitions of the same module.
proof idea
The structure is introduced as a plain definition whose five fields are populated by the downstream witness logicComplexAnalyticSubstrateCert. That witness supplies the carrier equivalence directly, uses reflexivity for the two transport identities, invokes logicRiemannZeta_eulerProduct_tendsto for the Euler-product limit, and invokes logicCompletedRiemannZeta_one_sub for the functional equation.
why it matters
The certificate is required by RecoveredComplexMellinBridge and LogicThetaZetaBridge, which embed it as the analytic_substrate field. It implements the explicit Phase 2 decision recorded in the module documentation: retain Mathlib ℂ as the analytic substrate rather than redevelop contour integration on recovered complexes. The construction therefore supplies the complex-analysis layer presupposed by any later appeal to zeta regularization inside the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.