IndisputableMonolith.Foundation.LogicComplexCompat
The module supplies the Riemann zeta function and its completed version defined on the logic-recovered complex carrier. It acts as the compatibility layer that lets the RS zeta program operate on LogicComplex inputs. Number theorists following the Recognition Science zeta phases cite it when bridging Euler-product definitions to Mellin and theta stages. The module assembles these objects by direct import of the complex carrier and the two zeta ledger modules.
claimThe Riemann zeta function $ζ(s)$ for $s$ in the recovered complex plane is given by the Euler product on the half-plane Re$(s)>1$, together with the completed form $ξ(s)$ obeying the functional equation $ξ(s)=ξ(1-s)$.
background
Recognition Science recovers complex numbers as ordered pairs of reals via the ComplexFromLogic carrier, which proves equivalence to the standard ℂ without redeveloping analytic machinery. The module imports this carrier to host zeta objects. Upstream, EulerProductEqualsZeta wires the RS prime-ledger partition to the classical Euler product equality on Re$(s)>1$. CompletedZetaLedger packages the reciprocal balance law that encodes the completed-zeta functional equation.
proof idea
This is a definition module with no proofs. It declares logicRiemannZeta, logicCompletedRiemannZeta and the auxiliary maps by composing the imported LogicComplex carrier with the zeta ledger constructions.
why it matters in Recognition Science
The module supplies the zeta objects required by MellinTransform for its reflection theorem and by ZetaFromTheta for the theta-to-completed-zeta bridge. It occupies the interface step in the RS-native zeta program between the Euler-product phase and the analytic-continuation phases.
scope and limits
- Does not redevelop complex analysis inside the logic carrier.
- Does not prove analytic continuation or holomorphy statements.
- Does not address convergence questions beyond those inherited from the imported zeta modules.
- Limits its scope to compatibility definitions for downstream Mellin and theta modules.
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