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 Hilbert orthogonal projection onto a closed subspace
Definition
Assume the Axiom of Countable Choice. Let be a closed linear subspace of a real or complex Hilbert space (Linear subspace of a vector space). By the orthogonal-decomposition theorem (Orthogonal decomposition by a closed subspace) every has a unique representation
and the Hilbert orthogonal projection onto is the map
assigning to its unique -component. Its defining properties are therefore
which characterise uniquely: a map with these defining properties must agree with the -component of the unique decomposition of each .
Agreement with the finite-dimensional projection. If is a finite-dimensional inner-product space and a subspace, then For a subspace of a finite-dimensional inner product space, writes and The orthogonal projection is the -component in defines as the unique -component of ; the defining properties displayed above are the same, so they define the same map on a finite-dimensional Hilbert space.
Range and kernel. for every , and for because with ; conversely says exactly that . Hence the range of is and its kernel is , and is the identity on and zero on .