toRat
plain-language theorem explainer
The definition maps each multiplicative index, a finitely supported function from primes to integers, to the positive real obtained by raising each prime to its exponent and multiplying. Researchers building the algebraic skeleton for a Hilbert-Pólya candidate operator cite this embedding when populating the state space or applying the diagonal cost operator. It is realized by a direct product over the support of the index.
Claim. Let $v$ be a finitely supported map from the set of primes to the integers. Then $toRat(v) := ∏_p p^{v(p)} ∈ ℝ$, with the product taken over primes having nonzero exponent under $v$.
background
The module builds an algebraic skeleton for a candidate Hilbert-Pólya operator on the free ℝ-module over the multiplicative group ℚ_{>0}^×, using the Recognition Science cost J to enforce reciprocal symmetry that mirrors the zeta functional equation. MultIndex is the type of finitely supported functions from primes to integers, serving as the free abelian group on the primes. toRat recovers the positive rational represented by such an index and casts it into ℝ.
proof idea
One-line wrapper that applies the product operation on the finitely supported function, raising each prime value to the corresponding integer exponent and casting the result into ℝ.
why it matters
This embedding of the index space into the reals is required to define the state space and the diagonal operator D in the candidate construction. It is used by downstream transport theorems such as toComplex_ofLogicRat and the round-trip results in RationalsFromLogic. Within the Recognition Science framework it supplies the concrete map needed for the involution and shift operators whose commutation relations are proved without sorry, while the spectral identification with zeta zeros remains the open Hilbert-Pólya question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.