involutionOp_candidateOp
plain-language theorem explainer
The theorem establishes that the candidate Hilbert-Pólya operator commutes with the reciprocal involution on the free real module over multiplicative indices. Number theorists and physicists seeking operator models for the Riemann zeta zeros would cite this for the symmetry that lets the spectrum decompose into involution eigenspaces mirroring s to 1-s. The proof is a direct term-mode verification that unfolds the candidate as a linear combination of diagonal and shift operators then rewrites via the known commutation lemmas for each piece.
Claim. Let $U$ be the reciprocal involution operator on the free real module over the multiplicative indices, and let $C_{S,λ}$ be the candidate operator given by the diagonal cost operator plus a finite weighted sum of prime-shift operators for primes in the finite set $S$ with weights $λ$. Then $U ∘ C_{S,λ} = C_{S,λ} ∘ U$.
background
The module builds an algebraic skeleton for a Hilbert-Pólya candidate operator on the free real module StateSpace over the multiplicative index space MultIndex (the free abelian group on primes, isomorphic to the positive rationals). The Recognition Science cost function J induces the diagonal operator diagOp via costAt, while shiftOp p implements multiplication by each prime p; involutionOp implements the map sending each index vector to its negative, which corresponds to the rational reciprocal q to 1/q and preserves cost by the upstream fact costAt_neg_eq. The local setting is the Recognition-Cost candidate for the Hilbert-Pólya operator, whose main structural theorems include involutionOp_involutive, involutionOp_diagOp_comm, and involutionOp_shiftOp.
proof idea
The term proof unfolds candidateOp into diagOp plus a sum of lambda-weighted shiftOp terms. It distributes the composition with involutionOp using the linearity rules LinearMap.comp_add and LinearMap.add_comp, then applies the commutation lemmas involutionOp_diagOp_comm and involutionOp_sum_primeHop to obtain equality on each summand.
why it matters
This supplies the commutation property required by the downstream master certificate hilbert_polya_candidate_certificate, which assembles the reciprocal symmetry of the cost, the involutivity of the involution, and the commutation facts into a single structural statement. It realizes the Hilbert-Pólya-style symmetry that mirrors the zeta functional equation ξ(s) = ξ(1-s) inside the Recognition Science framework built from the J-cost fixed point and the eight-tick octave. The open spectral question of whether the eigenvalues match the imaginary parts of the non-trivial zeta zeros is left untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.