CostPotentialBound
plain-language theorem explainer
CostPotentialBound encodes an abstract lower bound on the cost function costAt at multiplicative indices, requiring costAt(v) to grow at least as fast as R times a chosen norm to the power α. Spectral theorists working on the J-cost operator cite it as the linear-growth precondition for sub-conjecture C.2. The declaration is a bare structure definition that packages the inequality without invoking lemmas or reductions.
Claim. Let MultIndex be the set of multiplicative indices and let costAt map each index to its J-cost. For any norm function norm : MultIndex → ℝ and constants R > 0, α ∈ ℝ, the bound asserts that R ⋅ norm(v)^α ≤ costAt(v) holds for every v ∈ MultIndex.
background
The module CostOperatorRegularity builds the operator-theoretic setting for the cost operator T_J on the dense domain of finite-support multiplicative states. It proves structural facts such as density and symmetry to zero sorry, then encodes the three analytic sub-conjectures (essential self-adjointness, compact resolvent, trace-class heat kernel) as hypothesis structures that depend on prime-weight assumptions.
proof idea
The declaration is a structure definition whose single field directly records the growth inequality. No upstream lemmas are applied; the structure simply packages the abstract precondition stated in the module documentation.
why it matters
CostPotentialBound supplies the growth precondition for sub-conjecture C.2 inside the regularity analysis of T_J. It is referenced by the hypothesis structures EssentialSelfAdjointness and CompactResolvent and by the regularity_chain in the same module. In the Recognition framework it bridges the multiplicative cost algebra to the spectral properties required for the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.