remembers
plain-language theorem explainer
The structure remembers bundles a defect sensor's full center ρ with the explicit analytic witness that its charge is realized by the reciprocal of the Riemann zeta function. Researchers building sampled trace families from the Euler product instantiation of the RS cost framework cite this when lifting abstract carriers to concrete zeta data. It is realized as a direct structure definition with no proof obligations or computational content.
Claim. A structure that stores the center ρ ∈ ℂ together with the property that the charge of the associated defect sensor is witnessed by ζ(s)⁻¹.
background
The EulerInstantiation module realizes the abstract RS carrier and sensor framework (from AnnularCost and CostCoveringBridge) via the Euler product of ζ(s). Core objects include PrimeSum σ := ∑_p p^{-σ}, HilbertSchmidtNorm σ := ∑_p p^{-2σ}, carrierLogSeries σ := ∑_p [2 log(1 - p^{-σ}) + 2 p^{-σ}], and carrierDerivBound σ := 2 ∑_p (log p) p^{-2σ} / (1 - p^{-σ}). The module proves convergence of these series for Re(s) > 1/2, yielding a holomorphic nonvanishing C(s) = det₂²(I - A(s)) whose logarithmic derivative is bounded, thereby satisfying the EulerCarrier and RegularCarrier interfaces.
proof idea
Structure definition that directly packages the center ρ and the zetaReciprocal witness; no lemmas or tactics are applied.
why it matters
It supplies the concrete data needed by canonicalDefectSampledFamily to construct the sampled family attached to a hypothetical defect. This step closes the instantiation chain (primes → Hilbert-Schmidt operator → convergent det₂ → EulerCarrier) that makes the cost-covering axiom applicable and yields conditional RH. It directly supports the analytic witness for defect charge in the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.