ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

Transporting an elementary-chain map through collapse

Example

For collapses $π_{α} : M_{α} \to {\overset{ˉ}{M}}_{α}$ of an elementary membership chain, the maps are $j_{α β} = π_{β} \circ ι_{α β} \circ π_{α}^{- 1}$ . Their action on an ordinal is an order-type embedding, and equality with inclusion is an additional condition. In ZFC the two-stage chain $X ≺ V_{κ + ω}$ constructed below gives an explicit failure of inclusion.

Facts & Assumptions

[F1]

Elementary chains and compatible collapses: A nonempty set-ordinal elementary chain of actual membership structures satisfying Extensionality has a union elementary over every stage, and the union has a transitive collapse. Conjugating the inclusions by stage and union collapses gives coherent elementary embeddings; these are not asserted to be inclusions of the transitive images.

[F2]

What the collapse fixes: Let $π : X \to \overset{ˉ}{X}$ be a collapse of actual membership as above. It fixes every transitive subset $A \subseteq X$ pointwise. If $α \in X$ is an actual ordinal, $π (α)$ is the order type of $X \cap α$ . In particular, if $X \cap α$ is transitive, $π (α) = X \cap α$ .

[F3]

Countable elementary submodels and their collapses: In ZFC, if an infinite set membership structure $M$ satisfies Extensionality, then for every at most countable $A \subseteq M$ there is a countably infinite $X ≺ M$ containing $A$ , and $X$ has a countable transitive collapse. To retain a set $a \in M$ as one parameter, use $A = {a}$ .

[F4]

Hartogs: an ordinal that does not inject into a given set: For every set $A$ there is an ordinal (def-ordinal) that does not inject into $A$ , that is, admits no injective function into $A$ . The least such ordinal is the Hartogs number $ℵ (A)$ , and it is exactly

$ℵ (A) = {o t (S, R) : S \subseteq A and R well-orders S},$

the set of order types (thm-mostowski-collapse) of the well-ordered subsets of $A$ .

The proof is choice free. That is the whole point of the theorem: in ZF alone, with no assumption that $A$ can be well ordered, one still gets an ordinal too long to be laid inside $A$ .

[F5]

The Axiom of Choice: The Axiom of Choice (AC) is the following statement.

Every family of nonempty sets has a choice function > (def-choice-function).

Written out: for every set $F$ all of whose members are nonempty, there exists a function $g$ with domain $F$ satisfying $g (S) \in S$ for all $S \in F$ .

An equivalent formulation is that a product of nonempty sets is nonempty: if $X_{i} \neq \emptyset$ for every $i \in I$ , then $\prod_{i \in I} X_{i} \neq \emptyset$ . Here $\prod_{i \in I} X_{i}$ is the set of functions $f$ with domain $I$ such that $f (i) \in X_{i}$ for every $i \in I$ ; when a family of nonempty sets is indexed by itself, such an $f$ is precisely a choice function for it.

Verification

Given: A chain and its actual collapse maps, with a named ordinal at an earlier stage; ambient ZFC for the concrete witness.

1.1F1F2given

For a named actual ordinal $ξ \in M_{α}$ , put $τ_{α} = ot (M_{α} \cap ξ)$ . F2 gives $π_{α} (ξ) = τ_{α}$ , so direct substitution in F1 yields $j_{α β} (τ_{α}) = π_{β} (ξ) = ot (M_{β} \cap ξ) = τ_{β}$ . On a predecessor $η \in M_{α} \cap ξ$ , its order position $ot (M_{α} \cap η)$ is sent to $ot (M_{β} \cap η)$ . These equalities specify the induced order embedding.

2.1step 1.1algebra

For three stages the calculation is $j_{β γ} (j_{α β} (u)) = π_{γ} (π_{β}^{- 1} (π_{β} (π_{α}^{- 1} (u)))) = π_{γ} (π_{α}^{- 1} (u)) = j_{α γ} (u)$ , with inclusions understood at the displayed domain changes. For two identical stages this computes the identity. If the named ordinal has $τ_{α} \neq τ_{β}$ , step 1.1 moves it, whereas literal inclusion would fix it. Thus inclusion requires additional agreement of collapse values and does not follow from the conjugation formula.

3.1F2F3F4F5step 1.1∎

Here is a chain for which the values differ. In ZFC let $κ = ℵ (ω)$ from F4, and put $θ = κ + ω$ . The transitive infinite set $V_{θ}$ contains $κ$ and satisfies Extensionality: all members of each of its elements remain in its domain, so internal agreement of members is actual agreement. F3, with the singleton parameter set ${κ}$ and the AC assumption F5, supplies a countable $X ≺ V_{θ}$ containing $κ$ . Take the two-stage chain $M_{0} = X$ , $M_{1} = V_{θ}$ . F2 makes $π_{1}$ the identity, and gives $τ = π_{0} (κ) = ot (X \cap κ)$ . This ordinal injects into $ω$ : compose the inverse order isomorphism with a countable enumeration inverse for X. F4 says $κ$ does not inject into $ω$ , so $τ \neq κ$ . Step 1.1 now calculates $j_{01} (τ) = κ \neq τ$ . This elementary transported map moves an element of its domain and therefore is not literal inclusion.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

Geschke, Models of Set Theory — §4 collapse interface pp11–12; published chain theorem (standard reference, not scraped)