MultIndex
plain-language theorem explainer
MultIndex supplies the free abelian group on the primes as the discrete index set for positive rationals in the Recognition Science candidate Hilbert-Pólya operator. Number theorists and spectral geometers working on zeta-zero realizations would cite it as the domain for the diagonal cost operator and its involution symmetries. The declaration is a direct type abbreviation with no lemmas or computational steps.
Claim. Let $M$ denote the set of all finitely supported functions from the set of prime numbers to the integers, written $M = P_0^0$ where $P$ is the set of primes.
background
In the Recognition Science construction of a candidate Hilbert-Pólya operator, the pre-Hilbert space is the free real module on the multiplicative group of positive rationals. MultIndex realizes this group as its index space: each element $v$ corresponds to a unique rational $q = toRat(v) = prod p^{v(p)}$ via the map supplied by the sibling definition toRat. The module imports the set Primes from EulerInstantiation and the multiplicativity property of J-automorphisms from CostAlgebra to ensure the cost function behaves compatibly under multiplication.
proof idea
The declaration is a direct abbreviation to the standard Finsupp type over the primes set with integer coefficients. No lemmas are invoked; it simply renames the Mathlib construction for local use in the module.
why it matters
MultIndex is the algebraic foundation on which costAt, diagOp, shiftOp and involutionOp are defined, and it supplies the domain for the master certificate hilbert_polya_candidate_certificate that records the reciprocal symmetry J(q) = J(1/q) together with the commutation relations mirroring the zeta functional equation. It realizes the T5 J-uniqueness and the free abelian group on primes inside the Recognition framework, leaving open the spectral identification with the imaginary parts of the zeta zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.