Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26
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.

⋂k(−1/k,1/k)={0} is not open

Statement refuted

Refuted claim: an arbitrary intersection of open subsets of R is open (FALSE: an arbitrary intersection of open subsets of R is open, Open subset of R (every point has a neighbourhood inside it), closed subset (complement open), and clopen).

The witness is Uk:=(−1/k, 1/k) for k≥1: each Uk is a nonempty open interval, the family is nested, and

⋂k≥1(−1k, 1k)  =  {0},

which is not open. The index runs over k≥1 because 1/0 is undefined; read as a family indexed by N it is j↦(−1/(j+1), 1/(j+1)). The refutation is carried out in full in FALSE: an arbitrary intersection of open subsets of R is open and is recorded here as the named counterexample. The comparison worth keeping in view is the finite case: any finite subfamily of {Uk} has intersection the smallest of its members, which is open.

Facts & Assumptions

Given: For each natural k≥1 the interval Uk:=(−1/k, 1/k), where 1/k is the inverse of the canonical natural k⋅1R.

[A1]

The refuted claim: for every family of open subsets of R, the intersection is open.

[L1]

Each Uk is open, the intersection of the family is {0}, and {0} is not open (FALSE: an arbitrary intersection of open subsets of R is open).

[L2]

U is open when every point of it has a neighbourhood inside it, and each interval (a,b) is an open set; Nε(x)={ y:∣y−x∣<ε } (Open subset of R (every point has a neighbourhood inside it), closed subset (complement open), and clopen, Intervals of R: the nine order-convex forms, nondegeneracy, and length, The ε-neighbourhood and the punctured ε-neighbourhood of a point of R).

[L3]

Reciprocal Archimedean property: for every real ε>0 there is a natural n≥1 with 1/n<ε (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean).

[L4]

Canonical naturals are positive for k≥1 and their inverses are positive (Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order); ∣z∣≥0 with ∣z∣=0 only for z=0, and ∣z∣<c exactly when −c<z<c for c>0 (Basic properties of the absolute value); 0<1, so 2:=1+1>0 and 0<d⋅2−1<d for d>0 (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property)). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.

Counterexample

technique · direct
1.1

Each Uk is a nonempty open subset of R, being the interval (−1/k,1/k) with 1/k>0, so the family { Uk:k≥1 } is an instance of the claim [A1], which asserts that its intersection is open.

A1L1L2L4
1.2

0∈Uk for every k≥1, since ∣0∣=0<1/k by [L4].

L1L4
2.1

If x≠0 then ∣x∣>0 by [L4], so [L3] supplies a natural n≥1 with 1/n<∣x∣, and x∈Un would give ∣x∣<1/n, which trichotomy forbids; hence x∉Un. With step 1.2 this gives ⋂k≥1Uk={0}.

step 1.2L3L4
3.1

The singleton {0} is not open, since for every real ε>0 the point ε⋅2−1 lies in Nε(0) and differs from 0 by [L4]. So the family of step 1.1 consists of open sets and its intersection, computed in step 2.1, is not open: the claim [A1] is refuted.

step 1.1step 2.1A1L1L2L4∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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