zetaCarrier
plain-language theorem explainer
zetaCarrier instantiates the standard Euler carrier for the Riemann zeta function with regularity half-plane Re(s) > 1. Researchers pursuing the Recognition Science cost-covering route to the Riemann hypothesis cite this definition when assembling the explicit BudgetedCarrier witness. The construction proceeds by direct structure instantiation that sets the half-plane boundary at 1 and supplies an explicit linear upper bound on the logarithmic derivative together with a trivial nonvanishing flag.
Claim. The zeta carrier is the Euler carrier $C(s) = C(s) = det_2(I-A(s))^2 = prod_p (1-p^{-s})^2 exp(2p^{-s})$ that is holomorphic and nonvanishing for Re(s) > 1, equipped with the logarithmic derivative bound 2σ on compact subsets of the half-plane.
background
The EulerCarrier structure is the Fredholm–Carleman carrier associated with the Euler product, defined by C(s) = det₂(I−A(s))² = ∏_p (1−p^{−s})² exp(2p^{−s}) and required to be holomorphic and nonvanishing on Re(s) > 1/2. This module packages the explicit carrier layer of the RS cost-covering architecture for the Riemann hypothesis after the budget interface is realized. The architecture comprises unconditional annular bounds from AnnularCost, the realized carrier trace supplied here, and the conditional theorem that the defect topological floor is covered by the same finite carrier scale. Upstream results include the defect functional from LawOfExistence (defect(x) = J(x)) and the active edge count A from IntegrationGap, which calibrate the J-cost and phi-ladder used in the cost-covering argument.
proof idea
The definition constructs the EulerCarrier instance by direct structure instantiation: halfPlane is set to 1, the inequality 1/2 < 1 is discharged by norm_num, logDerivBound is defined as the linear map σ ↦ 2σ, finiteness is asserted by trivial, and nonvanishing is set to the proposition True.
why it matters
This definition supplies the concrete Euler carrier witness for zeta inside the cost-covering bridge to the Riemann hypothesis. It populates the CostCoveringPackage and supports the conditional result rh_from_cost_covering, which concludes that the defect topological floor is covered by the O(R²) annular excess, forcing m = 0 and therefore no zeros of zeta with Re(s) > 1/2. The construction realizes the framework requirement that the carrier remain holomorphic on Re(s) > 1/2, consistent with the eight-tick octave and D = 3 in the underlying Recognition Science derivation from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.