WeightSquareSummable
plain-language theorem explainer
WeightSquareSummable encodes the requirement that a map from primes to reals has square-summable values. Researchers formalizing the spectral theory of the cost operator T_J cite it to enforce the bandwidth constraint that keeps the operator inside the Hilbert space. The definition is introduced as a direct abbreviation of the standard summability predicate applied to the squared sequence.
Claim. Let $λ : ℙ → ℝ$ be any function from the set of primes to the reals. Then $∑_{p ∈ ℙ} λ(p)^2 < ∞$.
background
The CostOperatorRegularity module constructs the dense domain of finite-support multiplicative states for the candidate cost operator T_J and isolates three regularity sub-conjectures under explicit assumptions on prime weights. The definition weightDecay is precisely the condition that the sum of squared weights is finite; it is the operator-theoretic counterpart of the Recognition Science bandwidth constraint. Upstream, the Primes definition supplies the set {n | Nat.Prime n} and the meta-realization structure records the structural axioms needed for the forcing chain.
proof idea
The declaration is a one-line definition that directly applies the Mathlib summability predicate to the sequence of squared weights indexed by Nat.Primes. No lemmas or tactics are invoked; the body is the literal transcription of the required convergence statement.
why it matters
WeightSquareSummable supplies the weights_summable field inside the EssentialSelfAdjointness structure (sub-conjecture C.1) and is invoked by the cost_operator_regularity_certificate theorem that assembles the module's structural facts. It implements the bandwidth-derived decay needed for the cost operator to be densely defined and symmetric, thereby supporting the passage from the T0-T8 forcing chain to the spectral analysis of T_J. The definition closes one piece of the scaffolding that converts the J-cost functional into a legitimate unbounded operator on the Hilbert space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.