involutionOp_diagOp_comm
plain-language theorem explainer
The reciprocal involution operator commutes with the diagonal cost operator on the free R-module over multiplicative indices. Researchers constructing algebraic models of the Riemann hypothesis cite this as the operator-level counterpart of the zeta functional equation symmetry. The proof is a one-line wrapper that reduces the claim to the index-level identity J(1/q) = J(q) by extensionality and simplification.
Claim. Let $U$ be the reciprocal involution operator and $D$ the diagonal cost operator on the free $R$-module over multiplicative indices. Then $U D = D U$.
background
The module builds an algebraic skeleton for a Hilbert-Pólya candidate on the free R-module over Q>0^x (identified with the free abelian group on primes via MultIndex). Key objects are costAt (the Recognition cost J evaluated at the rational corresponding to an index), diagOp (the multiplication operator by these J-values), and involutionOp (the linear map induced by index negation, which encodes the reciprocal map q to 1/q). The local setting is the Recognition-Cost candidate for the Hilbert-Pólya operator; the module explicitly states that it does not prove the spectrum matches zeta zeros. The upstream lemma costAt_neg_eq supplies the index-level reciprocity J(1/q) = J(q) that drives the commutation.
proof idea
Apply linear-map extensionality to reduce equality of operators to their action on an arbitrary vector v. The resulting pointwise equality simplifies directly by the lemma costAt_neg_eq, which encodes the reciprocity of the cost function at negated indices.
why it matters
This commutation is one of the four structural properties collected in the master certificate hilbert_polya_candidate_certificate. It is invoked inside involutionOp_candidateOp to establish that the full candidate operator (diagOp plus prime shifts) commutes with the involution, mirroring the s ↔ 1-s symmetry of the completed zeta function. In the Recognition framework it realizes the reciprocal property of J at the operator level, consistent with the J-uniqueness and self-similar fixed-point steps of the forcing chain. The open spectral question (whether eigenvalues recover the imaginary parts of zeta zeros) remains untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.