ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09

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.

An explicit uncountable delta system

Example

For $α < ω_{1}$ , let $a_{α} = {0, α + 1}$ . This is an uncountable family of distinct two-element sets forming a delta system with root ${0}$ . The singleton family $b_{α} = {α}$ instead has empty root.

Facts & Assumptions

Given: Ordinals carry their usual membership order; $ω_{1}$ is the first uncountable ordinal.

[F1]

The delta-system condition is equality of every pairwise intersection at distinct indices with the specified root. Delta systems and roots

Verification

1.1

For each $α$ , $α + 1 \neq 0$ , so $a_{α}$ has two elements. Distinct ordinals have distinct successors: if $α < β$ , then $α + 1 \leq β < β + 1$ . Thus $a_{α} \cap a_{β} = {0}$ whenever $α \neq β$ . Also $a_{α} = a_{β}$ would identify their unique nonzero elements and force $α = β$ . Consequently the family has size $ω_{1}$ and is a delta system with root ${0}$ .

F1given

2.1

For $α \neq β$ , $b_{α} \cap b_{β} = \emptyset$ . The map $α \mapsto b_{α}$ is injective, so this is another $ω_{1}$ -sized delta system, with empty root. For instance $a_{0} \cap a_{1} = {0, 1} \cap {0, 2} = {0}$ whereas $b_{0} \cap b_{1} = {0} \cap {1} = \emptyset$ .

F1given∎

Depends on

Delta systems and roots

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

2 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 (2024), Theorem 9.20, printed pp77–78; explicit pairwise-intersection instance (standard reference, not scraped)