pith. sign in
def

shiftInvOp

definition
show as:
module
IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
domain
NumberTheory
line
145 · github
papers citing
none yet

plain-language theorem explainer

The inverse prime-shift operator maps each basis vector indexed by a multiplicative index to the vector shifted by subtracting one at the given prime. Researchers constructing algebraic models for the Hilbert-Pólya conjecture cite it to establish the required intertwining with the reciprocal involution. The definition is a direct application of the domain-mapping linear map on finitely supported functions.

Claim. Let $V_p^{-1}$ denote the linear endomorphism of the free real module over the multiplicative index space satisfying $V_p^{-1}(e_v) = e_{v - δ_p}$, where $δ_p$ is the standard basis element at the prime $p$.

background

This module builds an algebraic skeleton for a Hilbert-Pólya operator candidate on the free real module over the multiplicative group of positive rationals, realized via finite-support integer vectors on the primes. The pre-Hilbert space is the free real module on these indices. The prime set is taken from the Euler instantiation. The overall construction uses the recognition cost function J whose reciprocal symmetry J(x) = J(1/x) induces operator-level symmetries mirroring the zeta functional equation.

proof idea

One-line wrapper that applies the linear map induced by domain remapping on the Finsupp structure, subtracting the indicator vector for the prime.

why it matters

The definition is required for the master certificate establishing structural properties of the candidate operator and for the theorems showing that the reciprocal involution intertwines the shift with its inverse. It enables the prime-hop term as the sum of shift and inverse shift. This fills the algebraic part of the Recognition Science approach to the Hilbert-Pólya conjecture, leaving the spectral identification with zeta zeros as an open question.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.