Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

In {0}[1,2]\{0\} \cup [1,2] with the metric of R\mathbb{R}, the closure of B(0,1)={0}B(0,1) = \{0\} is {0}\{0\} while the closed ball is {0,1}\{0,1\}

Statement refuted

Refuted claim: in every metric space, the closure of the open ball B(x,r)B(x,r) is the closed ball Bˉ(x,r)\bar B(x,r) (FALSE: in every metric space the closure of B(x,r)B(x,r) is the closed ball of radius rr).

The witness is the metric subspace

X:={0}[1,2]RX := \{0\} \cup [1,2] \subseteq \mathbb{R}

of the real line with its usual metric (The absolute value makes R\mathbb{R} a metric space: d(x,y)=xyd(x,y) = |x-y| is a metric, its open balls are the intervals (xr,x+r)(x-r, x+r), and it is unbounded, Isometry, isometric embedding, and the subspace metric on a subset, Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length), with x=0x = 0 and r=1r = 1. In it

BX(0,1)={0},BX(0,1)={0},BˉX(0,1)={0,1},B_X(0,1) = \{0\}, \qquad \overline{B_X(0,1)} = \{0\}, \qquad \bar B_X(0,1) = \{0,1\},

so the closure of the open ball is a proper subset of the closed ball of the same centre and radius. The inclusion B(x,r)Bˉ(x,r)\overline{B(x,r)} \subseteq \bar B(x,r) that does hold in general is proved in FALSE: in every metric space the closure of B(x,r)B(x,r) is the closed ball of radius rr and is not repeated.

Facts & Assumptions

Given: The real line with dR(u,v)=uvd_{\mathbb{R}}(u,v) = |u-v|, and X:={0}[1,2]X := \{0\} \cup [1,2] with the subspace metric d:=dR(X×X)d := d_{\mathbb{R}} \restriction (X \times X).

[L2]

Balls: BX(a,s)={yX:d(a,y)<s}B_X(a,s) = \{y \in X : d(a,y) < s\} and BˉX(a,s)={yX:d(a,y)s}\bar B_X(a,s) = \{y \in X : d(a,y) \le s\} (Open ball, closed ball and sphere in a metric space).

[L5]

Absolute value and order: t=t|t| = t for t0t \ge 0, t=t|-t| = |t|, and 0<10 < 1; by trichotomy t1t \ge 1 excludes t<1t < 1 (Absolute value in an ordered field, Basic properties of the absolute value, The multiplicative identity is positive, Ordered field, Complete ordered field (least-upper-bound property)).

[L6]

Intervals: [1,2]={tR:1t2}[1,2] = \{t \in \mathbb{R} : 1 \le t \le 2\} (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

Counterexample

technique · direct
1.1

Every y[1,2]y \in [1,2] has y1y \ge 1, so d(0,y)=0y=y=y1d(0,y) = |0-y| = |-y| = y \ge 1; and d(0,0)=0<1d(0,0) = 0 < 1.

L1L5L6
2.1

Hence BX(0,1)={yX:d(0,y)<1}={0}B_X(0,1) = \{\, y \in X : d(0,y) < 1 \,\} = \{0\}, since no y[1,2]y \in [1,2] satisfies d(0,y)<1d(0,y) < 1; and BˉX(0,1)={yX:d(0,y)1}={0,1}\bar B_X(0,1) = \{\, y \in X : d(0,y) \le 1 \,\} = \{0, 1\}, since among the points of [1,2][1,2] exactly y=1y = 1 satisfies y1y \le 1.

step 1.1L2L5L6
2.2

The set [1,2]=X{0}[1,2] = X \setminus \{0\} is open in XX: for y[1,2]y \in [1,2] the ball BX(y,1)B_X(y,1) cannot contain 00, because d(0,y)1d(0,y) \ge 1 by step 1.1, so BX(y,1)[1,2]B_X(y,1) \subseteq [1,2]. Therefore {0}\{0\} is closed in XX.

step 1.1L2L3
3.1

Since {0}\{0\} is closed it equals its own closure, so BX(0,1)={0}={0}\overline{B_X(0,1)} = \overline{\{0\}} = \{0\}, whereas BˉX(0,1)={0,1}\bar B_X(0,1) = \{0,1\} contains the point 101 \ne 0.

step 2.1step 2.2L4L5
4.1

The two sets are therefore different, and (X,d)(X,d) with x=0x = 0, r=1r = 1 refutes the claim: the closure of an open ball can be a proper subset of the closed ball of the same centre and radius.

step 3.1

Remarks

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: 48 results over 13 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