Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

A specialization generic kills a tree

Statement

Let M be a transitive model of ZFC, let T∈M be a Suslin tree there, and let G be an M-generic filter on its finite-specialization forcing P(T), when such a filter is supplied externally. For

Dt={p∈P(T):t∈dom⁡(p)},f=⋃G,

every Dt is dense, f:T→ω is total and separates comparable nodes, and

T=⋃n<ωAn,An=f−1({n}),

where every An is an antichain and at least one An is uncountable. Thus the unchanged ground tree is special and not Suslin in M[G].

Facts & Assumptions

Given: M,T,P(T),G as in the Statement. AC holds in M and in M[G].

[F1]

Finite-specialization forcing of the ground Suslin tree is ccc, preserves all ground cardinals and cofinalities, and internally forces the ground tree to be special and non-Suslin. Specializing forcing kills a Suslin tree

[F2]

Its conditions are finite natural-valued maps that give unequal labels to distinct comparable nodes; stronger conditions extend graphs and the empty function is greatest. Finite specializing conditions

[F3]

Each Dt is dense, and the union of a nonempty directed family meeting all Dt is a total specializing map. Dense domains and directed unions of specializing conditions

[F4]

A Suslin tree has height ω1 and countable levels, and a total map separating comparable nodes witnesses specialness. Aronszajn, Suslin and special trees

[F5]

Under countable choice, a countable union of countable sets is countable. Countable unions of at most countable sets, assuming ACω

[A1]

AC is available in the ground and is inherited by the supplied ZFC generic extension. The Axiom of Choice

Verification

1.1F2F3givenconstruct

Fix t∈T and p∈P(T). If t∈dom⁡(p), take q=p. Otherwise put N={0,ran⁡(p)=∅,1+max⁡ran⁡(p),ran⁡(p)≠∅,q=p∪{(t,N)}. The finite range has a maximum in the second case, and N differs from every old label. Therefore every new comparable pair involving t has unequal labels, while old pairs still satisfy [F2]. Thus q∈P(T), q≤p, and q∈Dt. This calculates the density of every domain requirement, including the empty-condition case where the added label is 0.

2.1F2F3step 1.1

Since G is a nonempty directed generic filter, it meets every ground dense set Dt. If (t,i),(t,j)∈⋃G, directedness gives a common stronger condition containing both pairs, so [F2] gives i=j. Hence f=⋃G is a function. Meeting Dt for each t makes its domain all of T. If s<Tt, choose conditions in G containing s and t and a common stronger condition; [F2] gives f(s)≠f(t). This is the total specializing map promised by [F3].

3.1F4step 2.1

For each n<ω, define An=f−1({n}). If s,t∈An are distinct, then f(s)=f(t)=n, so step 2.1 says they cannot be comparable; hence An is an antichain. Totality gives T=⋃n<ωAn. The fiber A0 is included but may be empty, and no argument singles out a predetermined uncountable fiber.

4.1F1F4F5F6A1step 3.1

Suppose for contradiction that every An were countable in M[G]. Then [F5] would make T countable. The height map sends its nodes onto a cofinal subset of the preserved ω1M: [F1] preserves ω1, and the old tree still has a node at every countable height by [F4]. The image of a countable set is countable, contradicting [F6]. Thus some, but not necessarily the zero, fiber An is uncountable.

5.1F1F4F6step 2.1step 3.1step 4.1

By step 2.1, the restriction of f to any branch is injective into ω. A cofinal branch would therefore have a countable cofinal set of node heights in the preserved ω1, contrary to [F6]. Hence T remains Aronszajn. Step 3.1 witnesses that it is special, while step 4.1 supplies an actual uncountable antichain, so it is not Suslin. “Kills” refers only to the Suslin property: the tree set, order, height, and countable old levels remain.

6.1F1F2F5F6A1step 1.1step 2.1step 3.1step 4.1step 5.1∎

The calculation was made in a supplied generic extension only to display the objects. By [F1], its dense-set, directed-union, preservation and ZFC arguments are already encoded by the internal forcing relation below the greatest empty condition. No M-generic over the universe is asserted to exist. The empty function, singleton extensions, label zero, possibly empty fibers, and absence of a top level at the limit height ω1 create no exception. The density and union calculations in steps 1.1-3.1 are choice-free; AC is used through preservation and the countable-union and boundedness conclusions in steps 4.1-5.1.

Remarks

  • Preservation of ω1 alone does not identify an uncountable fiber. The countable-union theorem and the cofinal height map supply the required contradiction.
  • A total natural-valued specialization cannot create a cofinal branch: its restriction to such a branch would inject a cofinal height set into ω.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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