shiftOp_shiftInvOp
plain-language theorem explainer
The theorem establishes that the prime-shift operator V_p and its inverse V_p^{-1} compose to the identity linear map on the free real module over multiplicative indices, for each prime p. Researchers modeling the Hilbert-Pólya conjecture via Recognition Science cost functions would cite this to confirm formal unitarity of the shift components. The proof reduces the map equality to basis vectors via extensionality, applies the single-action lemmas for shift and inverse-shift, then cancels the net exponent change with abelian arithmetic.
Claim. For each prime number $p$, let $V_p$ be the linear operator on the free real module over multiplicative indices that increments the exponent of $p$ by one. Then $V_p$ composed with its inverse $V_p^{-1}$ (which decrements the exponent of $p$ by one) equals the identity linear map.
background
The module builds an algebraic skeleton for a candidate Hilbert-Pólya operator on the free real module StateSpace over MultIndex (the free abelian group on primes, isomorphic to positive rationals). The Recognition cost J induces the diagonal operator diagOp via costAt, while shiftOp p and shiftInvOp p realize multiplication and division by p at the index level. This setup encodes the reciprocal symmetry J(q) = J(1/q) that mirrors the zeta functional equation.
proof idea
The proof applies the ext tactic to reduce the linear-map equality to an identity of coefficients on each basis vector v. It then simplifies via the lemmas shiftInvOp_single and shiftOp_single, which replace the composite action by a single index shift of net zero. The congr 1 tactic aligns the resulting basis elements, after which abel cancels the opposing exponents in the additive group of indices.
why it matters
This result is invoked inside the master certificate hilbert_polya_candidate_certificate, which assembles the structural properties of the candidate operator: reciprocal symmetry of costAt, involutivity of the involution operator, commutation with diagOp, and the shift-inverse relation. It supplies the formal unitarity of each V_p, a prerequisite algebraic symmetry before the open spectral question of whether eigenvalues match the imaginary parts of zeta zeros can be posed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.