HilbertSchmidtNormSq
plain-language theorem explainer
HilbertSchmidtNormSq defines the squared Hilbert-Schmidt norm of the prime operator A(s) as the sum over primes of p to the power -2σ. Researchers instantiating the Recognition Science cost framework via the Euler product would cite this definition when checking convergence of the associated determinant. The definition is a direct encoding of the sum restricted to the set of primes.
Claim. The squared Hilbert-Schmidt norm of the prime operator A(s) is defined by $||A(s)||_2^2 := ∑_p p^{-2σ}$ for real σ.
background
The module instantiates the abstract RS carrier and sensor framework from AnnularCost and CostCoveringBridge by substituting the Euler product of ζ(s). Core objects include PrimeSum σ := ∑_p p^{-σ} and the present quantity, which the module doc identifies as the HS norm squared of A(s). The local setting is the three-layer chain: abstract cost axioms, conditional RH via carrier axioms, and concrete Euler product yielding holomorphic nonvanishing C(s) on Re(s) > 1/2.
proof idea
The definition is a one-line wrapper that applies the infinite sum ∑' directly to the Primes set, raising each prime to the real power -2σ.
why it matters
This supplies the key convergence condition for det₂(I - A(s)) in the module doc. It feeds the downstream results hilbert_schmidt_convergent, carrier_log_convergent, and euler_instantiation, which close the bridge to the cost-covering axiom and conditional RH. In the Recognition Science framework the definition anchors the concrete number-theoretic layer to the abstract carrier/sensor structure, consistent with the phi-ladder and eight-tick octave upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.