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.
The operator norm as the least bound and as the unit-sphere or unit-ball supremum
Definition
Let and be normed spaces over the same scalar field, and let be bounded in the sense of A bounded linear operator between normed spaces. The operator norm of is
The set on the right contains and every bound for bounds it above. Thus its finite real supremum exists by the proved least-upper-bound property of the library's real field (The Cauchy-sequence reals have the least-upper-bound property). In particular every number strictly below the supremum is exceeded by a member of this set; otherwise it would be a smaller upper bound. No choice principle is used for this assertion.
The same number is the least bound of :
If , positive homogeneity also gives
When , the unit sphere is empty and the unit-ball supremum is , so .
Remarks
- The inequality holds for every by the unit-ball definition and rescaling.
- The unit-ball formula is the one used uniformly below, because it also covers the zero-space case without a separate convention.