EulerInstantiationCert
plain-language theorem explainer
EulerInstantiationCert packages convergence of the summed det2 log factors, non-vanishing of the carrier value, positivity of the derivative bound, and sensor-compatible regular carriers, all restricted to real parts above 1/2. Analytic number theorists linking the zeta Euler product to Recognition Science cost axioms would cite this certificate to activate the covering bridge. The structure is assembled directly from upstream convergence and non-vanishing lemmas with no further reduction steps.
Claim. Let $C(s)$ be the Euler product carrier. For every real part $σ > 1/2$ the series $∑_p det_2 log factor(p, σ)$ converges, $C(σ) ≠ 0$, and the logarithmic derivative satisfies a positive bound. For any defect sensor there exists a regular carrier whose radius equals the sensor real part minus $1/2$.
background
The module instantiates the abstract carrier/sensor framework of AnnularCost and CostCoveringBridge by substituting the concrete Euler product for ζ(s). Core objects are the prime sum $P(σ) = ∑_p p^{-σ}$, the squared Hilbert-Schmidt norm $∑_p p^{-2σ}$, the carrier log series, and the derivative bound $2∑_p (log p) p^{-2σ}/(1-p^{-σ})$. Upstream lemmas establish Hilbert-Schmidt convergence for σ > 1/2 and carrier non-vanishing on the same half-plane.
proof idea
The structure is introduced by its four fields. The verified predicate extracts the conjunction of non-vanishing, positive derivative bound, and sensor compatibility. The downstream constructor mkEulerInstantiationCert populates the fields by direct application of det2_product_convergent, carrier_nonvanishing, carrierDerivBound_pos, and eulerRegularCarrier.
why it matters
The certificate closes the instantiation chain from Euler product to the RegularCarrier interface, allowing the cost-covering axiom to be invoked and yielding a conditional Riemann hypothesis. It is consumed by mkEulerInstantiationCert. Within the Recognition framework it supplies the concrete analytic object that realizes the carrier non-vanishing and bounded derivative steps required for the T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.