shiftOp_shiftInvOp
plain-language theorem explainer
For each prime p the operators V_p and V_p^{-1} on the free real module over multiplicative indices satisfy V_p composed with V_p^{-1} equals the identity. Researchers building the Recognition-Science candidate for the Hilbert-Pólya operator invoke this to obtain formal unitarity of the shifts. The proof reduces the claim to basis vectors via extensionality, applies the single-action lemmas for each operator, and cancels the index shift by abelian addition.
Claim. Let $p$ be prime. Let $V_p$ be the prime-shift operator and $V_p^{-1}$ its inverse on the free $ℝ$-module over the multiplicative indices. Then $V_p ∘ V_p^{-1} = id$.
background
The module builds an algebraic skeleton for a candidate Hilbert-Pólya operator on StateSpace, the free $ℝ$-module on MultIndex (the free abelian group on primes, isomorphic to $ℚ_{>0}^×$). The Recognition cost J induces the diagonal operator diagOp; shiftOp p and shiftInvOp p implement multiplication and division by p on the underlying rational. The module documentation lists the structural symmetries required of the candidate, including reciprocal symmetry of the cost and formal unitarity of the shifts.
proof idea
The proof applies the extensionality tactic to an arbitrary vector v. It simplifies the composition with the lemmas shiftInvOp_single and shiftOp_single together with the definitions of linear-map composition and Finsupp singletons. The resulting index equation is discharged by the congr tactic followed by abelian cancellation.
why it matters
This supplies the unitarity relation V_p ∘ V_p^{-1} = id required by the master certificate hilbert_polya_candidate_certificate. It closes one of the four structural properties enumerated in the module documentation for the Recognition-Science candidate. The result sits inside the program that translates the J-cost reciprocal symmetry J(x) = J(1/x) into operator-level intertwining with the multiplicative involution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.