RecoveredComplexMellinBridge
plain-language theorem explainer
RecoveredComplexMellinBridge assembles a certificate for recovered-complex zeta operations together with a real kernel and its admissible Mellin package that enforces reflection symmetry. Workers on the RS-native zeta program cite this structure as the Phase 3 transform-level bridge that Phase 4 will fill with an explicit theta kernel. The declaration is a plain four-field record whose fields directly encode the substrate certificate, the kernel, the MellinAdmissibleKernel assumptions, and the equality M(s) = M(1-s).
Claim. A structure that packages a certificate ensuring all analytic zeta operations occur in the complex numbers via the recovered-complex equivalence, a real-valued kernel function, an admissible Mellin package for that kernel (recording the transform values and the validity of the substitution that sends the parameter s to 1-s), and the reflection property that the Mellin transform satisfies M(s) = M(1-s) for every real s.
background
The module implements Phase 3 of the RS-native zeta program. It supplies a formal Mellin-transform interface whose reflection property follows from reciprocal symmetry of the kernel, while deliberately separating the algebraic/RS content (reciprocal symmetry and kernel substitution) from the analytic content (existence of the integral transform and validity of the x to x^{-1} change of variables). The result is not yet the theta/zeta functional equation; it is the transform-level bridge that Phase 4 will instantiate with a theta kernel. MellinAdmissibleKernel records the exact analytic assumptions an integral definition must satisfy: M s is the transform value at s, and the substitution property asserts that the x to x^{-1} change of variables is valid and maps the transform at s to the transform at 1-s. LogicComplexAnalyticSubstrateCert certifies that all analytic zeta operations are performed in Mathlib complex numbers through the recovered-complex equivalence.
proof idea
This is a structure definition with no proof body. It directly assembles the four required components: the LogicComplexAnalyticSubstrateCert from the compatibility module, an arbitrary real kernel, a MellinAdmissibleKernel instance for that kernel, and the reflection equality that is already part of the MellinAdmissibleKernel substitution field.
why it matters
The structure earns its place as the Phase 3 bridge in the RS-native zeta program and is used by the downstream constructor recoveredComplexMellinBridge_of_admissible. Its doc-comment states that it records the bridge Phase 4 must instantiate with an explicit theta kernel. The construction aligns with the Recognition Composition Law through the reciprocal symmetry built into MellinAdmissibleKernel and with the broader forcing chain that derives reflection properties from J-cost symmetry. It leaves open the concrete choice of theta kernel that will close the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.