costAt_neg_eq
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that the spectrum of the candidate operator matches the imaginary parts of the non-trivial zeta zeros.
- Does not construct the Hilbert space completion or establish essential self-adjointness.
- Does not derive any explicit eigenvalue formulas or numerical spectra.
- Applies strictly to the algebraic free module, without analytic continuation or convergence issues.
formal statement (Lean)
102theorem costAt_neg_eq (v : MultIndex) : costAt (-v) = costAt v := by
proof body
Term-mode proof.
103 unfold costAt
104 rw [toRat_neg]
105 exact (Jcost_symm (toRat_pos v)).symm
106
107/-! ## The state space: free ℝ-module on `MultIndex` -/
108
109/-- The pre-Hilbert space: free `ℝ`-module on `MultIndex`. -/