Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck 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.

[0,1) is neither open nor closed in R

Statement refuted

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

The witness is the half-open interval E:=[0,1) (Intervals of R: the nine order-convex forms, nondegeneracy, and length). It fails openness at its left endpoint 0, which belongs to E while every neighbourhood of 0 reaches below 0, and it fails closedness at 1, which does not belong to E while every neighbourhood of 1 reaches into E. The refutation is carried out in full in FALSE: every subset of R is either open or closed and is recorded here as the named counterexample.

Facts & Assumptions

Given: The interval E:=[0,1)={ x∈R:0≤x<1 } (Intervals of R: the nine order-convex forms, nondegeneracy, and length).

[A1]

The refuted claim: every subset of R is open or closed.

[L1]
[L2]

U is open when every x∈U admits ε>0 with Nε(x)⊆U; F is closed when R∖F is open; Nε(x)={ y:∣y−x∣<ε } (Open subset of R (every point has a neighbourhood inside it), closed subset (complement open), and clopen, The ε-neighbourhood and the punctured ε-neighbourhood of a point of R).

[L3]

Every nonempty finite set of reals has a minimum, which is one of its members (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L4]

Absolute value: ∣z∣=z for z≥0 and ∣z∣=−z for z<0 (Basic properties of the absolute value); 0<1, so 2:=1+1>0 and 0<d⋅2−1<d for d>0; adding a constant preserves an inequality and the order is total (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

0∈E and 1∉E, so E is a legitimate instance of the claim [A1] and 1∈R∖E.

A1L4
1.2

E is not open: for a real ε>0 the point y:=−(ε⋅2−1) satisfies ∣y−0∣=ε⋅2−1<ε by [L4], so y∈Nε(0), while y<0 puts y outside E. Hence no neighbourhood of the point 0 of E is contained in E.

L1L2L4
1.3

E is not closed: for a real ε>0 put t:=min⁡{ε,1}⋅2−1, positive by [L3] and [L4], and y:=1−t; then t≤1⋅2−1 gives y≥1−1⋅2−1>0, and t>0 gives y<1, so y∈E; and ∣y−1∣=t≤ε⋅2−1<ε, so y∈Nε(1). Hence no neighbourhood of the point 1 of R∖E is contained in R∖E, so R∖E is not open.

L1L2L3L4
2.1

By steps 1.2 and 1.3 the set E is neither open nor closed, so the claim [A1] fails at E and is refuted.

step 1.1step 1.2step 1.3A1L1L2∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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