pith. machine review for the scientific record. sign in
def definition def or abbrev high

toRat

show as:
view Lean formalization →

toRat maps each multiplicative index, a finitely supported function from primes to integers, to the corresponding positive real via the product of each prime raised to its exponent. Researchers building the Recognition Science candidate for the Hilbert-Pólya operator cite this embedding when transporting between the index space and reals for operator constructions. The definition is a direct one-line product over the support of the index.

claimFor a finitely supported function $v$ from the set of primes to the integers, define $toRat(v) := ∏_p p^{v(p)}$, where the product runs over primes in the support of $v$.

background

The module constructs the algebraic skeleton of a candidate Hilbert-Pólya operator on the free real module over the multiplicative group of positive rationals, using the Recognition Science cost function J. MultIndex is defined as the free abelian group on the primes, represented as finitely supported functions from primes to integers. toRat recovers the corresponding positive rational as a real number via the product formula. The module documentation states that the reciprocal symmetry J(x) = J(1/x) translates into operator-level intertwining with the multiplicative involution, mirroring the zeta functional equation, but does not claim to prove the Riemann hypothesis.

proof idea

This is a one-line definition that applies the product operation over the support of the multiplicative index, raising each prime to the corresponding integer exponent and interpreting the result in the reals.

why it matters in Recognition Science

This map embeds the multiplicative index space into the reals and feeds directly into downstream results such as toComplex_ofLogicRat, which recovers complex numbers from logic rationals, and theorems in RationalsFromLogic including add_mul', eq_iff_toRat_eq, and equivRat that rely on transport to Mathlib rationals. It supports the main theorems on involution and shift operators that mirror the zeta functional equation. The construction leaves open the spectral question of whether the eigenvalues match the imaginary parts of the zeta zeros.

scope and limits

formal statement (Lean)

  64def toRat (v : MultIndex) : ℝ :=

proof body

Definition body.

  65  v.prod (fun p k => (p.val : ℝ) ^ (k : ℤ))
  66
  67/-- The cost evaluated at the rational represented by `v`. -/

used by (29)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.