How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Injective resolvents need not be bounded below
Statement refuted
False assertion: for every densely defined nonnegative self-adjoint operator on a nonzero complex Hilbert space, if is injective then .
Statement references
Facts & Assumptions
Given: the Axiom of Choice, over , where , and the definitions of and in the Counterexample.
The Axiom of Choice: every family of nonempty sets has a choice function.
Positive unbounded spectral calculus from a bounded resolvent: under the Axiom of Choice, is bounded positive self-adjoint on a nonzero complex Hilbert space, and its compact spectrum has a unique regular spectral PVM on its Borel sets with ; the push-forward under has domain and operator , and the theorem permits while .
Cauchy–Schwarz: , with equality exactly for dependent pairs: for square-summable complex sequences , .
Counterexample
Given: [A1], [F1]–[F2], and the false assertion in the Statement.
On , with inner product and standard basis given by if and otherwise, all coordinate indices below range over . Define and . Finite sequences lie in and are dense. For , Cauchy–Schwarz [F2] gives , so and is nonnegative.
The operator is self-adjoint. If , there is with for every finite sequence ; choosing gives , so and . Conversely, if then satisfies the adjoint identity for every : both inner-product series converge by [F2] because , and their terms agree. Thus and .
The inverse of is the bounded diagonal operator . Indeed for any , satisfies , and . The operator is positive and injective, but it is not bounded below because for unit vectors . The vector belongs to : for , , so . It is not in , since would require for every , which is not square-summable. Hence is not surjective and .
Define for Borel . Its values are orthogonal coordinate projections, and the coordinate definition gives , , and . For disjoint Borel , each coordinate occurs in at most one projection, so the partial sums converge in to : the squared norm of the omitted coordinates is a tail of the convergent nonnegative series . Thus is strongly countably additive. It integrates the coordinate function to , because its integral acts diagonally by on each . For every , its finite scalar measure is . For any Borel , the finite set is compact and contained in , and because . Hence is inner regular on every Borel set. Since is compact, for any Borel and , inner regularity of gives a compact with ; then the open set contains and its excess measure is less than . Thus is also outer regular, so is a regular PVM. Hence [F1] identifies it with the bounded-resolvent spectral PVM. Since no atom is at zero, , although step 3.1 proves . This refutes the asserted implication and shows why a zero spectral projection must be distinguished from a spectral value.