det2_product_convergent
plain-language theorem explainer
The theorem establishes summability of det2LogFactor p σ over primes for real σ > 1/2. Researchers instantiating the Recognition Science carrier via the Euler product of zeta would cite it to justify holomorphy and nonvanishing of C(s) on Re(s) > 1/2. The proof is a one-line wrapper that reduces the claim to absolute summability via Summable.of_norm and det2_log_summable.
Claim. For real σ > 1/2 the series ∑_{p prime} det₂LogFactor(p, σ) converges, where det₂LogFactor(p, σ) is the logarithmic contribution of each prime factor to det₂(I − A(σ)) with A(σ) the Hilbert–Schmidt operator whose squared norm is ∑_p p^{-2σ}.
background
This declaration belongs to the EulerInstantiation module, which supplies the concrete Euler-product layer on top of the abstract annular-cost and cost-covering-bridge framework. Core objects defined in the module are PrimeSum σ := ∑_p p^{-σ}, HilbertSchmidtNorm σ := ∑_p p^{-2σ}, carrierLogSeries σ := ∑_p [2 log(1 − p^{-σ}) + 2 p^{-σ}], and carrierDerivBound σ. The local setting is the three-layer instantiation chain: abstract cost axioms → conditional RH → concrete Euler carrier C(s) = det₂(I − A(s))² that is holomorphic and nonvanishing for Re(s) > 1/2.
proof idea
The proof is a one-line wrapper. It applies Summable.of_norm to pass to the normed series, then uses simpa with Real.norm_eq_abs to invoke the already-proved summability statement det2_log_summable hσ.
why it matters
The result is invoked directly by carrier_log_convergent (which states that log C(σ) converges on Re(s) > 1/2) and by mkEulerInstantiationCert (which assembles the verified EulerInstantiationCert record). It completes the step 'primes → A(s) Hilbert–Schmidt → det₂ convergent' in the module’s architecture, thereby enabling the EulerCarrier and RegularCarrier interfaces and the subsequent application of the cost-covering axiom. The argument sits inside the Recognition Science forcing chain after T5–T8 and the Recognition Composition Law, supplying the number-theoretic bridge to conditional RH.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.