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 with Countable Choice
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Completeness, Completion, and Uniform Continuity
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Simple Field Extensions and the Construction of the Complex Numbers
- Suprema and Infima
- The ZFC Axioms and the Basic Set Constructions
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
A pointwise bounded sequence of bounded linear maps on a Banach space has uniformly bounded norms under . The two-sign estimate supplies the local algebra. The proof then selects independent near-norming vectors once, fixes signs deterministically, and obtains a Cauchy sequence with an explicit geometric tail. Its limit contradicts pointwise boundedness if the operator norms are unbounded. All estimates work over the real or complex field, with no completeness assumption on the codomain.
The companion page calculates the coordinate projections on and shows why completeness matters on .
3 · Logical flowchart
4 · Definitions, theorems and proofs
Two signs detect an operator increment
Statement
Let be a bounded linear operator between normed spaces over the same field . For all , No completeness or choice principle is assumed.
Facts & Assumptions
Given: as above and .
A bounded linear operator is in particular linear, and its domain and codomain have the scalar homogeneity and triangle inequality of normed spaces (A bounded linear operator between normed spaces).
Proof
By linearity, .
Consequently . Division by the positive real number proves the claim, including , , and zero spaces.
Remarks
This is the algebraic estimate in Sokal, printed p.2, equation (2), written independently of the surrounding local-ball lemma. Boundedness is part of the operator interface; the calculation needs only linearity.
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.
5 · Examples, counterexamples and false statements
None yet.