Alphabeta MathHow 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.
Discontinuous linear functionals on infinite-dimensional Banach spaces are not available in ZF + DC
Remark
On an infinite-dimensional Banach space, the existence of a discontinuous linear functional is a choice-sensitive statement. Full Choice gives one immediately from an infinite Hamel basis: pick the basis, prescribe an unbounded coefficient functional on it, and extend linearly. The opposite direction is not a theorem of ZF + DC. Howard and Tachtsis record the consistency boundary, and Heil's discussion of Hamel bases spells out the elementary "basis gives an unbounded functional" half.
The point for this page is negative rather than positive: the explicit discontinuous functional on the companion example below lives on the incomplete space , not on a Banach space. That distinction is exactly why this remark is kept separate from the example and why it never serves as a dependency.
Used by
Dependency tree · 0 levels
Nothing. This result depends on no other item in the library.
Sources
- Christopher Heil, A Basis Theory Primer (standard reference, not scraped)
- Paul Howard and Eleftherios Tachtsis, On infinite-dimensional Banach spaces and weak forms of the axiom of choice (standard reference, not scraped)