Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02
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.

Rudin's bounded rational spikes are not equicontinuous and have no uniformly convergent subsequence

Statement refuted

Refuted: a uniformly bounded family of continuous functions on [0,1][0,1] must be equicontinuous or have a uniformly convergent subsequence.

Facts & Assumptions

Given: fn(x)=x2/(x2+(1−nx)2)f_n(x)=x^2/(x^2+(1-nx)^2) for 0≤x≤10\le x\le1.

[L1]

A uniform limit of continuous real functions is continuous (The uniform limit of continuous real-valued functions on a metric space is continuous).

Proof

technique · direct
1.1

Each fnf_n is continuous, 0≤fn≤10\le f_n\le1, fn(0)=0f_n(0)=0, and fn(1/n)=1f_n(1/n)=1.

givenalgebra
1.2

For every fixed x>0x>0, fn(x)→0f_n(x)\to0, while fn(0)=0f_n(0)=0. Thus any uniformly convergent subsequence would have the zero function as its pointwise limit, consistently with [L1].

givenL1algebra
2.1

The common values at 00 and 1/n→01/n\to0 contradict equicontinuity at 00.

step 1.1algebra
2.2

Uniform convergence to zero is impossible because ∥fn∥∞≥fn(1/n)=1\lVert f_n\rVert_\infty\ge f_n(1/n)=1.

step 1.1step 1.2algebra
3.1

This bounded family is neither equicontinuous nor uniformly sequentially compact.

step 2.1step 2.2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 55 results over 14 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