CostPotentialLinearGrowth
plain-language theorem explainer
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).
Claim. There 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.