det2Factor
plain-language theorem explainer
The definition supplies the per-prime multiplicative factor (1 - p^{-σ}) exp(p^{-σ}) used to build det₂ in the Euler product for the Recognition Science cost carrier. Researchers instantiating the abstract annular cost framework via zeta-function products cite it when constructing holomorphic nonvanishing functions on Re(s) > 1/2. The definition is a direct algebraic expression with no auxiliary lemmas or reductions.
Claim. For each prime $p$ and real number $σ$, the per-prime factor is defined by $(1 - p^{-σ}) · exp(p^{-σ})$.
background
The EulerInstantiation module shows that the Euler product of ζ(s) instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge. Core objects include PrimeSum σ := ∑_p p^{-σ} (prime zeta), HilbertSchmidtNorm σ := ∑_p p^{-2σ} (HS norm squared of A(s)), carrierLogSeries σ := ∑_p [2 log(1-p^{-σ}) + 2p^{-σ}], and carrierDerivBound σ. The local setting is the three-layer chain: abstract cost framework, abstract carrier plus axiom implying conditional RH, and concrete Euler product yielding the carrier. Upstream structures supply J-cost minimization (strictly convex with minimum at x=1), ledger factorization of (ℝ₊, ×), spectral emergence of SU(3)×SU(2)×U(1) and three generations, and nuclear density tiers on the φ-ladder.
proof idea
This is a direct definition that implements the per-prime factor exactly as (1 - (p : ℝ)^(-σ)) * Real.exp((p : ℝ)^(-σ)). No tactics or lemmas are applied; the expression is written out in one line to match the required entire-function property in s.
why it matters
The definition supplies the building block for det₂(I-A(s)) convergence and the subsequent holomorphic nonvanishing of C(s) on Re(s) > 1/2, which satisfies the EulerCarrier and RegularCarrier interfaces and activates the cost-covering axiom. It fills the primes → A(s) Hilbert-Schmidt → det₂ convergent step in the module architecture, supporting the conditional RH route. It touches the broader Recognition Science landmarks of J-cost convexity and the eight-tick octave through the carrier construction, though no open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.