denseDomain_mem
plain-language theorem explainer
Every state in the state space belongs to the dense domain of finite-support multiplicative-index states for the cost operator. Spectral theorists studying the J-cost operator T_J would cite this to confirm the domain is the full space before invoking Friedrichs extensions or resolvent estimates. The proof is a one-line wrapper reducing directly to the definition of denseDomain.
Claim. For every state $f$ in the state space, $f$ belongs to the dense domain $D$ of finite-support multiplicative-index states.
background
The module establishes operator-theoretic foundations for the candidate cost operator $T_J$ on states derived from multiplicative indices. The dense domain $D$ is the subspace of finite-support states, which is dense in the underlying Hilbert space. Upstream results include the cost function defined as the J-cost of recognition events, the multiplicativity of J-automorphisms, and the recovery map toRat from logic rationals to rationals.
proof idea
The proof is a one-line wrapper that applies the definition of denseDomain, which by construction contains every finitely-supported state.
why it matters
This theorem supplies the first structural fact in the regularity certificate, which compiles all zero-sorry facts for the cost operator. It supports the sub-conjectures on essential self-adjointness, compact resolvent, and trace-class heat kernel by ensuring the domain is the full state space. The result sits inside the Recognition Science number-theory layer that prepares the phi-ladder mass formula and the eight-tick octave for spectral analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.