toRat_neg
The map sending a multiplicative index to its positive rational satisfies toRat of the negated index equals the reciprocal of toRat of the index. Researchers constructing the algebraic skeleton of a Hilbert-Pólya operator candidate cite this to obtain the reciprocal symmetry needed for the involution operator. The proof invokes additivity of toRat on the pair consisting of an index and its negative, substitutes the zero index whose image is one, then applies field simplification using positivity.
claimFor any element $v$ of the free abelian group on the primes, the positive rational associated to $-v$ equals the reciprocal of the positive rational associated to $v$.
background
The module constructs an algebraic model for a candidate Hilbert-Pólya operator on the free real module over the multiplicative group of positive rationals. MultIndex is the free abelian group on the primes, realized as finitely supported functions from primes to integers. The function toRat sends such an index to the real number obtained by taking the product over primes of each prime raised to the corresponding exponent; this recovers the positive rational represented by the index.
proof idea
The tactic proof first applies the additivity lemma toRat_add to the pair (-v, v), producing the relation toRat((-v) + v) equals toRat(-v) times toRat(v). It rewrites the left side using the fact that the sum is the zero index together with toRat_zero, yielding the product equal to one. Positivity of toRat(v) supplies the nonzero hypothesis for field_simp, after which linarith solves for the reciprocal.
why it matters in Recognition Science
This lemma supplies the index-level reciprocal symmetry that is lifted to prove costAt_neg_eq, which states that the J-cost is invariant under negation of the index. That invariance is used to show the diagonal cost operator commutes with the reciprocal involution operator, one of the structural relations required for the candidate to mirror the zeta functional equation. It therefore closes an algebraic prerequisite for the commutation theorems involutionOp_diagOp_comm and involutionOp_shiftOp in the Recognition Science treatment of the Hilbert-Pólya conjecture.
scope and limits
- Does not prove that the spectrum of the constructed operator coincides with the imaginary parts of the zeta zeros.
- Does not address self-adjointness or spectral properties on the completed Hilbert space.
- Applies only inside the algebraic free module on indices, not to continuous or analytic extensions.
- Does not derive the explicit form of the J-cost, only its symmetry under index negation.
Lean usage
theorem costAt_neg_eq (v : MultIndex) : costAt (-v) = costAt v := by unfold costAt; rw [toRat_neg]; exact (Jcost_symm (toRat_pos v)).symmformal statement (Lean)
92theorem toRat_neg (v : MultIndex) : toRat (-v) = (toRat v)⁻¹ := by
proof body
Tactic-mode proof.
93 have h_sum : toRat ((-v) + v) = toRat (-v) * toRat v := toRat_add (-v) v
94 have h_zero : ((-v) + v) = (0 : MultIndex) := by simp
95 rw [h_zero, toRat_zero] at h_sum
96 have hv_pos : 0 < toRat v := toRat_pos v
97 have hv_ne : toRat v ≠ 0 := ne_of_gt hv_pos
98 field_simp [hv_ne]
99 linarith [h_sum]
100
101/-- Reciprocal symmetry of `J` at the index level: `J(1/q) = J(q)`. -/