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.

Higher Cohen forcing violates GCH at a regular cardinal

Statement

In ZFC, let $κ$ be infinite regular and $λ > κ$ satisfy $2^{< κ} = κ$ and $λ^{κ} = λ$ . Then $Add (κ, λ)$ preserves all cardinals, adds $λ$ distinct subsets of $κ$ , and forces $2^{κ} = λ$ . Consequently, if $λ \geq κ^{+ +}$ , GCH fails at $κ$ . Over ground-model GCH, $κ = ℵ_{1}$ and $λ = ℵ_{3}$ give a cardinal-preserving extension with CH and $2^{ℵ_{1}} = ℵ_{3}$ .

Facts & Assumptions

Given: AC and the stated cardinal arithmetic.

[F1]

Closure and chain conditions of Cohen forcing gives $κ$ -closure and $κ^{+}$ -cc.

[F2]

Closure, distributivity, and absence of new short sequences and Chain conditions preserve high cofinalities and ccc preserves cardinals divide cardinal preservation at $κ$ .

[F3]

Nice-name reduction and the ccc counting bound supplies the maximal-antichain name-count method.

[F4]

Cardinal sum $κ \oplus λ$ , product $κ \otimes λ$ and exponentiation $κ^{λ}$ , and why they are written apart from the ordinal operations supplies exponent laws.

Proof

1.1

F1, F2 preserve cardinals at most $κ$ by closure and at least $κ^{+}$ by the chain condition, hence all cardinals. The coordinate-domain and bit-separation dense sets from the Cohen calculation give $λ$ distinct subsets of $κ$ , so $2^{κ} \geq λ$ .

F1F2

1.2

Replace the countable antichains in the nice-name proof by antichains of size at most $κ$ . A nice name for a subset of $κ$ is coded by $κ$ many subsets of $P$ of size at most $κ$ . Since $∣ P ∣ = λ$ and $λ^{κ} = λ$ , there are at most $(λ^{κ})^{κ} = λ$ such names. Thus $2^{κ} \leq λ$ , proving equality.

F3F4

2.1

If $λ \geq κ^{+ +}$ , equality gives $2^{κ} > κ^{+}$ , so GCH fails. Under GCH with $κ = ℵ_{1}$ and $λ = ℵ_{3}$ , the hypotheses hold; $κ$ -closure adds no reals, so CH remains true, while step 1.2 gives $2^{ℵ_{1}} = ℵ_{3}$ .

F1F2step 1.2∎

Depends on

Used by

Easton-support orientation for many regular cardinals Remark

Dependency tree · two levels

32 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

Karagila, Forcing & Symmetric Extensions, higher Cohen forcing (standard reference, not scraped)