WeightSquareSummable
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.
claimLet $λ : ℙ → ℝ$ 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 in Recognition Science
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.
scope and limits
- Does not prescribe any concrete decay rate such as polynomial or exponential for λ_p.
- Does not establish convergence for any specific choice of weights.
- Does not relate the weights to the J-function or the phi-ladder.
- Does not address essential self-adjointness or compactness of the resolvent.
formal statement (Lean)
93def WeightSquareSummable (lamP : Nat.Primes → ℝ) : Prop :=
proof body
Definition body.
94 Summable (fun p : Nat.Primes => (lamP p) ^ 2)
95
96/-- The stronger decay condition needed for compact resolvent:
97 `λ_p = O(1/p^{1+ε})` for some `ε > 0`. -/