Alphabeta Math
DefinitionDefinition: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Order on bounded self adjoint operators

Definition

Assume Countable Choice and let H be a nonzero complex Hilbert space. Write

B(H)sa:={TB(H):T=T}

for the set of bounded self-adjoint operators on H (Self-adjoint, positive, unitary and normal operators). For S,TB(H)sa define

ST(TS)x,x0for every xH.

Equivalently TS; the notation T0 is exactly the positivity of Self-adjoint, positive, unitary and normal operators. Operators are compared only when both are self-adjoint: the relation is not defined for a general pair in B(H), and no conjugate-linear or non-real quadratic form is admitted by the definition.

B(H)sa is a real vector space and is a partial order on it. Sums and real scalar multiples of self-adjoint operators are self-adjoint, because the adjoint is conjugate-linear and T=T (Hilbert-adjoint identities); the zero operator is self-adjoint. So the comparisons below are between elements of a real vector space.

  • Reflexivity. SS=0 and 0x,x=0, so SS.
  • Transitivity. If ST and TU, then for every x (US)x,x=(UT)x,x+(TS)x,x0, by additivity of the pairing in its first argument, so SU.
  • Antisymmetry. If ST and TS, then (TS)x,x=0 for every x. The sesquilinear form B(x,y):=(TS)x,y is linear in x and conjugate-linear in y and satisfies B(z,z)=0 for every z, so the four-term expansion 4B(x,y)=B(x+y,x+y)B(xy,xy)+iB(x+iy,x+iy)iB(xiy,xiy) vanishes for all x,y. Hence (TS)x,y=0 for all x,y, and fixing x and taking y=(TS)x gives (TS)x2=0, so TS=0 and S=T. The expansion is the displayed consequence of additivity and conjugate-linearity alone, so antisymmetry consumes no completeness of H (Hilbert space).

Two conventions. First, the order is a partial order on the real vector space of self-adjoint operators; it is not a total order, and the extrema of the spectrum in the later results are taken in R, not by comparing operators. Second, T0 refers to the quadratic form of a self-adjoint operator; the counterexample on the companion page shows that nonnegativity of the spectrum alone does not define positivity for operators that are not self-adjoint (The operator norm as the least bound and as the unit-sphere or unit-ball supremum for the operator data used throughout).

Depends on

Used by

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources