WeightDecayPolynomial
plain-language theorem explainer
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.
Claim. Let λ : ℙ → ℝ 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.