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

The scale subspace is closed

Statement

Assume AC. The Kojman–Shelah scale subspace X is closed in XR(B).

Facts & Assumptions

Given: The scale subspace and a point t∈X‾ XR(B). Write R=XR(B).

[F1]

X consists of Rudin points eventually equal to the terms of a strictly increasing eventual scale; admissible finite modifications preserve membership (Kojman-Shelah scale subspace).

[F2]

If 1≤m≤k and ℵm many points of X are strictly increasing at all coordinates n>k, their pointwise tail supremum agrees there with a point of X (Tail suprema land in the scale subspace).

[F3]

The boxes (a,t]R, a<t, give the local base at t, and R is a P-space (Clopen boxes and the P-space property).

[F6]

Specified set-valued rules admit transfinite recursion (Transfinite recursion).

[A1]

AC is assumed for cofinal enumerations and for fixing a choice from each nonempty intersection used in the recursion (The Axiom of Choice).

Proof

1.1F1F3

For any z,w∈X, choose indices witnessing F1. If their indices are equal, z=∗w; if one index is smaller, scale strictness and the two finite exceptional sets give the corresponding strict eventual inequality. Thus exactly one of z<∗w, w<∗z, or z=∗w holds, since B is infinite. Fix z∈X with z≤t, and let E(z,t)={n:z(n)=t(n)}. Set a(n)=0 on E(z,t) and a(n)=z(n) elsewhere. Point-coordinates of t are positive; outside E(z,t) we have z(n)<t(n). Hence a<t. By closure and F3 there is w∈X∩(a,t]R. If z<∗w, the equality coordinates of z,t must lie in the finite exception set, because at such a coordinate w(n)≤t(n)=z(n). Thus E(z,t) is finite. In the other two cases w≤∗z. But at every coordinate outside E(z,t), membership in the box gives w(n)>a(n)=z(n). Hence that complement is finite, so E(z,t) is cofinite.

2.1step 1.1F1F3

Put A={z∈X:z≤t}, and for each finite or cofinite E⊆B put AE={z∈A:E(z,t)=E}. Every local box at t meets X and contains only points at most t, so t∈A‾ R by F3. Step 1.1 partitions A into the AE. There are countably many possible E: finite subsets of B inject into the natural numbers by S↦∑n∈S2n (the largest differing exponent exceeds the sum of all smaller powers), and complementation identifies cofinite subsets with finite ones. If t avoided every AE‾ R, the countable intersection of their open complements would be an open neighborhood of t by F3 and would miss A, contradicting t∈A‾. Choose an E with t∈AE‾. If E is cofinite, AE is nonempty; take a member z. Then t=∗z, and t∈R makes this an admissible finite modification, so t∈X by F1. It remains to consider finite E.

3.1step 2.1F4F5F6A1

Since t∈R, some finite q bounds all its coordinate cofinalities strictly below ℵq and above ω. By F4 the possible cofinalities are among ℵ1,…,ℵq−1. Put Di={n∈B:cf⁡(t(n))=ℵi}. At least one Di is infinite, since these finitely many sets cover the infinite B. Let m≥1 be the least such index. The union of the Di for i<m is finite. Choose a natural number k≥m at least all members of this union and of the finite E; if the union is empty, use k=m. Consequently every tail coordinate n>k has cofinality at least κ=ℵm, and no such coordinate is in E. On the infinite set Dm∩(k,ω) choose increasing cofinal functions γn:κ⟶t(n). F4 and A1 supply them: enumerate a size-κ cofinal subset and recursively take increasing bounds, with every proper initial segment bounded because its size is less than the cofinality.

4.1step 2.1step 3.1F3F4F6A1

Construct zξ∈AE for ξ<κ as follows. At stage ξ, for n>k put rξ(n)=sup⁡η<ξzη(n), with empty supremum zero. Every previous value is below t(n), because its equality set is E and n∉E. Since ∣ξ∣<κ≤cf⁡(t(n)), F4 gives rξ(n)<t(n). Define a lower function aξ<t by setting it to zero on n≤k, to max⁡(rξ(n),γn(ξ)) on Dm∩(k,ω), and to rξ(n) on other tail coordinates. All these inequalities are strict by step 3.1. As t∈AE‾, the open box (aξ,t]R meets AE by F3. Fix by A1 a choice function for all such nonempty box intersections, a set-indexed family, before applying F6 to the displayed rule. The chosen zξ then satisfies zξ≤t, and at every n>k it is strictly above all earlier values and strictly below t(n). Also zξ(n)>γn(ξ) on Dm∩(k,ω). These verifications inductively justify every stage of the recursion.

5.1step 1.1step 3.1step 4.1F1F2

Apply F2 to the sequence of step 4.1 with this 1≤m≤k. It gives h∈X agreeing with g(n)=sup⁡ξ<κzξ(n) on the tail n>k. Replace h(n) by t(n) on the finite prefix n≤k, obtaining h′. It is still a Rudin point: use a finite aleph bound larger than the two uniform bounds for h and t. Hence F1 gives h′∈X. On the tail g(n)≤t(n), since every term is at most t(n); on the prefix equality holds by construction, so h′≤t. Moreover g(n)=t(n) for every n∈Dm∩(k,ω), since the sequence dominates the cofinal γn there and is bounded by t(n). This infinite set is contained in E(h′,t). Step 1.1 therefore forces E(h′,t) to be cofinite. Thus t=∗h′, and t∈R implies t∈X by F1.

6.1step 2.1step 5.1

Every point of X‾ R belongs to X, by the cofinite case of step 2.1 or the finite case of step 5.1. Therefore X is closed in R. 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