IndisputableMonolith.Foundation.LogicComplexCompat
This module defines the Riemann zeta function and its completed version on complex numbers recovered from the logic substrate. Researchers tracing the RS-native zeta program cite it to bridge the arithmetic ledger to analytic continuation steps. It assembles imported results from ComplexFromLogic, EulerProductEqualsZeta, and CompletedZetaLedger with no internal proofs.
claimThe module exports $\zeta_{\text{logic}}(s)$ and the completed $\xi_{\text{logic}}(s)$ for $s$ in the recovered complex carrier $\text{LogicComplex}$, satisfying the Euler product on $\operatorname{Re}(s)>1$ and the reciprocal functional equation.
background
The module occupies the Foundation layer and imports three upstream modules. ComplexFromLogic constructs the carrier LogicComplex as pairs of recovered reals and proves carrier-level equivalence with Mathlib's $\mathbb{C}$, without redeveloping complex analysis. EulerProductEqualsZeta wires the RS prime-ledger partition to the theorem that the Euler product equals the Riemann zeta function on $\operatorname{Re}(s)>1$. CompletedZetaLedger packages Mathlib's completed-zeta functional equation as the reciprocal balance law for the arithmetic ledger.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the zeta definitions that feed MellinTransform (Phase 3 of the RS-native zeta program, separating algebraic reciprocal symmetry from kernel substitution) and ZetaFromTheta (Phase 4, isolating the theta-style Mellin bridge to the completed functional equation). It enables the zeta function to be read directly on recovered complexes while preserving the Euler-product and balance-law properties.
scope and limits
- Does not develop complex analysis or prove holomorphy.
- Does not contain the full theta/Mellin analytic proof.
- Does not rederive the Euler product or functional equation.
- Limits to compatibility between recovered complexes and standard zeta.
used by (2)
depends on (3)
declarations in this module (9)
-
def
logicRiemannZeta -
def
logicCompletedRiemannZeta -
theorem
logicRiemannZeta_fromComplex -
theorem
logicCompletedRiemannZeta_fromComplex -
theorem
toComplex_re_eq -
theorem
logicRiemannZeta_eulerProduct_tendsto -
theorem
logicCompletedRiemannZeta_one_sub -
structure
LogicComplexAnalyticSubstrateCert -
def
logicComplexAnalyticSubstrateCert