denseDomain_nonempty
plain-language theorem explainer
The set of finitely-supported states serving as the domain for the cost operator is non-empty, as it contains the zero vector. Researchers formalizing the spectral theory of the J-cost operator would cite this when initializing the domain for symmetry and extension arguments. The proof is a direct term-mode construction that exhibits the zero state together with the trivial membership witness.
Claim. The set of finitely-supported multiplicative-index states is non-empty.
background
The module constructs the operator-theoretic foundations for the cost operator T_J by defining a dense domain of finite-support states, proving symmetry on that domain, and encoding three regularity sub-conjectures as hypothesis structures. The dense domain is introduced as the full state space because the type StateSpace = MultIndex →₀ ℝ already encodes finite support, so the universal set coincides with the intended subspace. Upstream, the definition of denseDomain records this identification explicitly, while the contains predicate from StakeGraph supplies list-membership checks used in related constructions.
proof idea
The proof is a one-line term that applies the definition of Nonempty by supplying the zero state as witness and the trivial proof of membership in the universal set.
why it matters
This result supplies the first structural fact in the regularity chain for the cost operator, confirming that the domain is available before symmetry and the sub-conjectures EssentialSelfAdjointness, CompactResolvent, and TraceClassHeatKernel are stated. It closes the non-emptiness requirement inside the module that prepares T_J as a legitimate spectral object, with zero sorry. No downstream uses are recorded yet; the fact remains a prerequisite for any later spectral analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.