Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-10
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.

Perfect-set game strategy dichotomy on Cantor space

Statement

In ZF let A⊆C=2N. In each round I plays a finite binary block (possibly empty), then II plays a bit. I wins iff the concatenated sequence is in A. An I winning strategy yields a continuous injection C→A with compact closed image having no isolated points. A II winning strategy yields an injection A→N. Fixed block codes turn this into a natural-number game, with an illegal II bit losing immediately.

Facts & Assumptions

[F1]

Cantor and Baire sequence spaces and coordinate codings supplies countable finite-word codes, the cylinder topology, and compactness and absence of isolated points of C.

[F2]

Gale–Stewart games and strategies defines full-history strategies and winning plays.

Proof

Given: The block-and-bit game in the statement; no determinacy or choice axiom is assumed.

1.1F1F2

Enumerate all finite binary words by length and then lexicographic order, including the empty word first. This gives I's natural-number codes. II's numbers zero and one are legal bits; at the first other number declare I the winner. At each legal round at least one output bit is appended, so the concatenation is infinite. A winning strategy on the coded game never prescribes a first illegal move on its consistent legal histories, since the opponent can always continue legally; restriction thus gives the stated game.

1.2F1F2

Fix an I winning strategy σ. For z∈C let F(z) be the outcome against II's successive bits z(n). It lies in A by F2. If z,w first differ at n, their game histories through I's nth block are identical, and their next bits differ at the same output position, so F(z)≠F(w). If two inputs agree in their first m bits, the first m full rounds agree and append at least m bits, hence their outputs agree in their first m bits. Thus F is continuous.

1.3F1F2

Fix instead a winning II strategy τ and x∈A. A barrier for x is a finite legal full history h consistent with τ, ending before an I move, whose concatenation s is a prefix of x, such that for every finite block t with s⌢t⊂x, the response τ(h⌢t) differs from the next bit of x. If no such barrier existed, start with the empty history and at each round choose the least block code preserving agreement with x after τ responds. The absence of a barrier makes this set nonempty at each resulting history. Recursion constructs a full τ-play concatenating to x (lengths grow by at least one), contrary to x∈A. Hence a barrier exists.

2.1F1step 1.2

By F1 and the open-cover definition, the image of C under F is compact: pull a cover back, take a finite subcover, and push its coverage forward. A compact set K in a metric space is closed: for x∉K the balls B(y,d(x,y)/3) cover K; finitely many suffice, and the minimum of the finitely many positive radii gives a ball about x missing all those balls. Closed subsets of a compact space are compact, since adjoining their open complement to a cover gives a cover of the whole space. Consequently images under F of closed subsets of C are compact and closed; injectivity now says its inverse on the image takes inverse images of closed sets to closed sets. Thus F is a homeomorphism onto its image. That image has no isolated point because C has none by F1.

3.1F1step 1.3

A fixed barrier history h can serve at most one x. Its concatenation gives the first ∣s∣ bits. Recursively, after reconstructing the additional block t=x↾[∣s∣,∣s∣+j), recover the next bit as 1−τ(h⌢t). Each query uses the same fixed history h, not an evolving hypothetical history. The barrier property justifies every such recovered bit, including j=0 with empty t. Full finite histories have natural-number codes by iterated finite-word coding F1. Assign each x∈A the least code of its barriers. Existence follows from step 1.3 and uniqueness per code from this reconstruction, so this assignment is an injection into N. When A=∅ it is the empty injection. QED.

Depends on

Used by

Dependency tree · two levels

9 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