shiftInvOp_single
plain-language theorem explainer
The inverse prime-shift operator V_p^{-1} acts on a basis vector c · e_v by subtracting the unit vector for prime p, yielding c · e_{v - e_p}. Researchers constructing algebraic models of the zeta functional equation inside Recognition Science would cite this when verifying formal unitarity of the shift operators. The proof is a one-line simplification that unfolds shiftInvOp and applies Finsupp's mapDomain rule on singletons.
Claim. Let p be a prime and v a multiplicative index. For any real scalar c, the inverse shift operator satisfies shiftInvOp_p (c · e_v) = c · e_{v - e_p}, where e_p is the standard basis vector for p.
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 maps from primes to integers that label positive rationals via the product map toRat. The shift operator V_p adds one to the p-exponent while its inverse subtracts one; these are defined via Finsupp lmapDomain so that they act as linear maps on the module. The construction uses the reciprocal symmetry of the Recognition cost J, which induces the involution operator U that intertwines V_p with V_p^{-1}.
proof idea
The proof is a one-line wrapper. It applies simp with the definition of shiftInvOp together with the lemmas Finsupp.lmapDomain_apply and Finsupp.mapDomain_single, which reduce the action on a singleton directly to the shifted index.
why it matters
This supplies the explicit action required by the downstream theorems involutionOp_shiftInvOp, shiftInvOp_shiftOp and shiftOp_shiftInvOp that establish U V_p = V_p^{-1} U and the formal unitarity V_p V_p^{-1} = id. Those relations realize the operator-level analog of the zeta functional equation inside the Recognition framework. The open spectral question, whether the full diagonal-plus-shift operator reproduces the imaginary parts of the zeta zeros, remains untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.