Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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 ACω. Let X be Banach and Y normed over the same field K{R,C}. Let (Tk)kN, with N={0,1,}, be a given sequence of bounded linear maps XY. If xX Mx[0,) kN:TkxMx, then there is M[0,) with TkM for every k. Completeness of Y, Hahn–Banach, Dependent Choice, and full Choice are not hypotheses.

Facts & Assumptions

Given: The spaces, sequence, pointwise bounds, and ACω in the statement.

[F1]

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).

[F2]

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).

[F3]

Every nonempty subset of N has a least element (The well-ordering principle).

[F4]

Countable Choice selects one member from each nonempty set in a given N-indexed family (The Axiom of Countable Choice (ACω)); only this defining clause is assumed.

[F5]

A fixed total map AA and starting element determine a unique recursive sequence (The recursion theorem).

[F6]

Properties with a zero base and a successor step hold for all naturals (The principle of mathematical induction).

[F7]

The two-sign bound applies to any bounded linear S:XY and any two domain vectors (Two signs detect an operator increment).

[F8]

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).

[F9]

Integer powers of nonzero reals are defined and obey addition-of-exponents and product laws (Integer powers am, Laws of integer exponents).

[F10]

In a complete ordered field, natural numbers are cofinal, and for each η>0 some positive natural has reciprocal less than η (Every complete ordered field is Archimedean, For every ε>0 in a complete ordered field there is a natural n1 with 1/n<ε).

[F11]

Banach completeness gives a limit in X for every norm-Cauchy sequence (Banach space).

Proof

technique · contradiction
1.1

By the real least-upper-bound property the nonempty unit-ball image sets of each bounded Tk have finite suprema. For any bounded S and z0, z/z is in the unit ball, so Sz=zS(z/z)Sz; for z=0 both sides vanish. If X={0} or Y={0} all operators are zero and M=0 works.

F1F2givenalgebra
1.2

The inequality 3nn+1 holds at n=0; if it holds at n, then 3n+13(n+1)n+2. Induction proves it for all n, and hence 3n1/(n+1). Given η>0, the reciprocal Archimedean assertion gives N1 with 1/N<η; for all nN, 3n1/(n+1)1/N<η. Thus 3n0.

F1F6F9F10algebra
2.1

Suppose instead that the operator norms have no finite upper bound. For every integer n1, the set {kN:Tk4n} is nonempty. Let kn be its unique least element and set Sn=Tkn. These uniquely specified indices define a sequence in ZF, with Sn4n>0. They need not be strictly increasing.

assume-contraF3F9step 1.1
3.1

Fix n1 and put a=Sn>0. Since 2a/3<a, the unit-ball supremum supplies w with w1 and Snw>2a/3. This w is nonzero. Thus v=w/w satisfies v=1 and Snv=Snw/w>2a/3. Hence the explicitly specified set En={vX:v=1, Snv>2Sn/3} is nonempty. This establishes nonemptiness separately for arbitrary n, without selecting all such w.

F2step 1.1step 2.1algebra
4.1

Apply ACω once to the family (Er+1)rN, obtaining vnEn for every n1. All these vectors are now fixed independently of subsequent partial sums. Set un=3nvn; then un=3n.

F4F9step 3.1algebra
5.1

For n1 and zX, define e(n,z)=1 if Sn(z+un)Sn(zun), and e(n,z)=1 otherwise. In particular ties take 1. The function f:N×XN×X given by f(r,z)=(r+1,z+e(r+1,z)ur+1) is total and single-valued. Recursion from (0,0) gives g; its first coordinate is r at stage r, because it starts at zero and increases by one. Induction therefore allows us to write g(r)=(r,xr), where x0=0 and xn=xn1+e(n,xn1)un. This construction uses no Dependent Choice.

F5F6step 4.1
6.1

The sign rule and the two-sign lemma give SnxnSnun=3nSnvn>(2/3)3nSn, and xnxn1=3n, for every n1.

F7step 4.1step 5.1algebra
7.1

For m>n0, repeated triangle inequalities give xmxnj=n+1m3j: the one-term case is step 6.1, and adjoining the next increment adds at most its norm, proving the assertion by induction on mn. If q=j=n+1m3j, scaling and cancelling the common terms in 3qq gives 2q=3n3m. Consequently q=(3n/2)(13(mn))3n/2. For m=n the sum and the distance are both zero.

F6F8F9step 6.1algebra
8.1

Given η>0, choose N so that 3N/2<η. For m,nN, step 7.1, symmetry, and the decreasing powers bound xmxn by 3N/2<η. Thus (xn) is Cauchy, and the stated completeness of X gives one xX with xxm0.

F11step 7.1step 1.2given
9.1

For fixed n and every m>n, xxnxxm+3n/2. Therefore xxn3n/2: a positive excess d would be contradicted by taking m>n with xxm<d/2.

step 7.1step 8.1algebra
10.1

For every n1, the triangle inequality applied to Snxn=Snx+Sn(xnx) gives SnxSnxnSnxnx>(1/6)3nSn(1/6)(4/3)n.

F9step 1.1step 2.1step 6.1step 9.1algebra
11.1

Induction gives (4/3)n1+n/3: equality holds at zero, and multiplication by 4/3 sends 1+n/3 to 1+(n+1)/3+n/91+(n+1)/3. For the given bound Mx, Archimedean cofinality supplies a natural n1 with n>18Mx. Then step 10.1 yields Tknx>(1/6)(1+n/3)>Mx, contradicting the pointwise bound. Thus a finite uniform bound exists.

F1F6F9F10step 10.1givendischarge-contradiction

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

Used by

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