LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

A nonzero bounded linear operator is large on one of two nearby points

Statement

Let $T : X \to Y$ be nonzero and bounded (A bounded linear operator between normed spaces), let $x \in X$ , and let $r > 0$ . There is a $y \in B (x, r)$ such that

$∥ T y ∥ > \frac{2 r}{3} ∥ T ∥,$

where $∥ T ∥$ is The operator norm as the least bound and as the unit-sphere or unit-ball supremum.

Facts & Assumptions

Given: A nonzero bounded linear operator $T$ , $x \in X$ , and $r > 0$ .

Proof

technique · direct

1.1givenchoose

The unit-ball definition of the operator norm supplies $z$ with $∥ z ∥ \leq 1$ and $∥ T z ∥ > 8 ∥ T ∥ / 9$ .

2.1step 1.1algebra

Put $w = (3 r / 4) z$ . Then both $x + w$ and $x - w$ lie in $B (x, r)$ , and $∥ T w ∥ > 2 r ∥ T ∥ / 3$ .

3.1step 2.1algebra

The triangle inequality applied to $T (x + w) - T (x - w) = 2 T w$ gives $\max {∥ T (x + w) ∥, ∥ T (x - w) ∥} \geq ∥ T w ∥ > \frac{2 r}{3} ∥ T ∥ .$

4.1step 2.1step 3.1∎

Choosing the corresponding one of $x + w, x - w$ proves the claim.

Depends on

Used by

Sokal's gliding-hump proof of uniform boundedness Theorem

Dependency tree · two levels

6 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, p. 1 (standard reference, not scraped)