StateSpace
plain-language theorem explainer
The pre-Hilbert space is the free real vector space on the multiplicative index group, the free abelian group generated by the primes. Number theorists and physicists constructing Recognition Science candidates for the Hilbert-Pólya operator cite this space as the domain for the diagonal cost operator and the prime-shift operators. The definition is a direct one-line abbreviation that instantiates the Finsupp type constructor on the index group.
Claim. The pre-Hilbert space is the free real vector space on the multiplicative index group (the free abelian group generated by the primes), consisting of all finitely supported functions from this group to the reals.
background
MultIndex is the free abelian group on the primes, written as finitely supported maps from primes to integers; the map toRat sends such an index to the corresponding positive rational interpreted as a real. costAt evaluates the Recognition Science cost function J at that rational, and the module builds operators on the resulting vector space. The local setting is the algebraic skeleton of a candidate Hilbert-Pólya operator whose diagonal part applies J and whose involution part implements the reciprocal symmetry J(q) = J(1/q). Upstream results supply the cost function via MultiplicativeRecognizerL4.cost and ObserverForcing.cost, which derive J from the Recognition Composition Law.
proof idea
This is a one-line abbreviation that directly applies the Finsupp construction to the multiplicative index group, producing the type of finitely supported real-valued functions on that group.
why it matters
This definition supplies the underlying vector space for diagOp, shiftOp, involutionOp and the candidateOp truncation in the same module, as well as the denseDomain and regularity certificate in CostOperatorRegularity. It realizes the pre-Hilbert space on which the Recognition Science cost J induces a diagonal operator that commutes with the involution mirroring the zeta functional equation. The open spectral question left explicit in the module documentation is whether the spectrum of the completed operator coincides with the imaginary parts of the non-trivial zeta zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.