costAt
plain-language theorem explainer
costAt assigns to each multiplicative index v the Recognition Science cost J evaluated at the positive rational it encodes. Researchers constructing candidate operators for the Hilbert-Pólya conjecture cite it when defining the diagonal cost operator on the free real module over the multiplicative indices. The definition is a direct one-line composition of the toRat embedding with the Jcost function.
Claim. For a finitely supported function $v$ from primes to integers, define $costAt(v) := J(∏_p p^{v(p)})$, where $J$ is the Recognition Science cost function and the product is the positive rational represented by the index $v$.
background
MultIndex is the free abelian group on the primes, written as finitely supported maps from Nat.Primes to ℤ. toRat sends such an index to the real number ∏ p^(v p). Jcost is the cost function imported from the Cost module and applied to positive reals. This definition appears in the module that builds the algebraic skeleton of a candidate Hilbert-Pólya operator on the free ℝ-module over MultIndex. The module imports Cost for Jcost and relies on the local toRat that specializes the recovery map from RationalsFromLogic.
proof idea
one-line wrapper that applies the composition of toRat and Jcost.
why it matters
costAt supplies the values that become the diagonal entries of diagOp and enters the growth statements in CostPotentialBound and CostPotentialLinearGrowth. It realizes the cost function on the index space, which enables the reciprocal symmetry proved in costAt_neg_eq. The definition fills the main definitions section of the Hilbert-Pólya candidate module, which establishes structural symmetries that mirror the zeta functional equation while leaving the spectral identification open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.