completedZetaFunctionalEquationCert_of_thetaBridge
plain-language theorem explainer
This definition constructs the completed zeta functional equation certificate by projecting fields from a supplied theta-zeta Mellin bridge. Researchers tracing the Recognition Science zeta program from theta data to the functional equation would cite it as the explicit packaging step. The construction is a direct field copy that transfers the Mellin function, its agreement with completedRiemannZeta, and the reflection symmetry.
Claim. Given a bridge structure $B$ containing an admissible theta Mellin transform, a function $m : ℂ → ℂ$, a proof that $m(s) = $ completedRiemannZeta$(s)$ for all $s$, and a proof that $m(s) = m(1-s)$ for all $s$, define the certificate $C$ by setting $C$.completedMellin $:= m$, $C$.completed_matches_zeta $:=$ the matching proof of $B$, and $C$.completed_reflection $:=$ the reflection proof of $B$.
background
The ZetaFromTheta module isolates Phase 4 of the RS-native zeta program: it records the exact bridge from a theta-style Mellin transform to the completed zeta function without claiming a full analytic formalization. ThetaCompletedZetaBridge is the structure that supplies an admissible theta, the completedMellin continuation, the pointwise agreement with completedRiemannZeta, and the transport of Mellin reflection to the map $s ↦ 1-s$. CompletedZetaFunctionalEquationCert is the weaker record that keeps only the Mellin function together with its zeta agreement and reflection property. The module imports MellinTransform and RecognitionTheta for the underlying transforms and uses LogicComplexCompat to stay inside the recovered-complex substrate; the unconditional functional equation remains Mathlib's completedRiemannZeta_one_sub.
proof idea
This is a one-line wrapper that constructs CompletedZetaFunctionalEquationCert by copying the completedMellin field directly from the input bridge and assigning the two proof fields from the corresponding properties of the bridge.
why it matters
The definition supplies the explicit map from the strong ThetaCompletedZetaBridge to the certificate consumed by logic_completed_zeta_functional_equation_from_theta. It therefore advances the Phase 4 goal of recovering the completed zeta functional equation under the theta/Mellin bridge inside the Recognition Science substrate. The construction keeps the RS-native path separate from the Mathlib theorem while preserving the reflection symmetry that ultimately traces to the J-cost convexity and eight-tick structure upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.