Alphabeta Math
LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedaudited 2026-09-22
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.

Uniform null G-delta sets capture block functions

Statement

There are uniformly assigned null Gδ sets Nf in Cantor space for f∈ωω and, for each open U whose canonical coin content is below one, finite capture sets φU(n) of size at most 2n+1, such that Nf⊆U implies f(n)∈φU(n) for all sufficiently large n. If f belongs to a transitive model, the code for Nf belongs to that model.

Facts & Assumptions

Given: Cantor space 2ω.

[F1]

Cantor and Baire sequence spaces and coordinate codings: the cylinder topology, compactness of Cantor space, coordinate pairing and explicit natural-number codes for finite binary words. The choice-free coin content needed here is constructed in step 1.1.

[F2]

The countable Borel hierarchy and its limit convention: the Gδ form of a countable intersection of open sets.

[F3]

Closed subspaces of complete metric spaces are complete; the converse under countable choice and [F1]: a closed subspace of Cantor space is complete; choosing the lexicographically least branch through each nonempty cylinder trace supplies a canonical countable dense subset. Hence Separable complete metric spaces are Baire in ZF makes every nonempty closed K⊆2ω a Baire space in ZF.

Proof

1.1F1construct

For an open O⊆2ω, let PO be the prefix-free set of shortest finite words s with [s]⊆O, and put ν(O)=∑s∈PO2−∣s∣, the supremum of its finite partial sums in the fixed word order. Define the closed content m(K)=1−ν(2ω∖K) and call E null when, for every k, it has an open cover of content below 2−k. Refining finitely many cylinders to one common length proves finite additivity on clopen sets, monotonicity, and countable subadditivity for open unions directly from binary-word counts. If K⊆D with K closed and D clopen, then m(K)≤ν(D). Every definition uses a fixed enumeration or a real supremum and hence exists in ZF.

2.1F1step 1.1

Using the canonical pairing from [F1], put Cn,m={⟨⟨n,m⟩,j⟩:j≤n} and Bn,m={x:∀c∈Cn,m x(c)=1}. The coordinate groups are disjoint and have size n+1. Refining to a prefix above the finitely many coordinates shows ν(Bn,m)=2−(n+1),ν(⋂(n,m)∈JBn,mc)=∏(n,m)∈J(1−2−(n+1)) for every finite J; this is a finite pattern count, not a product-measure theorem.

2.2F1step 1.1

Fix open U with ν(U)<1 and put K0=2ω∖U, so m(K0)>0. Enumerate the finite words as (si). Let Z be the union of those traces K0∩[si] with closed content zero. Such a compact zero-content trace has, for each requested rational error, a finite clopen cover of smaller content: choose a finite clopen subset of its open complement whose content is sufficiently close to one and take the complement. Choose the least finite cover in the fixed code order. Assigning error 2−i−k−2 to the pair (i,k) and taking the open union proves directly that Z is null, without Countable Choice. Put K=K0∖Z. The set Z is K0 intersected with the open union of the corresponding cylinders, so K is closed. Monotonicity gives m(K)≤m(K0), while the arbitrarily small canonical open covers of Z and the finite/open content inequalities give m(K0)≤m(K)+ε for every positive rational ε; hence m(K)=m(K0)>0. Every nonempty trace K∩[s] has positive closed content, since otherwise the corresponding K0∩[s] was removed.

3.1F2step 1.1step 2.1

For f:ω→ω put Nf=⋂k<ω⋃n≥kBn,f(n). It is Gδ by [F2]. For every k, its displayed tail union is an open cover of content at most ∑n≥k2−(n+1)=2−k by step 1.1, so Nf is null by the local definition. The assignment is arithmetic in f and the fixed blocks; therefore its code belongs to every transitive model containing f.

3.2step 1.1step 2.1step 2.2

For s∈TK={s:[s]∩K≠∅} put As(n)={m:K∩[s]∩Bn,m=∅}. For every finite J⊆{(n,m):m∈As(n)}, steps 1.1--2.2 give 0<m(K∩[s])≤∏(n,m)∈J(1−2−(n+1))≤exp⁡(−∑(n,m)∈J2−(n+1)). Taking canonical finite initial subsets shows that ∑n∣As(n)∣/2n+1 converges. Hence every As(n) is finite and ∣As(n)∣/2n+1→0.

4.1F3step 2.2step 3.1

Assume Nf⊆U, so K∩Nf=∅. If every K∩⋃n≥mBn,f(n) met every nonempty basic open subset of K, these sets would be dense open. The least-branch construction in [F3] makes K separable and complete in ZF, so the Baire theorem would make their intersection K∩Nf nonempty. Therefore some s∈TK and m satisfy K∩[s]∩⋃n≥mBn,f(n)=∅.

4.2F1step 3.2

Let i:2<ω→ω be the fixed bijection, and let n(s) be the least threshold after which ∣As(n′)∣/2n′+1≤2−i(s)−1. Put φU(n)=⋃{As(n):s∈TK, n(s)≤n}. For any finite E⊆φU(n), assign to each m∈E the least witnessing s in the fixed word order. Then ∣E∣2n+1≤∑s:n(s)≤n∣As(n)∣2n+1≤∑s2−i(s)−1≤1. If φU(n) had more than 2n+1 elements, its first 2n+1+1 elements would contradict this bound. Thus it is finite and has the required size.

5.1step 3.1step 4.1step 4.2

With s,m as in step 4.1 and ℓ=max⁡{m,n(s)}, every n≥ℓ satisfies K∩[s]∩Bn,f(n)=∅, hence f(n)∈As(n)⊆φU(n). Together with steps 3.1 and 4.2 this proves capture, the size bound and model-membership of the codes.

6.1step 3.1step 5.1∎

The steps above provide the uniformly assigned null Gδ sets and the capture sets with all stated properties, which is the Statement.

Depends on

Used by

Dependency tree · two levels

33 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