primeHop
plain-language theorem explainer
primeHop defines the off-diagonal hopping operator for each prime p as the sum of the forward shift V_p and its inverse on the free real module over multiplicative indices. Researchers building algebraic skeletons for the Hilbert-Pólya operator in Recognition Science would cite this as the multiplicative-direction term inside the candidate operator. The definition is a direct one-line sum of shiftOp p and shiftInvOp p.
Claim. For a prime $p$, the linear endomorphism $V_p + V_p^{-1}$ of the free real module on the multiplicative index group, where $V_p$ multiplies the index by $p$ and $V_p^{-1}$ divides by $p$.
background
The module builds an algebraic candidate for the Hilbert-Pólya operator on the free real module StateSpace over MultIndex, the free abelian group on primes (isomorphic to the positive rationals under multiplication). StateSpace is the pre-Hilbert space consisting of finitely supported real functions on MultIndex; diagOp applies the J-cost function to each basis vector while shiftOp p and its inverse implement multiplication and division by the prime p. The reciprocal symmetry J(x) = J(1/x) induces an involution operator that maps each shift to its inverse, mirroring the functional equation of the completed zeta function.
proof idea
One-line definition that adds the shift operator shiftOp p to the inverse shift operator shiftInvOp p.
why it matters
primeHop supplies the off-diagonal summands for the candidate operator candidateOp, which is the finite truncation D plus weighted sum of prime hops. It realizes the multiplicative direction in the Recognition Science framework and feeds the involution-commutation theorems involutionOp_primeHop and involutionOp_sum_primeHop. The module leaves open whether the spectrum of the completed operator reproduces the imaginary parts of the non-trivial zeta zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.