Alphabeta Math
TheoremStatement: AI-adaptedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passverified 2026-08-05 (gpt-5.6-sol-codex-subscription)
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 squeeze theorem

Statement

Let (ak)(a_k), (xk)(x_k) and (bk)(b_k) be sequences of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) with

akxkbkeventually,a_k \le x_k \le b_k \quad \text{eventually},

and suppose (ak)(a_k) and (bk)(b_k) both converge to the same real LL (Limits and Cauchy sequences of reals). Then (xk)(x_k) converges to LL.

The middle sequence is not assumed to converge; that is the point of the theorem, and it is why the squeeze is a tool for establishing convergence rather than for computing a limit already known to exist.

Facts & Assumptions

Given: Sequences (ak)(a_k), (xk)(x_k), (bk)(b_k) of reals, an index K0NK_0 \in \mathbb{N} with akxkbka_k \le x_k \le b_k for every kK0k \ge K_0, and a real LL such that (ak)(a_k) converges to LL and (bk)(b_k) converges to LL (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L1]

Convergence, quantified over rational ε>0\varepsilon > 0 (Limits and Cauchy sequences of reals).

[L2]

Absolute value: for c>0c > 0, u<c|u| < c if and only if c<u<c-c < u < c (Basic properties of the absolute value).

[L3]

Order arithmetic in R\mathbb{R}: adding a constant preserves << and \le; u<vwu < v \le w and uv<wu \le v < w both give u<wu < w; and \le is transitive (Order is preserved by adding a constant and by adding inequalities, Complete ordered field (least-upper-bound property), Ordered field).

[L4]

The order on N\mathbb{N} is total and transitive, so three indices K0,K1,K2K_0, K_1, K_2 admit an index KK with KK0K \ge K_0, KK1K \ge K_1 and KK2K \ge K_2, and then kKk \ge K gives kK0k \ge K_0, kK1k \ge K_1, kK2k \ge K_2 (\le is a linear order on N\mathbb{N}).

Proof

technique · direct
1.1

Let ε>0\varepsilon > 0 be rational. By convergence of (ak)(a_k) there is K1K_1 with akL<ε|a_k - L| < \varepsilon for all kK1k \ge K_1, and by convergence of (bk)(b_k) there is K2K_2 with bkL<ε|b_k - L| < \varepsilon for all kK2k \ge K_2.

L1
2.1

By [L2], akL<ε|a_k - L| < \varepsilon gives ε<akL-\varepsilon < a_k - L, that is Lε<akL - \varepsilon < a_k, for all kK1k \ge K_1; and bkL<ε|b_k - L| < \varepsilon gives bkL<εb_k - L < \varepsilon, that is bk<L+εb_k < L + \varepsilon, for all kK2k \ge K_2.

step 1.1L2L3
3.1

Choose KK with KK0K \ge K_0, KK1K \ge K_1 and KK2K \ge K_2. For every kKk \ge K the hypothesis gives akxkbka_k \le x_k \le b_k, so Lε<akxkbk<L+εL - \varepsilon < a_k \le x_k \le b_k < L + \varepsilon, hence Lε<xk<L+εL - \varepsilon < x_k < L + \varepsilon, hence ε<xkL<ε-\varepsilon < x_k - L < \varepsilon, hence xkL<ε|x_k - L| < \varepsilon.

step 2.1givenL2L3L4choose
4.1

The rational ε>0\varepsilon > 0 was arbitrary, so for every rational ε>0\varepsilon > 0 there is an index KK beyond which xkL<ε|x_k - L| < \varepsilon; that is, (xk)(x_k) converges to LL.

step 3.1L1

Remarks

  • The proof is direct from the definition and does not route through Limits preserve non-strict inequalities. It could not: that lemma assumes the middle sequence converges, which is what is being proved here.

  • Both bounding sequences must have the same limit. With ak=1a_k = -1, bk=1b_k = 1 and any (xk)(x_k) taking values in [1,1][-1, 1] the hypothesis akxkbka_k \le x_k \le b_k holds and nothing whatever follows, since a bounded sequence need not converge (FALSE: every bounded sequence converges).

  • The most common use is with ak=cka_k = -c_k and bk=ckb_k = c_k for a null sequence (ck)(c_k): if xkck|x_k| \le c_k eventually and ck0c_k \to 0, then xk0x_k \to 0. That special case also follows from A null sequence times a bounded sequence is null whenever xkx_k is presented as a product of a null sequence and a bounded one, but the squeeze needs no such presentation.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 43 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources