Alphabeta Math
ExampleConstruction: 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.

min(xy,1)\min(|x-y|, 1) on R\mathbb{R} has the usual topology and diameter at most 11

Example

On R\mathbb{R}, let dR(x,y)=xyd_{\mathbb{R}}(x,y) = |x-y| be the 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) and put

ρ(x,y):=min{xy, 1}(x,yR).\rho(x,y) := \min\{\, |x - y|,\ 1 \,\} \qquad (x, y \in \mathbb{R}).

Then:

  1. ρ\rho is a metric on R\mathbb{R}, uniformly equivalent and therefore topologically equivalent to dRd_{\mathbb{R}} (Topologically, uniformly and Lipschitz equivalent metrics on a set, Lipschitz equivalence implies uniform equivalence implies topological equivalence); so (R,ρ)(\mathbb{R},\rho) has exactly the usual topology of the real line.
  2. (R,ρ)(\mathbb{R},\rho) is a bounded metric space and diam(R)=1\operatorname{diam}(\mathbb{R}) = 1 in the metric ρ\rho (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space), whereas (R,dR)(\mathbb{R}, d_{\mathbb{R}}) is not bounded at all and has no diameter.

This is the concrete instance of min(d,1)\min(d,1) and d/(1+d)d/(1+d) are metrics uniformly equivalent to dd, so every metric space carries a bounded metric with the same topology on the real line, and it is the witness used for the failure of two plausible-sounding claims: that boundedness is topological, and that topologically equivalent metrics are Lipschitz equivalent.

Facts & Assumptions

Given: The real line with dR(x,y)=xyd_{\mathbb{R}}(x,y) = |x-y| and the function ρ=min{dR,1}\rho = \min\{d_{\mathbb{R}}, 1\}; the set D:={ρ(x,y):x,yR}D := \{\, \rho(x,y) : x, y \in \mathbb{R} \,\}.

[L2]

For any metric dd, the function min{d,1}\min\{d,1\} is a metric, is bounded with diameter at most 11 on a nonempty space, and is uniformly equivalent to dd (min(d,1)\min(d,1) and d/(1+d)d/(1+d) are metrics uniformly equivalent to dd, so every metric space carries a bounded metric with the same topology).

[L4]

The minimum of a two-element set of reals exists and is one of them (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set); 10=1|1 - 0| = 1 and 0<10 < 1 (Basic properties of the absolute value, Absolute value in an ordered field, The multiplicative identity is positive).

[L5]

The diameter is the least upper bound of the set of distances, so it is \ge every distance and \le every upper bound of them; and it is unique (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Suprema and infima are unique, Complete ordered field (least-upper-bound property), Ordered field).

Verification

technique · direct
1.1

By [L1] the function dRd_{\mathbb{R}} is a metric on R\mathbb{R} and R\mathbb{R} is not bounded in it.

L1
1.2

ρ(0,1)=min{01, 1}=min{1,1}=1\rho(0,1) = \min\{|0-1|,\ 1\} = \min\{1,1\} = 1, so 1D1 \in D.

L4
2.1

By [L2] applied to d=dRd = d_{\mathbb{R}}: ρ\rho is a metric on R\mathbb{R}, the space (R,ρ)(\mathbb{R},\rho) is bounded, diam(R)1\operatorname{diam}(\mathbb{R}) \le 1 in ρ\rho, and ρ\rho is uniformly equivalent to dRd_{\mathbb{R}}.

step 1.1L2
3.1

Claim 2: the diameter of R\mathbb{R} in ρ\rho is an upper bound of DD and 1D1 \in D by step 1.2, so it is 1\ge 1; combined with 1\le 1 from step 2.1 this gives diam(R)=1\operatorname{diam}(\mathbb{R}) = 1 in the metric ρ\rho, while by step 1.1 the space has no diameter at all in dRd_{\mathbb{R}}.

step 1.1step 1.2step 2.1L5
3.2

Claim 1: ρ\rho is a metric uniformly equivalent to dRd_{\mathbb{R}} by step 2.1, hence topologically equivalent to it, so the metric topology of ρ\rho is the usual topology of R\mathbb{R}.

step 2.1L3
4.1

Claims 1 and 2 hold by steps 3.2 and 3.1.

step 3.1step 3.2

Remarks

Depends on

Used by

Dependency tree · next 3 levels

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