Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31
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.

Assuming countable choice, the deleted Tychonoff plank is a regular nonnormal open subspace of a compact Hausdorff normal space

Statement

Assume the Axiom of Countable Choice. Let P=(ω1+1)×(ω+1)P=(\omega_1+1)\times(\omega+1) with the product of its ordinal order topologies, let p=(ω1,ω)p=(\omega_1,\omega), and let T=P{p}T=P\setminus\{p\}. Then PP is compact, Hausdorff, and normal, while TT is an open regular subspace that is not normal.

Facts & Assumptions

Given: The Axiom of Countable Choice and the ordinal product PP above.

[F2]

The ordinal order-topology basis gives neighbourhoods (α,ω1](\alpha,\omega_1] of ω1\omega_1, singleton neighbourhoods {n}\{n\} of n<ωn<\omega, and neighbourhoods (m,ω](m,\omega] of ω\omega (The order topology on an ordinal, with the half-open intervals (α,β](\alpha, \beta] and the initial segments [0,β][0, \beta] as a basis, Every ordinal with its order topology has a basis of clopen sets, and is T1T_1, Hausdorff and regular).

Proof

technique · contradiction
1.1

The factors ω1+1\omega_1+1 and ω+1\omega+1 are compact and T3T_3 by [L1], so [L2] makes PP compact, Hausdorff, regular, and normal.

L1L2
1.2

Since PP is T1T_1, {p}\{p\} is closed; hence TT is open. Its regularity follows from the hereditary regularity conclusion in [L2].

L2
1.3

Put E={ω1}×ωE=\{\omega_1\}\times\omega and F=ω1×{ω}F=\omega_1\times\{\omega\}, regarded as subsets of TT. The clopen ordinal basis shows that they are disjoint closed subsets of TT.

F2
2.1

Suppose, for a contradiction, that TT is normal. Choose disjoint open U,VTU,V\subseteq T with EUE\subseteq U and FVF\subseteq V.

F1step 1.3assume-contra
3.1

For n<ωn<\omega, let Cn={ξ<ω1:(ξ,ω1]×{n}U}C_n=\{\xi<\omega_1:(\xi,\omega_1]\times\{n\}\subseteq U\}. By [F2] each CnC_n is nonempty; [A1] chooses αnCn\alpha_n\in C_n simultaneously. The countable set {αn:n<ω}\{\alpha_n:n<\omega\} is bounded by some α<ω1\alpha<\omega_1.

A1F2step 2.1
3.2

Put β=α+1<ω1\beta=\alpha+1<\omega_1. Since (β,ω)V(\beta,\omega)\in V, [F2] gives γ<β\gamma<\beta and m<ωm<\omega with (γ,β]×(m,ω]V(\gamma,\beta]\times(m,\omega]\subseteq V.

F2step 2.1
4.1

The point (β,m+1)(\beta,m+1) lies in VV by step 3.2 and in UU by step 3.1, because β>ααm+1\beta>\alpha\ge\alpha_{m+1}. This contradicts UV=U\cap V=\varnothing, so TT is not normal; together with steps 1.1 and 1.2 this proves all the stated properties.

step 1.1step 1.2step 3.1step 3.2discharge-contradiction

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 144 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources