CompactResolvent
plain-language theorem explainer
CompactResolvent packages the hypothesis that the resolvent of the cost operator T_J is compact on H_-, assuming polynomial decay of prime weights λ_p and linear growth of the cost potential. Spectral theorists working on the J-cost operator cite this sub-conjecture when establishing discrete spectrum. The declaration is a structure definition that directly assembles the decay and growth conditions with a placeholder True for the analytic compactness statement.
Claim. Given λ_p : primes → ℝ, CompactResolvent(λ_p) asserts that there exists ε > 0 such that |λ_p| ≤ C / p^{1+ε} for some C > 0, that cost(v) ≥ R ∑_p |v_p| for all multiplicative indices v and some R > 0, and that the resolvent (T_J - z)^{-1} is compact on H_- (stated as a placeholder).
background
The CostOperatorRegularity module constructs the dense domain of finite-support multiplicative states for the cost operator T_J and states three regularity sub-conjectures as hypothesis structures. WeightDecayPolynomial requires λ_p = O(1/p^{1+ε}) for ε > 0, which implies square-summability of the weights. CostPotentialLinearGrowth requires costAt(v) ≥ R ⋅ ∑_p |v_p| for every multiplicative index v, which follows because J(p) ≥ J(2) = 1/4 for all primes p ≥ 2.
proof idea
This is a structure definition that directly packages the three fields: the polynomial weight decay condition, the linear cost growth condition, and a placeholder True for compactness. No lemmas or tactics are applied; the declaration serves as a hypothesis interface awaiting analytic discharge.
why it matters
CompactResolvent is sub-conjecture C.2 and feeds the regularity_chain theorem, which couples it with EssentialSelfAdjointness to obtain TraceClassHeatKernel. In the Recognition framework it supports discrete spectrum for T_J, consistent with J-uniqueness and the phi-ladder from the forcing chain. It touches the open analytic question of discharging the compactness placeholder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.