involutionOp_single
plain-language theorem explainer
The theorem establishes that the reciprocal involution operator U maps each basis element c · e_v in the free real module over multiplicative indices to c · e_{-v}. Researchers constructing Recognition Science candidates for the Hilbert-Pólya operator cite it when verifying the operator-level translation of the J-cost reciprocity J(q) = J(1/q). The proof is a one-line term simplification that unfolds involutionOp and applies the Finsupp mapDomain lemmas on singletons.
Claim. Let $v$ be a multiplicative index (finitely supported function from primes to integers) and let $c$ be a real coefficient. The reciprocal involution operator $U$ on the free real module satisfies $U(c · δ_v) = c · δ_{-v}$, where $δ_v$ is the standard basis vector at index $v$.
background
MultIndex is the type of finitely supported functions from the set of primes to the integers; it indexes the multiplicative group of positive rationals via the map toRat that sends $v$ to the product of primes raised to the exponents in $v$. The state space is the free real module on these indices, written StateSpace or MultIndex →₀ ℝ. The involutionOp is the linear operator that implements the reciprocal map on indices, sending each $v$ to $-v$ and thereby encoding the symmetry $J(q) = J(1/q)$ of the Recognition Cost function at the operator level.
proof idea
The proof is a one-line term-mode simplification. It unfolds the definition of involutionOp, then applies Finsupp.lmapDomain_apply followed by Finsupp.mapDomain_single to reduce the image of a singleton-supported vector directly to the negated-index singleton.
why it matters
This lemma is the base case used by involutionOp_shiftOp and involutionOp_shiftInvOp to obtain the intertwining relations $U ∘ V_p = V_p^{-1} ∘ U$. Those relations supply the operator-level analog of the zeta functional equation $ξ(s) = ξ(1-s)$. The result therefore closes one structural step in the algebraic skeleton of the Hilbert-Pólya candidate built from the Recognition Science cost function, consistent with the reciprocal automorphism in CostAlgebra and the forcing-chain symmetry at T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.