LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

The bilateral shift metric is a metric, cylinders are its basic balls, and the shift space is sequentially compact

Statement

Let $X = {0, 1}^{Z}$ , let $d$ and $σ$ be the metric expression and the shift map of The bilateral two-symbol shift space, its metric, its shift map and its cylinder sets, and for $m \geq 0$ let $F_{m} : = {- m, \dots, m}$ and $[s]_{F_{m}} : = {t \in X : t_{k} = s_{k} for k \in F_{m}}$ be the cylinder determined by $s$ on $F_{m}$ . Then:

$d$ is a metric on $X$ (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric);
for every $s \in X$ and every $m \geq 0$ ,

$B (s, 2^{- m}) \subseteq [s]_{F_{m}} \subseteq \overline{B} (s, 2^{1 - m});$

consequently every cylinder is open in the metric topology (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement) and every nonempty open subset of $X$ contains a cylinder; 3. $X$ is sequentially compact (Countably compact, sequentially compact and limit point compact metric spaces): every sequence in $X$ has a subsequence converging in $d$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ), and the construction of that subsequence uses no choice principle; 4. granting the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) and the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain), $(X, d)$ is compact (Open cover, subcover, compact metric space, and compact subset of a metric space).

Facts & Assumptions

Given: The set $X$ of bi-infinite binary sequences, the expression $d (s, t) = \sum_{k \geq 0} 2^{- k} ∣ s_{k} - t_{k} ∣ + \sum_{k \geq 1} 2^{- k} ∣ s_{- k} - t_{- k} ∣$ , and the cylinders $[s]_{F_{m}}$ .

[F1]

The real absolute value satisfies $∣ a + b ∣ \leq ∣ a ∣ + ∣ b ∣$ (The triangle inequality). The geometric series satisfies $\sum_{k \geq 0} 2^{- k} = 2$ and $\sum_{k = m + 1}^{\infty} 2^{- k} = 2^{- m}$ for $m \geq 0$ ; a series of nonnegative reals converges if and only if its partial sums are bounded, and convergent series may be added termwise and compared termwise (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges, A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum, Convergent series add and scale termwise, Series, partial sums, convergence and the sum, divergence, and the tail series, Lower bound, bounded below, bounded set).

[F2]

Balls and topology: $B (s, ε) = {t : d (s, t) < ε}$ and $\overline{B} (s, ε) = {t : d (s, t) \leq ε}$ for the metric $d$ ; a set is open when every point of it has a ball contained in it; a metric space carries the topology induced by its balls (Open ball, closed ball and sphere in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

[F3]

A subset $D \subseteq X$ is dense when every nonempty open subset meets $D$ (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets).

[F4]

A metric space is sequentially compact when every sequence has a convergent subsequence; compact, countably compact, limit point compact and sequentially compact metric spaces coincide, and this equivalence is proved under the Axioms of Countable and Dependent Choice (Open cover, subcover, compact metric space, and compact subset of a metric space, Countably compact, sequentially compact and limit point compact metric spaces, For a metric space, compact, countably compact, limit point compact, sequentially compact, and complete together with totally bounded are all equivalent, given countable choice and dependent choice, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

Proof

technique · direct; verify the metric axioms, identify cylinders with balls up to a factor two, and diagonalise a sequence of binary sequences

1.1givenF1F2algebra

The expression $d (s, t)$ is a sum of two convergent series of nonnegative terms by [F1], since $∣ s_{j} - t_{j} ∣ \leq 1$ ; hence it is a nonnegative real and $d (s, t) = d (t, s)$ because $∣ s_{j} - t_{j} ∣ = ∣ t_{j} - s_{j} ∣$ . If $s \neq t$ there is $j \in Z$ with $s_{j} \neq t_{j}$ ; the corresponding term of $d (s, t)$ is positive and all terms are nonnegative, so $d (s, t) > 0$ . Finally, for $s, t, u \in X$ the termwise inequality $∣ s_{j} - t_{j} ∣ \leq ∣ s_{j} - u_{j} ∣ + ∣ u_{j} - t_{j} ∣$ and [F1] give $d (s, t) \leq d (s, u) + d (u, t)$ after multiplying by $2^{- ∣ j ∣}$ and adding the two one-sided series. Hence $d$ is a metric, which is clause 1.

1.2givenF1F2algebra

Fix $s \in X$ and $m \geq 0$ . If $t \in B (s, 2^{- m})$ then $2^{- ∣ j ∣} \leq d (s, t) < 2^{- m}$ for every $j$ with $∣ j ∣ \leq m$ and $t_{j} \neq s_{j}$ ; since $2^{- ∣ j ∣} \geq 2^{- m}$ there, no such $j$ exists, so $t \in [s]_{F_{m}}$ . Conversely, if $t \in [s]_{F_{m}}$ then all terms with $∣ j ∣ \leq m$ vanish and the remaining terms are at most $2^{- ∣ j ∣}$ ; hence $d (s, t) \leq \sum_{∣ j ∣ > m} 2^{- ∣ j ∣} = 2 \cdot 2^{- m} = 2^{1 - m}$ , that is $t \in \overline{B} (s, 2^{1 - m})$ . This proves the two inclusions of clause 2.

1.3givenF1F2

Let $(x_{n})_{n \geq 0}$ be a sequence in $X$ . Define $F_{m} = {- m, \dots, m}$ and construct subsequences $(x_{n}^{(m)})_{n \geq 0}$ recursively: $x_{n}^{(0)} : = x_{n}$ , and given $(x_{n}^{(m - 1)})$ , the map $n \mapsto x_{n}^{(m - 1)} ∣_{F_{m}}$ takes values in the finite set ${0, 1}^{F_{m}}$ , so some value $r_{m}$ occurs for infinitely many $n$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences); let $r_{m}$ be the lexicographically least such value (with respect to a fixed enumeration of $F_{m}$ ), and let $i_{0}^{(m)} < i_{1}^{(m)} < \dots$ enumerate the infinite set ${n : x_{n}^{(m - 1)} ∣_{F_{m}} = r_{m}}$ ; define $x_{j}^{(m)} : = x_{i_{j}^{(m)}}^{(m - 1)}$ . This is a simultaneous recursive construction with no choice: each $r_{m}$ is selected by a least-element rule, and each increasing enumeration is defined by least-element recursion on an infinite subset of $N$ . For $m \geq 1$ every term of $(x_{n}^{(m)})$ has restriction $r_{m}$ to $F_{m}$ , and each $(x_{n}^{(j)})$ with $j \geq m$ is a termwise subsequence of $(x_{n}^{(m)})$ .

2.1step 1.2F2F3algebra

Every cylinder $[w]_{p, q}$ is open: if $t \in [w]_{p, q}$ and $M : = \max {∣ p ∣, ∣ q ∣}$ , then any $u$ with $d (t, u) < 2^{- M}$ satisfies $u_{j} = t_{j}$ for every $∣ j ∣ \leq M$ by the argument of step 1.2, hence $u \in [w]_{p, q}$ ; thus $B (t, 2^{- M}) \subseteq [w]_{p, q}$ . Conversely, if $V \subseteq X$ is nonempty and open and $s \in V$ , choose $ε > 0$ with $B (s, ε) \subseteq V$ and $m$ with $2^{1 - m} < ε$ ; then step 1.2 gives $[s]_{F_{m}} \subseteq \overline{B} (s, 2^{1 - m}) \subseteq B (s, ε) \subseteq V$ . Hence cylinders are open and form a basis for the topology, as claimed in clause 2.

2.2step 1.21.3F1F2algebra

Put $y_{j} : = x_{j}^{(j)}$ ; the indices of the original sequence at which $y_{j}$ sits are strictly increasing in $j$ , so $(y_{j})$ is a subsequence. For $m \geq 1$ , if $j, j^{'} \geq m$ , then $y_{j}$ and $y_{j^{'}}$ both have restriction $r_{m}$ to $F_{m}$ by step 1.3, so $d (y_{j}, y_{j^{'}}) \leq \sum_{∣ k ∣ > m} 2^{- ∣ k ∣} = 2^{1 - m}$ ; hence $(y_{j})$ is a Cauchy sequence in $(X, d)$ . Define $s \in X$ by $s_{k} : = r_{m} (k)$ for every $m \geq \max {1, ∣ k ∣}$ ; this is well defined because $r_{m + 1} ∣_{F_{m}} = r_{m}$ for $m \geq 1$ (every term of $(x_{n}^{(m + 1)})$ is a term of $(x_{n}^{(m)})$ , so the restriction of $r_{m + 1}$ to $F_{m}$ stabilises the same value). Then $d (y_{j}, s) \leq 2^{1 - m}$ for every $j \geq m \geq 1$ , so $y_{j} \to s$ by [F2]. This proves clause 3.

3.1step 2.2F4∎

Clause 4 follows from clause 3 and [F4], which turns sequential compactness into compactness under the two stated choice axioms.

Remarks

The metric can be written with the symmetric weight $2^{- ∣ k ∣}$ : for $s, t \in X$ , splitting the sum at $k = 0$ shows $d (s, t) = \sum_{k \in Z} 2^{- ∣ k ∣} ∣ s_{k} - t_{k} ∣$ in the sense that the two defining one-sided series are exactly the positive- and negative-index parts. The one-sided form is used here because it avoids a two-sided summation convention.
The diagonal construction of step 1.3 is canonical: the value $r_{m}$ is the least stabilised restriction, and the increasing enumeration of an infinite subset of $N$ is produced by least-element recursion. Countable choice is used only when compactness is read off from sequential compactness in clause 4, which is why that clause is stated as a separate hypothesis.

The bilateral shift metric is a metric, cylinders are its basic balls, and the shift space is sequentially compact

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources