Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Rudin shrinking obstruction

Statement

Assume AC. In X=XR(B) the sets Fk={h∈X:h(n)=ℵn for every n∈B with n≤k}, k<ω, are closed, decrease, and have empty intersection. For every sequence of open sets Uk⊇Fk there is b∈∏n∈Bℵn with

∅≠{h∈X:b<h}⊆⋂k<ωUk.

All inequalities are pointwise. In particular, no such open neighborhoods have empty intersection.

Facts & Assumptions

Given: The stated spaces, slices and open neighborhoods, in the AC setting.

[F1]

PB is the box product of the ordinal intervals [0,ℵn], B is an infinite subset of ω∖{0,1}, and XR(B) requires a uniform strict finite-aleph bound on uncountable coordinate cofinalities (Rudin ordinal box spaces on infinite index sets).

[F2]

Every open neighborhood of Fk contains a pointwise tail above a function in ∏n∈Bℵn (Neighborhoods of Rudin initial-top slices contain tails).

[F5]

α+β is the order type of a copy of α followed by a copy of β (α+β is the order type of α followed by β).

[A1]

AC supplies a countable choice of the existing tail bounds (The Axiom of Choice).

Proof

1.1F1F3

For a coordinate n, the set {h∈X:h(n)<ℵn} is open: it is the intersection with X of the box with factor [0,ℵn) at n and whole factors elsewhere, and [0,ℵn) is an open initial ray of the ordinal interval. Thus the set with h(n)=ℵn is closed. Each Fk is the intersection of finitely many such sets, hence closed, and Fk+1⊆Fk because it imposes all preceding equalities. The empty initial coordinate set gives F0=F1=X. If h belonged to every Fk, taking k=n would give h(n)=ℵn for every n∈B. F3 would make these coordinate cofinalities ℵn, which have no finite uniform aleph bound: the infinite subset B of the natural numbers is unbounded, since a bounded subset would be finite. This contradicts F1. Hence ⋂kFk=∅.

1.2F2F3F4A1

For every k, F2 gives a nonempty set of functions zk∈∏n∈Bℵn whose tails are contained in Uk. Use A1 to choose one for each k and put b(n)=sup⁡k<ωzk(n). Each ℵn is uncountable regular by F3, so F4 gives b(n)<ℵn. Thus b belongs to the product in the statement. If b<h with h∈X, then zk(n)≤b(n)<h(n) at every coordinate and every k. The defining property of zk puts h in every Uk.

2.1step 1.2F1F3F4F5F6

Define h(n)=b(n)+ω1 using ordinal addition. By F5 this is the order type of the disjoint ordered sum of b(n) and ω1. With μ=max⁡(∣b(n)∣,ℵ1), one has μ<ℵn because b(n)<ℵn and n≥2. F6 bounds that sum's cardinality by μ, hence its order type h(n) is below the initial ordinal ℵn: an ordinal at least ℵn would contain a copy of ℵn and have cardinality at least ℵn. The final copy of ω1 is cofinal in the sum, so cf⁡(h(n))≤ω1. A shorter cofinal set cannot exist. Its part in the final copy would be bounded there by regularity F3 and F4, and a larger point of that copy would then bound the entire set, including all points in the initial b(n) part. Therefore cf⁡(h(n))=ω1. The final copy is nonempty and has no largest point, so h(n)>b(n), also when b(n)=0. All coordinate cofinalities of h are ω1<ℵ2, so F1 gives h∈X.

3.1step 1.1step 1.2step 2.1

The point h in step 2.1 belongs to the tail above b, making that tail nonempty. Step 1.2 puts the entire tail in ⋂kUk, and step 1.1 gives the decreasing closed sequence with empty intersection. These are all the stated conclusions. QED.

Depends on

Used by

Dependency tree · two levels

40 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