Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Cardinal exponentiation below the continuum under MA

Statement

In ZFC+MA, for every infinite κ<2ℵ0, 2κ=2ℵ0. Consequently the continuum is regular.

Proof

1.1F2

Fix X⊆κ. Let PX consist of pairs (s,F) with s a finite partial map ω→2 and F⊆κ∖X finite. Put (t,H)≤(s,F) iff s⊆t, F⊆H, and t−1(1)∩(dom⁡(t)∖dom⁡(s))is disjoint from⋃α∈FAα. This is transitive: an extension never puts a new 1 on any set already protected by the weaker condition. Conditions with the same stem s are compatible, since (s,F∪H) extends both. There are only countably many finite stems, so PX is σ-centered and hence ccc.

2.1F1F2step 1.1

For α∉X, let Eα={(s,F):α∈F}; this is dense because adjoining α to F changes no stem. For α∈X and n<ω, let Dα,n={(s,F):(∃m>n) [m∈Aα∩dom⁡(s) and s(m)=1]}. Given (s,F), the set Aα∩⋃β∈FAβ is finite by almost disjointness. Since Aα is infinite, choose m>n outside that finite set and dom⁡(s); setting s(m)=1 gives an extension in Dα,n. Thus all these sets are dense. Their number is at most κ⋅ℵ0=κ, so MA supplies a filter G meeting them. Let rX={m:(∃(s,F)∈G) s(m)=1}. Directedness makes the stems in G consistent. If α∈X, meeting every Dα,n makes rX∩Aα infinite. If α∉X, choose (s,F)∈G∩Eα. For any (t,H)∈G, take (u,K)∈G below both. Since (u,K)≤(s,F) and α∈F, no new 1 of u beyond s lies in Aα; hence t−1(1)∩Aα⊆s−1(1). Consequently rX∩Aα⊆s−1(1) is finite. Therefore X={α:∣rX∩Aα∣=ℵ0}.

3.1F3step 2.1∎

Choosing the least real in a fixed well-order among the codes for each X gives an injection P(κ)↪P(ω); AC is used here. Monotonicity gives c≤2κ, hence equality. If cf⁡(c)=λ<c, then c≤cλ=(2λ)λ=2λ=c, while König gives cλ>c, contradiction. Therefore c is regular.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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