shiftOp_single
plain-language theorem explainer
The prime-shift operator V_p maps the scaled basis vector c e_v to c e_{v + δ_p} where δ_p increments the exponent of prime p. Researchers constructing algebraic models for the Hilbert-Pólya operator on the free module over positive rationals cite this for verifying basis actions. The proof proceeds by direct simplification invoking the definition of shiftOp together with the mapDomain property on Finsupp singletons.
Claim. Let $p$ be a prime, $v$ a multiplicative index, and $c$ a real scalar. Then the prime-shift operator $V_p$ satisfies $V_p(c e_v) = c e_{v + δ_p}$, where $δ_p$ is the index with value 1 at $p$ and 0 elsewhere.
background
The module builds a candidate Hilbert-Pólya operator on the free real module StateSpace whose basis is indexed by MultIndex, the finitely supported functions from primes to integers that label positive rationals via toRat. The prime-shift operator shiftOp p, denoted V_p, multiplies the underlying rational by p by incrementing the p-exponent in the index. Upstream results supply the J-cost function from PhiForcingDerived.of and the ledger factorization from DAlembert.LedgerFactorization.of, which calibrate the diagonal operator diagOp that commutes with these shifts in later theorems.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definitions shiftOp, Finsupp.lmapDomain_apply and Finsupp.mapDomain_single.
why it matters
This lemma supplies the concrete action needed to verify the intertwining relations such as involutionOp_shiftOp, which states that the reciprocal involution U satisfies U V_p = V_p^{-1} U and thereby mirrors the functional equation of the zeta function at the operator level. It advances the Recognition Science program of realizing the Hilbert-Pólya conjecture via the J-cost symmetry on the multiplicative group, without yet addressing the spectral identification with zeta zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.