involutionOp_involutive
plain-language theorem explainer
The reciprocal involution operator U on the free real module over multiplicative indices satisfies U composed with itself equals the identity. Researchers constructing Recognition Science candidates for the Hilbert-Pólya operator would cite this to confirm the involutive symmetry that mirrors the zeta functional equation. The proof is a direct one-line wrapper that applies function extensionality followed by simplification on the definition of U.
Claim. Let $U$ be the reciprocal-involution operator on the free real module over the multiplicative index space. Then $U^2 = id$.
background
The module builds an algebraic skeleton for a Hilbert-Pólya candidate on the free real module StateSpace over MultIndex, the free abelian group on primes. The Recognition Science cost J induces the diagonal operator diagOp, while the symmetry J(q) = J(1/q) induces the involutionOp U that sends each basis vector at index v to the basis vector at -v. Upstream results supply the reciprocal automorphism from CostAlgebra and the reciprocal event from LedgerForcing, which together define U as the linear extension of the map q to 1/q.
proof idea
The proof applies function extensionality to reduce the linear-map equality to a pointwise check on vectors v. Simplification then unfolds the definition of involutionOp (built from the reciprocal map) and verifies that two applications recover the original vector.
why it matters
This theorem supplies one of the three structural properties collected in the master certificate hilbert_polya_candidate_certificate. It confirms that the reciprocal involution is its own inverse, consistent with the J-cost symmetry and the Recognition Science reciprocal event. The result thereby supports the module's construction of an operator whose intertwining relations mirror the zeta functional equation, while leaving open the spectral question of whether eigenvalues match the imaginary parts of the zeta zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.