CostPotentialLinearGrowth
The definition encodes the linear lower bound on the cost potential in terms of the L1 norm of a multiplicative index. Spectral theorists studying the cost operator T_J cite it as the growth hypothesis needed for resolvent compactness. The statement follows from the uniform lower bound J(p) >= J(2) together with the symmetry J(1/p) = J(p).
claimThere exists a positive real number $R$ such that for every multiplicative index $v$, $R$ times the sum of the absolute values of the components of $v$ is at most the cost evaluated at $v$.
background
The module formalizes operator-theoretic foundations for the cost operator $T_J$ on the dense domain of finite-support multiplicative-index states. It introduces three regularity sub-conjectures as hypothesis structures, with this definition supplying the cost-growth precondition paired with polynomial weight decay. The J-cost structure originates in the phi-forcing derivation, where the recognition cost satisfies the composition law and yields the lower bound J(p) >= 1/4 for primes.
proof idea
The definition is stated directly as the existence of R > 0 satisfying the linear inequality for all v. It rests on the prime lower bound for J together with sign symmetry, without further lemmas or tactics.
why it matters in Recognition Science
It supplies the cost-growth hypothesis required by the CompactResolvent structure (sub-conjecture C.2), which asserts compactness of the resolvent of T_J once weights decay polynomially. The definition therefore closes one precondition in the chain from the J-cost construction to discrete spectrum and trace-class heat kernel. It touches the open analytic discharge of the three regularity conjectures.
scope and limits
- Does not prove existence of R from first principles.
- Does not specify the numerical value of R or its relation to phi.
- Does not address essential self-adjointness or trace-class properties.
- Does not incorporate the full Hilbert-space inner product or domain details.
formal statement (Lean)
84def CostPotentialLinearGrowth : Prop :=
proof body
Definition body.
85 ∃ R : ℝ, 0 < R ∧ ∀ v : MultIndex,
86 R * (v.support.sum (fun p => |(v p : ℝ)|)) ≤ costAt v
87
88/-! ## Weight decay condition -/
89
90/-- The bandwidth-derived decay condition on prime weights: the sum
91 of squared weights is finite. This is the operator-level analog
92 of the RS bandwidth constraint. -/