module module high

`IndisputableMonolith.NumberTheory.HilbertPolyaCandidate`

This module defines the multiplicative index for positive rationals as finitely supported functions from primes to integers. It supplies conversions toRat and costAt together with basic arithmetic lemmas. The definitions are imported by CostOperatorRegularity to construct the dense domain of finite-support states for the cost operator T_J. The module contains only definitions and supporting lemmas with no theorems.

claimThe index for the multiplicative group is the type of finitely supported functions from the set of primes to integers, equipped with toRat mapping each index to an element of the positive rationals and costAt evaluating the associated J-cost.

background

The module supplies number-theoretic infrastructure inside the Recognition Science formalization. Its doc-comment states that the index for the multiplicative group of positive rationals is a finitely-supported function from primes to integers. Sibling definitions include MultIndex (the type itself), toRat (the conversion back to a positive rational), costAt (the cost evaluation), and lemmas such as toRat_zero, toRat_add, toRat_neg that encode the group law. The module imports Cost to access the underlying J-cost and is used to build finite-support states.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the index structure required by the downstream CostOperatorRegularity module. That module constructs the dense domain of finite-support states, proves symmetry on the domain, and states the three regularity sub-conjectures (essential self-adjointness, discrete spectrum, trace-class) for the candidate cost operator T_J. The index therefore anchors the operator-theoretic treatment of the Hilbert-Polya candidate inside the Recognition framework.

scope and limits

Does not define or construct the cost operator T_J.
Does not prove symmetry or any spectral property.
Does not state the regularity sub-conjectures.
Does not connect indices to zeta zeros or the Riemann hypothesis.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.CostOperatorRegularity module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (29)

abbrev MultIndex L60
def toRat L64
def costAt L68
theorem toRat_zero L70
theorem toRat_pos L73
theorem toRat_add L81
theorem toRat_neg L92
theorem costAt_neg_eq L102
abbrev StateSpace L110
def diagOp L122
theorem diagOp_single L126
def shiftOp L134
theorem shiftOp_single L138
def shiftInvOp L145
theorem shiftInvOp_single L148
def involutionOp L155
theorem involutionOp_single L158
theorem involutionOp_involutive L165
theorem involutionOp_diagOp_comm L171
theorem involutionOp_shiftOp L181
theorem involutionOp_shiftInvOp L191
theorem shiftOp_shiftInvOp L202
theorem shiftInvOp_shiftOp L211
def primeHop L224
theorem involutionOp_primeHop L229
def candidateOp L243
theorem involutionOp_sum_primeHop L249
theorem involutionOp_candidateOp L268
theorem hilbert_polya_candidate_certificate L279