shiftInvOp_shiftOp
plain-language theorem explainer
The declaration proves that for any prime p the composition of the inverse prime-shift operator with the forward shift operator recovers the identity linear map on the free real module over multiplicative indices. Algebraic number theorists exploring Hilbert-Pólya candidates would reference this result to establish the invertibility of the hopping operators built from the J-cost. The term-mode proof reduces the claim to basis vectors via extensionality, applies the single-shift lemmas, and cancels in the additive group.
Claim. For each prime $p$, if $V_p$ denotes the linear shift operator associated to multiplication by $p$ on the state space and $V_p^{-1}$ its inverse, then $V_p^{-1} ∘ V_p = id$.
background
The module builds an algebraic skeleton for a candidate Hilbert-Pólya operator on the free ℝ-module StateSpace over MultIndex (the free abelian group on primes, isomorphic to ℚ_{>0}^×). The Recognition Science cost J induces the diagonal operator diagOp, while shiftOp p implements the multiplicative action by prime p and shiftInvOp p supplies its formal inverse. The reciprocal symmetry J(x) = J(1/x) is encoded via involutionOp, mirroring the zeta functional equation ξ(s) = ξ(1-s).
proof idea
The term proof applies extensionality to an arbitrary vector v, simplifies the composition via shiftOp_single, shiftInvOp_single, Finsupp.lsingle_apply and LinearMap.id_apply, then uses a congruence step followed by abelian cancellation on the coefficients.
why it matters
This supplies the left-inverse property for the prime-shift operators V_p, complementing the right-inverse listed among the module's main theorems (shiftOp_invertible). It supports the structural symmetries required for the candidate operator to intertwine with the involution that encodes J-reciprocity. The module explicitly leaves the spectral identification with zeta zeros as the open Hilbert-Pólya conjecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.