WeightDecayPolynomial
WeightDecayPolynomial encodes the polynomial decay requirement on prime-indexed weights λ_p = O(1/p^{1+ε}) for ε > 0. Researchers verifying compact resolvent properties for the cost operator T_J cite this predicate as the weights_decay hypothesis in sub-conjecture C.2. The definition consists of a direct existential statement over a positive bounding constant C.
claimLet λ : ℙ → ℝ assign real weights to primes and let ε ∈ ℝ. The predicate WeightDecayPolynomial(λ, ε) holds if there exists C > 0 such that |λ(p)| ≤ C / p^{1+ε} for every prime p.
background
This module constructs the operator-theoretic setting for the candidate cost operator T_J, introducing the dense domain of finite-support multiplicative states and stating three regularity sub-conjectures as hypothesis structures. The basic weightDecay condition requires square-summability of the prime weights λ_p; WeightDecayPolynomial strengthens it to a uniform polynomial bound with positive exponent. Upstream, Primes is defined as the set {n ∈ ℕ | Nat.Prime n}, supplying the discrete index set for all weight functions.
proof idea
One-line wrapper that directly encodes the predicate as an existential quantifier over C > 0 satisfying the uniform bound |lamP p| ≤ C / (p.val : ℝ)^{1+ε} for all p : Nat.Primes. No lemmas or tactics are invoked; the body is the explicit Prop.
why it matters in Recognition Science
The predicate supplies the weights_decay field inside the CompactResolvent structure (sub-conjecture C.2) and appears in the cost_operator_regularity_certificate that assembles the module's structural facts. It supports the transition from the J-cost functional to a spectral operator with discrete spectrum by guaranteeing the decay needed for compactness of the resolvent. The analytic discharge of the regularity conjectures remains open.
scope and limits
- Does not assert that weights derived from the J-functional satisfy the bound.
- Does not fix any concrete value of ε.
- Does not prove square-summability (handled by the separate weight_polynomial_decay_summable theorem).
- Does not constrain the linear growth of the cost potential.
formal statement (Lean)
98def WeightDecayPolynomial (lamP : Nat.Primes → ℝ) (ε : ℝ) : Prop :=
proof body
Definition body.
99 ∃ C : ℝ, 0 < C ∧ ∀ p : Nat.Primes, |lamP p| ≤ C / (p.val : ℝ) ^ (1 + ε)
100
101/-- Polynomial decay (with exponent at least `1`, i.e., `ε ≥ 0`) implies
102 square-summability. We need `2 * (1 + ε) > 1` which holds for any
103 `ε > -1/2`; in particular for any `ε ≥ 0`. -/