module module high

`IndisputableMonolith.NumberTheory.HilbertPolyaCandidate`

This module defines MultIndex as the finitely supported functions from primes to integers, indexing the multiplicative group of positive rationals. Researchers formalizing the cost operator T_J in Recognition Science would cite it when building the state space for spectral analysis. The module supplies supporting definitions and lemmas on toRat and costAt with no proofs.

claimLet $M$ be the set of finitely supported functions from the primes to $Z$. The map toRat sends each such index to an element of $Q_{>0}^×$, and costAt evaluates the J-cost at that index.

background

The module sits in the NumberTheory domain and imports only Mathlib and IndisputableMonolith.Cost. Its central definition, MultIndex, is described as the index for the multiplicative group $Q_{>0}^×$: a finitely-supported function from primes to integers. Sibling definitions include toRat (conversion to rationals), costAt (evaluation of the cost function), StateSpace (finite-support states), and the diagonal and shift operators diagOp and shiftOp.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the state space and index structure required by the downstream module CostOperatorRegularity, which constructs the dense domain $D$ of finite-support states and states the three regularity sub-conjectures for the cost operator $T_J$. It therefore supplies the concrete objects on which essential self-adjointness, discrete spectrum, and trace-class properties are later imposed.

scope and limits

Does not prove any spectral properties of the cost operator.
Does not reference the forcing chain T0-T8 or the Recognition Composition Law.
Does not define the cost operator $T_J$ itself.
Does not address the alpha band or mass ladder.

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