involutionOp_shiftInvOp
The theorem states that the reciprocal involution operator U satisfies U ∘ V_p^{-1} = V_p ∘ U for the prime-shift operator V_p on the free module over multiplicative indices. Researchers constructing algebraic models of the Riemann hypothesis cite this when checking that the candidate operator respects the zeta functional equation. The proof reduces the operator equality to an identity on basis vectors by direct simplification of the single-prime actions followed by abelian cancellation.
claimLet $U$ be the reciprocal involution operator and let $V_p$ be the shift operator for a prime $p$. Then $U ∘ V_p^{-1} = V_p ∘ U$.
background
The module builds an algebraic skeleton for a Hilbert-Pólya candidate on the free ℝ-module StateSpace over MultIndex (the free abelian group on primes, isomorphic to ℚ_{>0}^×). The operator involutionOp (U) implements the map q ↦ 1/q, which preserves J-cost by the sibling result costAt_neg_eq. The operators shiftOp p (V_p) and shiftInvOp p (V_p^{-1}) implement multiplication and division by p. This theorem is the symmetric counterpart to the sibling involutionOp_shiftOp, which gives U ∘ V_p = V_p^{-1} ∘ U. Upstream composition rules from CostAlgebra ensure the linear maps are well-defined.
proof idea
The proof extends the linear-map equality to an arbitrary vector v, then simplifies the compositions using the explicit single-basis actions shiftInvOp_single, involutionOp_single, and shiftOp_single together with Finsupp.lsingle_apply. A final congr 1 followed by abel equates the resulting coefficients in the free module.
why it matters in Recognition Science
This result is invoked directly in the proof of the downstream theorem involutionOp_primeHop, which shows that U commutes with the prime-hop operator V_p + V_p^{-1}. Combined with the earlier commutation involutionOp_diagOp_comm, the symmetries ensure the candidate operator respects the reciprocal symmetry of the zeta function. In the Recognition Science setting this mirrors the J-cost property J(x) = J(1/x) at the operator level, completing one of the structural requirements listed in the module for the algebraic skeleton. The open spectral question (whether the eigenvalues match the imaginary parts of the zeta zeros) remains untouched.
scope and limits
- Does not prove that the spectrum of the candidate operator coincides with the imaginary parts of zeta zeros.
- Does not address self-adjointness or domain questions for the unbounded operator on a completed Hilbert space.
- Applies only to the algebraic free module StateSpace, not to any L2 completion.
- Does not incorporate commutation with the diagonal cost operator diagOp.
Lean usage
rw [involutionOp_shiftInvOp p]formal statement (Lean)
191theorem involutionOp_shiftInvOp (p : Nat.Primes) :
192 involutionOp ∘ₗ shiftInvOp p = shiftOp p ∘ₗ involutionOp := by
proof body
Term-mode proof.
193 ext v
194 simp only [LinearMap.coe_comp, Function.comp_apply,
195 shiftInvOp_single, involutionOp_single, shiftOp_single,
196 Finsupp.lsingle_apply]
197 congr 1
198 abel
199
200/-- The shift and inverse-shift compose to the identity (formal unitarity
201 of `V_p`). -/