CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

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.

V equals L gives a Suslin tree

Statement

ZF proves that $V = L$ implies the existence of a normal splitting Suslin tree on $ω_{1}$ .

Facts & Assumptions

Given: Ambient ZF and the hypothesis $V = L$ .

[F1]

V equals L implies diamond derives a diamond sequence on $ω_{1}$ from $V = L$ in ZF.

[F2]

The constructible universe satisfies AC says that $L$ satisfies AC; under $V = L$ this is ambient AC.

[F3]

Diamond constructs a normal splitting Suslin tree proves in ZFC that diamond constructs a normal splitting Suslin tree with underlying set $ω_{1}$ .

[A1]

The Axiom of Choice names the hypothesis explicitly required by F3 and supplied here by F2.

Proof

1.1

By F1, $V = L$ supplies a diamond sequence on $ω_{1}$ . By F2 and the equality $V = L$ , A1 holds in the ambient universe. This explicit use of Choice is essential to the cited tree proof: it supplies its countable-union, maximal-antichain, and deterministic well-ordering steps.

F1F2A1given

2.1

Apply F3 with the diamond sequence and AC from step 1.1. The resulting tree is normal and splitting, has underlying set $ω_{1}$ , has countable levels, and has neither an uncountable antichain nor a cofinal branch; hence it is a Suslin tree. No tree is asserted at the degenerate heights zero or one, and no weakening from stationary guessing to merely unbounded guessing is made.

F3step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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

Lietz, Set Theory, Theorem 7.20, pp.60–61; published diamond-to-Suslin construction (standard reference, not scraped)