carrier_pos
plain-language theorem explainer
The theorem establishes that the carrier function C(σ) obtained from the squared determinant of the Euler product operator is strictly positive for every real σ exceeding 1/2. Researchers deriving conditional Riemann hypothesis statements from cost-covering axioms would cite this positivity to guarantee a nonvanishing holomorphic carrier. The argument is a one-line term that unfolds the carrier definition to an exponential and invokes the positivity of the real exponential function.
Claim. For every real number $σ > 1/2$, the carrier function $C(σ)$ obtained from the squared determinant of the Euler product operator satisfies $0 < C(σ)$.
background
The module instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge by means of the Euler product for ζ(s). Core objects include PrimeSum σ = ∑_p p^{-σ}, HilbertSchmidtNorm σ = ∑_p p^{-2σ}, carrierLogSeries σ = ∑_p [2 log(1 - p^{-σ}) + 2 p^{-σ}], and the resulting carrier C(s) = det₂²(I - A(s)) which is holomorphic and nonvanishing on Re(s) > 1/2 once the log series converges. The local setting is the three-layer instantiation chain: abstract cost axioms, conditional RH via cost-covering, and concrete Euler product supplying the carrier.
proof idea
The proof is a one-line term that unfolds the definition of carrierValue to expose an exponential expression and then applies the lemma Real.exp_pos.
why it matters
This result feeds directly into carrier_nonvanishing and zeros_in_continuation in the same module, and supplies the positivity step used by sensitivity_pos, sensitivity_strict_anti and pulseSpacing_pos in the engineering modules. It completes the concrete Euler instantiation step in the module architecture, moving from convergent Hilbert-Schmidt norm and log series to a nonvanishing carrier that satisfies the EulerCarrier interface and thereby makes the cost-covering axiom applicable toward conditional RH.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.