CorollaryStatement: AI-adaptedProof: 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 Suslin tree yields nonproductive ccc

Statement

In ZFC, if a Suslin tree exists, then there is a ccc poset $P$ whose coordinatewise square $P \times P$ is not ccc.

Facts & Assumptions

Given: A Suslin tree $T$ and AC.

[F1]

Every Suslin tree yields a normal splitting Suslin tree. Every Suslin tree has a normal splitting refinement

[F2]

The reverse-order poset of a normal splitting Suslin tree is ccc, but its coordinatewise square is not ccc. A ccc tree poset whose square is not ccc

[A1]

AC is available and its use by both constructions is propagated. The Axiom of Choice

Proof

1.1

Apply F1 to $T$ and call the resulting normal splitting Suslin tree $S$ . The normalization retains height $ω_{1}$ and the Suslin prohibitions, so its output is not an empty or singleton degeneration.

F1A1given

2.1

Let $P$ be $S$ with the reverse tree order. By F2, $P$ is ccc and the explicitly coordinatewise product $P \times P$ has an uncountable antichain, so it is not ccc. Thus this $P$ witnesses the assertion. No new choice is made here beyond the choices already declared by the cited suppliers.

F2A1step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

Monk, Set theory following Jech, Proposition 9.34, printed pp. 86-87 (sibling-selection argument); product deduction supplied by the cited local theorem (standard reference, not scraped)