involutionOp
The reciprocal involution operator U maps each basis vector e_v of the free real module on multiplicative indices to e_{-v}, realizing the map from a positive rational q to its reciprocal 1/q. Number theorists exploring Hilbert-Pólya approaches to the Riemann hypothesis cite this construction for the symmetry it encodes between the cost operator and prime shifts. The definition is a direct one-line application of Finsupp.lmapDomain to the negation map on indices.
claimLet $U$ be the linear endomorphism of the free real module on the multiplicative index space such that $U(e_v) = e_{-v}$ for each index $v$, where the map $v$ to $-v$ corresponds to the multiplicative inversion on the associated positive rational.
background
This definition sits inside the module that builds an algebraic candidate for the Hilbert-Pólya operator on the free real module StateSpace over MultIndex. MultIndex is the free abelian group on the primes, realized as finitely supported integer functions on Nat.Primes and mapped to positive rationals by toRat. The Recognition Science cost J satisfies J(q) = J(1/q) at the index level, which lifts to operator symmetries here.
proof idea
This is a one-line definition that applies Finsupp.lmapDomain ℝ ℝ to the negation function on indices, sending each basis vector e_v to e_{-v}.
why it matters in Recognition Science
This operator U supplies the reciprocal symmetry required by the master certificate hilbert_polya_candidate_certificate. It encodes the J-cost reciprocity at the operator level, yielding the commutation U D = D U and the intertwining U V_p = V_p^{-1} U that parallel the functional equation of the xi function. The construction leaves open whether the spectrum of the full candidate matches the imaginary parts of the zeta zeros.
scope and limits
- Does not prove that the spectrum of the candidate operator coincides with the imaginary parts of the zeta zeros.
- Does not complete the pre-Hilbert space to a Hilbert space or address domain issues.
- Does not establish self-adjointness of the candidate operator.
- Does not analyze the continuous spectrum or other spectral properties.
formal statement (Lean)
155def involutionOp : StateSpace →ₗ[ℝ] StateSpace :=
proof body
Definition body.
156 Finsupp.lmapDomain ℝ ℝ (fun v => -v)
157