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.
Sequential uniform boundedness under countable choice
Statement
Work in ZF and assume . Let be Banach and normed over the same field . Let , with , be a given sequence of bounded linear maps . If then there is with for every . Completeness of , Hahn–Banach, Dependent Choice, and full Choice are not hypotheses.
Facts & Assumptions
Given: The spaces, sequence, pointwise bounds, and in the statement.
The library's reals have the least-upper-bound property and form a complete ordered field (The Cauchy-sequence reals have the least-upper-bound property).
The operator norm is the unit-ball supremum; the zero-domain norm is zero (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).
Every nonempty subset of has a least element (The well-ordering principle).
Countable Choice selects one member from each nonempty set in a given -indexed family (The Axiom of Countable Choice ()); only this defining clause is assumed.
A fixed total map and starting element determine a unique recursive sequence (The recursion theorem).
Properties with a zero base and a successor step hold for all naturals (The principle of mathematical induction).
The two-sign bound applies to any bounded linear and any two domain vectors (Two signs detect an operator increment).
Real finite sums include empty sums and obey scaling, splitting, and telescoping (Finite sums and finite products, by recursion, Laws of finite sums and finite products).
Integer powers of nonzero reals are defined and obey addition-of-exponents and product laws (Integer powers , Laws of integer exponents).
In a complete ordered field, natural numbers are cofinal, and for each some positive natural has reciprocal less than (Every complete ordered field is Archimedean, For every in a complete ordered field there is a natural with ).
Banach completeness gives a limit in for every norm-Cauchy sequence (Banach space).
Proof
By the real least-upper-bound property the nonempty unit-ball image sets of each bounded have finite suprema. For any bounded and , is in the unit ball, so ; for both sides vanish. If or all operators are zero and works.
The inequality holds at ; if it holds at , then . Induction proves it for all , and hence . Given , the reciprocal Archimedean assertion gives with ; for all , . Thus .
Suppose instead that the operator norms have no finite upper bound. For every integer , the set is nonempty. Let be its unique least element and set . These uniquely specified indices define a sequence in ZF, with . They need not be strictly increasing.
Fix and put . Since , the unit-ball supremum supplies with and . This is nonzero. Thus satisfies and . Hence the explicitly specified set is nonempty. This establishes nonemptiness separately for arbitrary , without selecting all such .
Apply once to the family , obtaining for every . All these vectors are now fixed independently of subsequent partial sums. Set ; then .
For and , define if , and otherwise. In particular ties take . The function given by is total and single-valued. Recursion from gives ; its first coordinate is at stage , because it starts at zero and increases by one. Induction therefore allows us to write , where and . This construction uses no Dependent Choice.
The sign rule and the two-sign lemma give , and , for every .
For , repeated triangle inequalities give : the one-term case is step 6.1, and adjoining the next increment adds at most its norm, proving the assertion by induction on . If , scaling and cancelling the common terms in gives . Consequently . For the sum and the distance are both zero.
Given , choose so that . For , step 7.1, symmetry, and the decreasing powers bound by . Thus is Cauchy, and the stated completeness of gives one with .
For fixed and every , . Therefore : a positive excess would be contradicted by taking with .
For every , the triangle inequality applied to gives .
Induction gives : equality holds at zero, and multiplication by sends to . For the given bound , Archimedean cofinality supplies a natural with . Then step 10.1 yields , contradicting the pointwise bound. Thus a finite uniform bound exists.
Remarks
The estimates adapt Sokal, printed p.2, equation (2) and the following proof. Selecting independent near-norming vectors before the deterministic sign recursion is the library's refinement; the precise axiom audit is not attributed to Sokal. MIT notes, Theorem 36, printed p.17 corroborate the sequence statement, and Teschl, §4.1, Corollary 4.4, printed p.103 gives the family formulation. Their Baire proofs are comparison material, not premises of this choice audit.
Depends on
- Two signs detect an operator increment
- The Cauchy-sequence reals have the least-upper-bound property
- The operator norm as the least bound and as the unit-sphere or unit-ball supremum
- Banach space
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- The well-ordering principle
- The recursion theorem
- The principle of mathematical induction
- Finite sums and finite products, by recursion
- Laws of finite sums and finite products
- Integer powers $a^m$
- Laws of integer exponents
- Every complete ordered field is Archimedean
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
Used by
- Coordinate partial sums on c₀ Example
Dependency tree · two levels
55 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
- Sokal, A really simple elementary proof of the uniform boundedness theorem (standard reference, not scraped)
- Lin and Rodriguez, MIT 18.102 Complete Lecture Notes (standard reference, not scraped)
- Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)