Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-10 (gpt-5.6-terra-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.

Dini's theorem fails on [0,): x/(ι(k+1)+x) decreases pointwise to zero but not uniformly

Statement refuted

Refuted claim: the compact-domain hypothesis in Dini's theorem can be dropped.

On [0,) define

fk(x):=xι(k+1)+x.

The functions fk and their pointwise limit 0 are continuous, and fk+1(x)fk(x) for every x0, but fk0 is not uniform.

Facts & Assumptions

Given: The functions fk in the Statement, with ak:=ι(k+1)>0.

[L3]

A subset of R is compact exactly when it is closed and bounded; [0,) is unbounded (A subset of R is compact if and only if it is closed and bounded, Lower bound, bounded below, bounded set).

[L4]

Dini's theorem on a closed interval concludes uniform convergence from continuity, pointwise monotonicity, and a continuous pointwise limit (Dini's theorem on a closed interval: monotone pointwise convergence of continuous functions to a continuous limit is uniform).

Counterexample

technique · direct
1.1

For every k, the denominator ak+x is positive on [0,), so fk is continuous by [L1]; the zero function is continuous as well.

givenL1
1.2

Since ak+1>ak>0, one has ak+1+x>ak+x>0, hence fk+1(x)fk(x) for every x0.

L2algebra
1.3

Fix x0. If x=0 then fk(x)=0; if x>0, then 0fk(x)x/ak, and [L2] gives x/ak0. Thus fk(x)0 for every x.

L2algebra
1.4

At xk:=ak one has fk(xk)=ak/(ak+ak)=1/2, so the convergence is not uniform.

givenalgebra
1.5

The domain [0,) is not compact by [L3].

L3
2.1

Hence all the listed Dini hypotheses except compactness hold, while the uniform conclusion fails; compactness cannot be dropped.

step 1.1step 1.2step 1.3step 1.4step 1.5L4

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: 77 results over 17 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