toRat_zero
The map from multiplicative indices to positive reals sends the zero index to 1. Researchers building the Recognition Science candidate for the Hilbert-Pólya operator cite this when normalizing the free module or verifying additive identities. The proof is a one-line simp that unfolds the finite-support product definition.
claimLet $v_0$ be the zero element of the free abelian group on the primes. The map sending an exponent vector to the corresponding positive real satisfies $v_0.map = 1$.
background
The module builds an algebraic skeleton for a candidate Hilbert-Pólya operator on the free real module over positive rationals, using the Recognition cost J. MultIndex is the free abelian group on primes, isomorphic to ℚ_{>0}^×. The map toRat recovers the real number ∏ p^k from an exponent vector v via finite product. This theorem is the normalization at the identity element and parallels the toRat_zero result from RationalsFromLogic that recovers rationals from the logic representation.
proof idea
One-line simp wrapper that unfolds the definition of toRat, reducing the empty product over zero support to 1.
why it matters in Recognition Science
This supplies the base case for additive identities, feeding into add_zero', zero_add', and toRat_neg in RationalsFromLogic and the local module. It anchors the structure before the involution and shift operators that mirror the zeta functional equation. The open spectral question is whether the resulting operator has eigenvalues matching the imaginary parts of the zeta zeros.
scope and limits
- Does not establish self-adjointness on a completed Hilbert space.
- Does not compute eigenvalues or address the Riemann hypothesis.
- Does not incorporate the J-cost function or the full operator spectrum.
Lean usage
rw [toRat_zero]formal statement (Lean)
70@[simp] theorem toRat_zero : toRat (0 : MultIndex) = 1 := by
proof body
One-line wrapper that applies simp.
71 simp [toRat]
72