denseDomain_nonempty
plain-language theorem explainer
The theorem states that the dense domain of finitely-supported multiplicative-index states for the cost operator is non-empty. Spectral theorists working on the J-cost operator regularity would cite this before invoking symmetry or self-adjointness results. The proof is a one-line term exhibiting the zero state and invoking its membership in the universal set.
Claim. The set of finitely-supported states in the multiplicative-index space is non-empty.
background
The module formalizes operator foundations for the candidate cost operator T_J. It defines denseDomain as the set of all states in StateSpace, where StateSpace consists of finitely-supported functions from multiplicative indices to reals; the doc-comment notes that this makes the full state space itself the dense subspace. The local setting is the construction of a dense domain D of finite-support states prior to symmetry and the three regularity sub-conjectures (essential self-adjointness, compact resolvent, trace-class heat kernel).
proof idea
The proof is a one-line term that selects the zero state and applies the trivial membership fact for the universal set.
why it matters
This non-emptiness fact is the first structural result in the CostOperatorRegularity module, which compiles to zero sorry before stating the hypothesis structures for essential self-adjointness and related conjectures. It supplies the populated domain required for subsequent operator-theoretic claims in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.