toRat_add
plain-language theorem explainer
The map from multiplicative indices to positive reals converts index addition into ordinary multiplication. Researchers constructing the Hilbert-Pólya candidate operator cite it to confirm that the underlying state space respects the multiplicative group law on positive rationals before the diagonal cost and shift operators are defined. The proof unfolds the product definition of toRat, applies the Finsupp additivity lemma for products, and reduces the exponent case via zpow_add₀ after a prime-nonzero check.
Claim. Let $v, w$ be finitely supported maps from the set of primes to the integers. Then the real number recovered from their sum equals the product of the two recovered numbers: $∏_p p^{v(p)+w(p)} = (∏_p p^{v(p)}) ⋅ (∏_p p^{w(p)})$.
background
In this module MultIndex is the free abelian group on the primes, written as finitely supported functions Nat.Primes →₀ ℤ. The function toRat sends such an index v to the positive real ∏p p^{v(p)}, recovering the element of ℚ{>0}^× that the index represents. This supplies the coordinate space on which the candidate Hilbert-Pólya operator is built, with its diagonal part later encoding the Recognition cost J and its involution implementing the functional-equation symmetry J(x) = J(1/x). The present theorem is the direct multiplicative counterpart of the additive transfer map toRat_add imported from RationalsFromLogic.
proof idea
Unfold toRat to expose the Finsupp product. Rewrite with Finsupp.prod_add_index, which decomposes the product over the summed supports. The first subgoal simplifies by definition; the second applies zpow_add₀ after extracting Nat.Prime.ne_zero to guarantee the base is nonzero.
why it matters
This compatibility is invoked by the transfer theorems add_assoc', add_comm', add_mul' and their siblings in RationalsFromLogic, which establish the ring axioms on LogicRat via the eq_iff_toRat_eq principle. Inside the Recognition framework it guarantees that the multiplicative index space behaves exactly as the positive rationals before the J-cost operator and the reciprocal involution are imposed, thereby closing one algebraic prerequisite for the candidate operator described in the module documentation. The spectral identification with zeta zeros remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.