involutionOp
plain-language theorem explainer
The reciprocal involution operator U maps each basis vector e_v of the free real module on multiplicative indices to e_{-v}. Researchers constructing Hilbert-Pólya candidates cite this definition to encode the reciprocal symmetry J(q) = J(1/q) at the operator level. The definition is a direct application of Finsupp.lmapDomain to the negation map on indices.
Claim. Let $H$ be the free real module on the multiplicative index space. The reciprocal involution operator $U : H → H$ is the linear map satisfying $U(e_v) = e_{-v}$ for every basis vector $e_v$.
background
The module builds an algebraic skeleton for a candidate Hilbert-Pólya operator on the free real module over the multiplicative group of positive rationals, using the Recognition Science cost function J. Key definitions include MultIndex as the free abelian group on primes (isomorphic to ℚ>0^×), StateSpace as the free ℝ-module on MultIndex serving as pre-Hilbert space, and the three operators: diagOp (diagonal cost), shiftOp (prime shifts), and involutionOp (reciprocal involution).
proof idea
This is a one-line definition that applies Finsupp.lmapDomain ℝ ℝ to the negation map on indices, inducing the linear map that sends each basis vector e_v to e_{-v}.
why it matters
This definition supplies the reciprocal involution U that appears in the master certificate hilbert_polya_candidate_certificate establishing structural properties of the candidate operator. It is used to prove involutionOp_involutive (U² = id), involutionOp_diagOp_comm, and involutionOp_shiftOp, which together encode the functional equation symmetry. In the Recognition Science framework it realizes the J(x) = J(1/x) property at the operator level, supporting the Hilbert-Pólya approach without claiming spectral identification with zeta zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.