module module high

`IndisputableMonolith.NumberTheory.HilbertPolyaCandidate`

This module defines MultIndex as the index set for the multiplicative group of positive rationals, realized as finitely supported functions from primes to integers. It supplies toRat to recover the rational and costAt to evaluate the J-cost. Researchers building the Hilbert-Polya candidate cite it to construct the dense domain of finite-support states for the cost operator T_J. The module consists of definitions and elementary algebraic lemmas.

claimLet $M$ be the type of finitely supported functions from the primes to $Z$. The map toRat sends $m$ in $M$ to the corresponding element of $Q_{>0}$, while costAt evaluates the J-cost on the index.

background

The module belongs to the NumberTheory section and imports the Cost module to access the underlying J-cost. Its central object is MultIndex, defined per the module doc-comment as an index for the multiplicative group $Q_{>0}^×$ via finitely supported prime-to-integer maps. Sibling definitions include toRat for conversion to rationals, costAt for cost evaluation, and lemmas toRat_zero, toRat_pos, toRat_add, toRat_neg, costAt_neg_eq that record the basic algebraic behavior of these maps on the index set.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the concrete index set and finite-support state constructions that feed the CostOperatorRegularity module. The downstream module uses these objects to build the dense domain $D$ of finite-support states and to state the three regularity sub-conjectures for the candidate cost operator $T_J$. It therefore supplies the multiplicative-index realization required for the Hilbert-Polya candidate inside the Recognition framework.

scope and limits

Does not establish spectral properties or self-adjointness of any operator.
Does not reference the phi-ladder, forcing chain, or physical constants.
Does not prove essential self-adjointness or trace-class claims.

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