involutionOp_primeHop
plain-language theorem explainer
The reciprocal involution operator commutes with the primeHop operator for each prime p. Researchers constructing algebraic models of the Riemann zeta function would cite this when verifying that the candidate operator respects the functional equation symmetry at finite truncations. The proof unfolds primeHop as the sum of shift and inverse-shift operators, distributes the compositions, substitutes the known intertwining relations, and reorders terms via addition commutativity.
Claim. Let $U$ be the reciprocal involution operator and let $V_p$ be the shift operator for a prime $p$. Then $U$ commutes with $V_p + V_p^{-1}$: $U ∘ (V_p + V_p^{-1}) = (V_p + V_p^{-1}) ∘ U$.
background
The module builds an algebraic skeleton for a candidate Hilbert-Pólya operator on the free real module over the multiplicative index space (free abelian group on the primes). The diagonal cost operator applies the J-cost function at each rational, the shift operator for prime p multiplies the index by p, and the involution operator implements the map sending each rational q to 1/q. This last map preserves J-cost because J(x) equals J(1/x). The module documentation states that the reciprocal symmetry of the zeta functional equation is mirrored by the intertwining of the involution with the shifts.
proof idea
The term proof first unfolds the definition of primeHop p. It distributes the linear-map composition over addition using the two distributivity lemmas for composition. It then substitutes the established intertwining relations involutionOp_shiftOp and involutionOp_shiftInvOp. Finally it invokes addition commutativity to equate the two sides.
why it matters
This theorem is invoked by involutionOp_sum_primeHop, which lifts the commutation to arbitrary finite weighted sums of primeHop operators by induction on the finset. It supplies one of the structural symmetries required for the candidate operator T_S(λ) to respect the reciprocal involution, exactly as described in the module documentation on mirroring the zeta functional equation. In the Recognition framework this step translates the J-cost reciprocity property into an operator-level identity before any spectral analysis begins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.