Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-14
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.

Nice refinements exist and are regular but not Lindelof

Statement

Every ordered fundamental space has a nice refinement (ω1,T~) satisfying (α) for every ωα<ω1. The refinement is separable, locally compact, locally countable, zero-dimensional, regular, and Hausdorff, but it is not Lindelöf. Here locally countable means that every point has a countable neighbourhood.

Facts & Assumptions

Given: An ordered fundamental space (ω1,T) and ZFC.

[F1]

Ordered fundamental spaces and nice refinements gives the rings, intermediate topologies, model chain, metrics, nice-refinement clauses, the families Γα(S,ν), and (α).

[F2]

A compact topological space is one whose every open cover has a finite subcover, and a compact subset carries the intrinsic subspace topology (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F3]

A compact metric space is totally bounded: at every positive radius it has a finite net (A compact metric space is complete and totally bounded, and neither implication uses any choice principle).

[F4]

A space is locally compact when every point has a compact neighbourhood (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space).

[F6]
[F7]

Countable elementary submodels and their collapses supplies a countable elementary hull containing any prescribed countable parameter set.

[F8]

Transfinite recursion constructs the model chain and the later stage-by-stage refinement from their functional successor and limit clauses.

[F9]

The Axiom of Choice supplies the simultaneous recursive choices of hulls, metrics, finite nets, ring points, and compact clopen enlargements.

Proof

technique · transfinite and finite recursion
1.1

Construct the required continuous chain Mα:α<ω1 explicitly. Start with an F7 hull containing the ordered fundamental space and its base assignment. At a successor, apply F7 to the countable set Mα{Mα,α} and the fixed parameters; at a countable limit take the union of the earlier increasing elementary chain, which is countable and elementary by the Tarski--Vaught test. F8 performs this recursion, and F9 makes the simultaneous hull choices. Now choose the compatible metrics dα allowed by F1 and F9. For α<ω put Vnα={α}. Inductively suppose the Vnξ and Hξ have been constructed for every ξ<α, and that the resulting topology below α is locally compact and zero-dimensional.

F1F7F8F9givenbaseih
2.1

Fix ωα<ω1. The countable model Mα+1 contains only countably many sets S satisfying S0 and SK(α,T~α); list them as Sν:ν<ω, repeating every such S infinitely often. This collection is nonempty because it contains S=, and that particular S makes the later star implication vacuous.

F1F7F9step 1.1
3.1

Recursively suppose Hα is fixed for <ν and put Aν=<νHα. This is a finite union of compact sets, hence compact. Every KΓα(Sν,ν) lies in Aν(Wναα): the first ν ring intersections lie in their Hα, while all remaining points lie in the nested Wνα.

F1F2step 1.1step 2.1ih
4.1

The family Γα(Sν,ν) has a finite Hausdorff 2ν-net Pν chosen from itself. Indeed, by [F3] choose a finite ε-net of the compact metric set Aν, where 2ε<2ν. Partition the remaining tail into the outer ring Rν=(WναWν+1α)(α+1) and the deeper tail Tν=Wν+1α(α+1). Record for each K which finitely many ε-cells meet KAν, whether K meets Rν, and whether it meets Tν. There are finitely many records. Two compacta with the same record are within Hausdorff distance at most 2ν: match their points in Aν through a common recorded cell; points in Rν are within its internal diameter 2ν3; and points in Tν are within 2ν by the triangle inequality, since every such point has distance at most 2ν1 from α. The two tail-incidence bits ensure that each required matching part is nonempty. Choosing one member for each realized record gives Pν; if Γα(Sν,ν)=, take Pν=.

F1F3F9step 3.1
5.1

Let Qν be the union of J(WναWν+1α) over JμνPμ. It is a compact subset of the relatively clopen nonempty ν-th ring. Local compactness and the clopen base below α cover Qν by finitely many compact clopen sets lying in that ring; their union is compact clopen. If this union is empty, choose a ring point and one compact clopen neighbourhood of it in the ring. Call the resulting nonempty compact clopen set Hνα; it contains Qν.

F1F2F9step 1.1step 4.1
6.1

For JPν, membership in Γα(Sν,ν) already puts its intersections with rings <ν inside Hα. For ν, the stage- definition includes Pν in μPμ, so Hα absorbs the -th ring intersection of J. Hence PνΓα(Sν,ω).

F1step 4.1step 5.1
6.2

Put Vmα={α}mHα. Its maximum is α and its part below α is open. It is compact in the intermediate topology: an intermediate-open cover has a member containing α, hence contains some WNα(α+1) and all Hα for N; only finitely many earlier compact Hα remain. It is therefore intermediate-closed, and [F1] makes the Vmα a clopen local base in the final refinement. The same argument for a final-open cover, now using a contained VNα, proves that Vmα is compact in the final topology.

F1F2step 5.1
7.1

Whenever Sν=S, steps 4.1 and 6.1 give KΓα(S,ν) JΓα(S,ω) dα(K,J)2ν. Every relevant S occurs infinitely often, so (α) holds.

F1step 2.1step 4.1step 6.1
8.1

Steps 2.1--7.1 together with step 6.2 perform the successor construction at every countable α, while limit stages take the accumulated earlier data. Transfinite induction therefore produces a nice refinement satisfying every (α).

F1step 1.1step 2.1step 3.1step 4.1step 5.1step 6.1step 6.2step 7.1discharge-induction
9.1

Every Vmα is compact by step 6.2, so [F4] gives local compactness. It lies in α+1, a countable ordinal, so it is a countable neighbourhood and the space is locally countable. The base is clopen and Hausdorff by [F1], hence zero-dimensional and regular by [F6].

F1F4F6step 6.2step 8.1
9.2

The set ω remains dense. Inductively, every nonempty relatively open Hαα meets the already dense ω, so every basic tail Vmα meets ω; for α<ω the singleton Vmα itself lies in ω. Thus the refinement is separable.

F1step 5.1step 8.1
9.3

Every initial segment α is open: if ξ<α, then each basic neighbourhood Vmξ is contained in ξ+1α. Consequently U={α:0<α<ω1} is an open cover of ω1. A countable subfamily has countable supremum δ<ω1 and its union is contained in δ, so it misses δ. By [F5] the refined space is not Lindelöf.

F1F5step 6.2step 8.1
10.1

Combining steps 7.1 and 8.1--9.3 gives all asserted properties. The empty Γ cases were handled in steps 2.1 and 4.1, ν=0 has A0=, the finite ordinals use singleton bases, and F9 records every nonempty simultaneous choice.

F8F9step 2.1step 4.1step 7.1step 8.1step 9.1step 9.2step 9.3discharge-induction

Depends on

Used by

Dependency tree · two levels

53 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