LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Completeness of the sup metric on finite-state value functions

Statement

For any finite set $S$ , let $B (S) = R^{S}$ , the set of real-valued functions on $S$ . Define

$d_{\infty} (U, V) = {\begin{cases} 0, & S = \emptyset, \\ \max_{s \in S} ∣ U (s) - V (s) ∣, & S \neq \emptyset . \end{cases}$

Then $d_{\infty}$ is a metric on $B (S)$ and $(B (S), d_{\infty})$ is complete.

Statement references

Mozgovoy, Lecture Notes on Metric Spaces and Functional Analysis.

Sutton and Barto, Reinforcement Learning: An Introduction.

Facts & Assumptions

Given: A finite set $S$ and the function space $B (S) = R^{S}$ .

[F1]

Finite, countably infinite, countable, uncountable: finiteness means there is a natural number $n$ and a bijection from $n = {0, \dots, n - 1}$ onto $S$ ; if $S$ is nonempty then $n \geq 1$ .

[F2]

$R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it: for $n \geq 1$ , $d_{\infty} (x, y) = \max_{k < n} ∣ x_{k} - y_{k} ∣$ and $d_{2} (x, y) = (\sum_{k < n} (x_{k} - y_{k})^{2})^{1 / 2}$ are metrics on $R^{n}$ .

[F3]

The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges: every Cauchy sequence of reals converges to a real.

[F4]

Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric and Complete metric space: every Cauchy sequence converges in the space: a metric satisfies separation, symmetry, and the triangle inequality; completeness means every Cauchy sequence converges in the same metric space.

[F5]

Cauchy sequence in a metric space, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , and Limits and Cauchy sequences of reals: metric Cauchy and convergence, as well as real Cauchy and convergence, are tested with rational $ε > 0$ .

[F6]

A sequence has at most one limit: a convergent real sequence has a unique limit.

[F7]

The well-ordering principle: every nonempty set of natural numbers has a least element.

[F8]

The principle of mathematical induction and $\leq$ is a linear order on $N$ : induction holds on $N$ , and its order is total.

Proof

1.1givenF4

If $S = \emptyset$ , then $B (S)$ has exactly one element, the empty function. Its only distance is $0$ ; nonnegativity, symmetry, separation, and the triangle inequality all hold on this singleton, and every sequence in it is constant and convergent.

1.2givenF1F2

Suppose $S \neq \emptyset$ . By [F1], fix $n \geq 1$ and a bijection $e : n \to S$ . Pulling functions back along $e$ identifies $B (S)$ with $R^{n}$ and carries $d_{\infty}$ exactly to the max metric of [F2]; hence it is a metric.

2.1step 1.2F2F5

Let $(U_{m})$ be Cauchy in $d_{\infty}$ on $B (S)$ . For each $j < n$ , define the real sequence $x_{m}^{(j)} : = U_{m} (e (j))$ . Given rational $ε > 0$ , the metric Cauchy condition supplies $K$ such that $d_{\infty} (U_{m}, U_{ℓ}) < ε$ for all $m, ℓ \geq K$ . Since the pulled-back $d_{\infty}$ is the maximum of the coordinate differences, $∣ x_{m}^{(j)} - x_{ℓ}^{(j)} ∣ < ε$ for every $j < n$ and $m, ℓ \geq K$ . Thus each coordinate sequence is Cauchy in $R$ .

3.1step 2.1F3F6

By [F3], each coordinate sequence converges. Denote its unique limit by $y_{j} \in R$ , using [F6].

4.1step 1.2step 3.1F1F6

Define $U : S \to R$ by $U (e (j)) : = y_{j}$ for $j < n$ . This is well defined because $e$ is a bijection, and it uses no choice because every $y_{j}$ is uniquely determined.

4.2step 3.1F5F7

Fix rational $ε > 0$ . For each $j < n$ , convergence to $y_{j}$ gives a nonempty set of natural thresholds $K$ such that $∣ x_{m}^{(j)} - y_{j} ∣ < ε$ for all $m \geq K$ . Let $K_{j}$ be its least member, using [F7].

5.1step 1.2step 4.2F8

The finite nonempty list $K_{0}, \dots, K_{n - 1}$ has a maximum $K$ : start with $K_{0}$ and, at each successor, retain the larger of the current maximum and the next threshold, which exists by the total order on $N$ ; induction proves the resulting value dominates every entry. Thus $K \geq K_{j}$ for all $j < n$ .

6.1step 1.2step 4.1step 5.1F2F4F5∎

For every $m \geq K$ , step 5.1 implies $∣ U_{m} (e (j)) - U (e (j)) ∣ < ε$ for every $j < n$ . Their finite maximum is one of these coordinate differences, so $d_{\infty} (U_{m}, U) < ε$ . Since this holds for every rational $ε > 0$ , $(U_{m})$ converges to $U$ in $d_{\infty}$ . Every Cauchy sequence therefore converges in $B (S)$ , and together with the metric property from steps 1.1–1.2 this proves completeness.

Remarks

The proof is a finite-coordinate Cauchy argument. The maximum norm makes each coordinate sequence Cauchy; completeness of the real line supplies its limit; one maximum of finitely many thresholds then gives convergence in the maximum norm.
The same argument proves completeness for the $d_{1}$ metric on $R^{n}$ . Each coordinate difference is at most $d_{1}$ . Given rational $ε > 0$ , choose for every coordinate a threshold at tolerance $ε / (2 n)$ , which is again a positive rational; after taking their finite maximum, monotonicity of finite sums gives $d_{1} (x^{(m)}, y) \leq n ε / (2 n) = ε / 2 < ε$ . The $d_{\infty}$ case is proved above. No later result on this page uses the $d_{1}$ observation.
No choice is spent. The limit point is assembled coordinatewise from unique limits, each threshold is the least one that works, and a common threshold is obtained by taking the maximum of finitely many indices.
The real completeness input is localised. The Cauchy criterion in $R$ is the only completeness theorem used. Its proof obtains real completeness from the least-upper-bound property through Bolzano–Weierstrass; the finite-coordinate argument adds no other completeness assumption.

Remarks references

The taxicab and supremum metrics.

Monotonicity and constant-summand laws for finite sums.

Depends on

Used by

Dependency tree · two levels

66 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

Sergey Mozgovoy, Lecture Notes on Metric Spaces and Functional Analysis (standard reference, not scraped)