weight_polynomial_decay_summable
plain-language theorem explainer
Polynomial decay of prime weights λ_p at rate p^{-(1+ε)} for ε ≥ 0 implies square-summability of λ_p² over the primes. Spectral analysts working on the cost operator T_J would cite this to close the bandwidth hypothesis for trace-class or compact-resolvent arguments. The proof obtains the decay constant, builds an explicit dominating p-series via the prime-to-nat injection, verifies pointwise domination, and invokes the norm-bounded summability criterion.
Claim. If there exists C > 0 such that |λ_p| ≤ C / p^{1+ε} for every prime p and every ε ≥ 0, then ∑_p λ_p² < ∞.
background
The CostOperatorRegularity module develops the operator theory for the candidate cost operator T_J on the dense domain of finite-support multiplicative states. WeightSquareSummable requires that the sum of squared prime weights is finite; this is the direct operator-level translation of the RS bandwidth constraint. WeightDecayPolynomial is the stronger hypothesis that |λ_p| ≤ C p^{-(1+ε)} for some C > 0 and ε ≥ 0, needed for compact resolvent.
proof idea
Obtain C and the pointwise bound from the decay hypothesis. Define the comparison series g(p) = (C / p^{1+ε})². Prove g summable by reducing the p-series ∑ 1/n^{2(1+ε)} (which converges for ε ≥ 0) through the injective map from primes to naturals, then scaling by C². Establish |λ_p|² ≤ g(p) by algebraic manipulation of squares and absolutes. Conclude with the norm-bounded summability lemma.
why it matters
The theorem supplies the second conjunct of cost_operator_regularity_certificate, which packages the structural facts needed for the three regularity sub-conjectures. It directly converts the polynomial-decay hypothesis into the square-summability condition required for the trace-class heat-kernel sub-conjecture. Within Recognition Science this step legitimizes T_J as a spectral object once the J-derived bandwidth constraint is assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.