costAt_neg_eq
plain-language theorem explainer
Reciprocal symmetry holds for the recognition cost at the multiplicative index level. For any index v the J-cost of the rational for -v equals the J-cost for v. Researchers building the Hilbert-Pólya candidate cite this symmetry to establish commutation between the diagonal cost operator and the reciprocal involution. The proof reduces directly by unfolding costAt, rewriting via the negation rule on toRat, and applying the Jcost symmetry lemma.
Claim. For every finitely supported integer-valued function $v$ on the primes, $J$ evaluated at the positive rational corresponding to $-v$ equals $J$ evaluated at the positive rational corresponding to $v$, where $J$ is the recognition cost function.
background
This module constructs the algebraic skeleton of a candidate Hilbert-Pólya operator on the free real vector space over the multiplicative indices. These indices are finitely supported maps from primes to integers; the map toRat converts an index v to the positive rational given by the product over primes of p raised to v(p). The costAt function then evaluates the J-cost at that rational. The local setting encodes the reciprocal symmetry J(q) = J(1/q) to mirror the zeta functional equation ξ(s) = ξ(1-s).
proof idea
The proof proceeds by term reduction. Unfold the definition of costAt to reach Jcost applied to toRat v. Rewrite the argument with toRat_neg, which replaces toRat(-v) by the reciprocal of toRat v. Apply the symmetry lemma Jcost_symm (using positivity of toRat v) and conclude with equality symmetry.
why it matters
The result supplies the reciprocal symmetry clause in the master certificate hilbert_polya_candidate_certificate that collects all structural properties of the candidate operator. It is invoked in the proof of commutation between the involution operator and the diagonal cost operator. Within the Recognition Science framework this realizes the reciprocal symmetry of J at the index level, supporting the intertwining that parallels the zeta functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.