Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Norm of a self adjoint operator from its quadratic form

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let H be a real or complex Hilbert space (Hilbert space) and let TB(H) be a bounded self-adjoint operator (Self-adjoint, positive, unitary and normal operators, A bounded linear operator between normed spaces), with operator norm T (The operator norm as the least bound and as the unit-sphere or unit-ball supremum). Put q(x):=Tx,x for xH and

M:=sup{q(x):x=1},

with the convention that a supremum over the empty set of reals is 0; the empty case occurs only for H={0}, where the only operator is T=0. Then

T=M=supx=1Tx,x.

The identity holds over both scalar fields, and in the case H={0} both sides equal 0.

Facts & Assumptions

Given: A real or complex Hilbert space H, a bounded self-adjoint operator T, the quadratic form q(x)=Tx,x, and M=sup{q(x):x=1} with the empty-supremum convention.

[A1]

Self-adjointness is the identity Tx,y=x,Ty for all x,y: a self-adjoint operator satisfies T=T, and the Hilbert adjoint is characterised by Tx,y=x,Ty (Self-adjoint, positive, unitary and normal operators, The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities).

[A2]

Inner-product algebra. The pairing is linear in the first argument, conjugate-linear in the second, conjugate symmetric, and positive definite, and v2=v,v (Real and complex inner-product spaces and their induced length). Consequently for real t>0 and x,yH one has T(tx),t1y=tt1Tx,y=Tx,y, the expansion q(x±u)=q(x)±Tx,u±Tu,x+q(u) holds, and if Tx,u is real then self-adjointness gives Tu,x=Tx,u=Tx,u, so that q(x+u)q(xu)=4Tx,u. For z0 with unit vector u=z/z one has q(z)=z2q(u).

[A3]

Parallelogram law. x+u2+xu2=2x2+2u2 for all x,uH (Pythagoras, the parallelogram identity, and the real and complex polarisation identities).

[A4]

Operator norm and Cauchy–Schwarz. TvTv and T=sup{Tv:v1} (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, A bounded linear operator between normed spaces); v,wvw (Cauchy–Schwarz: x,yxy, with equality exactly for dependent pairs), so the dual norm formula z=sup{z,y:y=1} holds for every zH by Cauchy–Schwarz and by testing y=z/z when z0 (both sides are 0 at z=0).

[A5]

Choice. Countable Choice is the hypothesis under which this pair's Hilbert-space interface is stated; no choice is used inside the argument below (The Axiom of Countable Choice (ACω)).

Proof

technique · direct

Given: Countable Choice, a real or complex Hilbert space H, a bounded self-adjoint T, and M=sup{q(x):x=1}.

1.1

The quadratic form is dominated by M. For zH, if z=0 then q(z)=0=Mz2, while if z0 then [A2] gives q(z)=z2q(u) for the unit vector u=z/z, hence q(z)=z2q(u)Mz2.

A2algebra
1.2

MT. For every unit vector x, Cauchy–Schwarz and the norm bound give q(x)=Tx,xTxxT, so T is an upper bound of the set whose supremum is M; hence MT, and when H={0} both numbers are 0.

A4algebra
2.1

A sesquilinear bound. For all x,yH one has Tx,yM2(x2+y2): if x=0 or y=0 then Tx,y=0 and the right side is 0; otherwise put c:=Tx,y, and if c0 choose the unit scalar ω with ωc=c (namely ω=c/c over C, ω=sign(c) over R) and set u:=ωy, so that u=y and Tx,u=ωc=c0 is real; then [A2] gives 4Tx,y=4Tx,u=q(x+u)q(xu)q(x+u)+q(xu)M(x+u2+xu2) by [step 1.1], and the parallelogram law [A3] turns the last factor into 2x2+2u2=2x2+2y2.

step 1.1A1A2A3algebra
3.1

Removing the norms. For x,y0 and every real t>0, [step 2.1] applied to the pair (tx,t1y) together with the scaling identity of [A2] gives Tx,yM2(t2x2+t2y2); the right side is minimised at t2=y/x>0, where it equals Mxy, so Tx,yMxy for all x,yH (the zero cases being trivial).

step 2.1A2algebra
4.1

TM. For x0 the dual norm formula [A4] gives Tx=supy=1Tx,yMx by [step 3.1] with y=1, and the inequality also holds at x=0; thus M is a uniform bound for T on the unit ball, so TM by the unit-ball characterisation of the operator norm in [A4].

step 3.1A4algebra
5.1

Conclusion. Steps 1.2 and 4.1 give T=M; if H={0} then T=0, M=0 by the empty-supremum convention and T=0, so the identity holds there as well.

step 1.2step 4.1A5

Depends on

Used by

Dependency tree · two levels

34 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