TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)

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.

Separation in the constructible universe

Statement

In ZF, for each fixed membership formula $ϕ (x, p)$ and $a, p_{1}, \dots, p_{n} \in L$ , the set ${x \in a : ϕ^{L} (x, p)}$ belongs to $L$ . Thus every instance of Separation holds in $L$ .

Facts & Assumptions

Given: ZF; fixed formula, constructible set and finitely many constructible parameters. Reflection on a parameter-containing level makes the desired subset an actual Def subset.

[F1]

Finite reflection along constructible levels: Above any bound a transitive level reflects the fixed formula for all its parameter tuples.

[F2]

Definable subsets of a membership structure: Every subset defined over a nonempty set level with its parameters belongs to Def of that level.

Proof

1.1

Choose an ordinal bound large enough that one level contains $a$ and every $p_{i}$ . Reflect $ϕ$ above this bound, obtaining a nonempty transitive $L_{β}$ containing those parameters. For every $x \in a$ , transitivity puts $x$ in $L_{β}$ , so $ϕ^{L} (x, p)$ agrees with satisfaction of $ϕ (x, p)$ in $L_{β}$ .

F1given

2.1

Over $L_{β}$ the formula $x \in a \land ϕ (x, p)$ defines exactly the desired subset: the first conjunct uses actual membership and the second agrees by step 1.1. F2 puts this subset in $Def (L_{β}) = L_{β + 1} \subseteq L$ . An empty a or a formula with no satisfying elements gives the empty subset by the same definition. The argument uses only this fixed formula and ambient ZF.

F2step 1.1∎

Depends on

Used by

Absoluteness, idempotence and minimality of L Theorem
Internal Power Set in L Theorem
Replacement in L Theorem
Semantic and formal inner-model theorem for L Theorem
The canonical definable global well-order of L Theorem
The constructible universe satisfies AC Theorem

Dependency tree · two levels

5 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 Theorem 5.7 p15; Marks Lemma 20.5 p87 (standard reference, not scraped)