LemmaStatement: 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.

Names for pairs, functions and ordinals

Statement

In ZF, for a set T of P-names put $S (T) = T \times P$ . For nonempty $G \subseteq P$ its value is ${τ_{G} : τ \in T}$ , where $τ_{G} = {val}_{G} (τ)$ . Define

$pairName (σ, τ) = S ({S ({σ}), S ({σ, τ})}) .$

Its value is the Kuratowski pair $⟨ σ_{G}, τ_{G} ⟩$ . If $i \mapsto τ_{i}$ is a set function of names on I, then $S ({pairName (\overset{ˇ}{i}, τ_{i}) : i \in I})$ is a graph name whose value is the function $i \mapsto (τ_{i})_{G}$ on I. If the family and P belong to a transitive ZF model M, these constructed names belong to M. For every ground ordinal alpha, $(\overset{ˇ}{α})_{G} = α$ .

Facts & Assumptions

Given: ZF; G nonempty and a set-indexed family of names. Explicit S and nested singleton calculations produce ordered pairs and function graphs, with internal construction and check-ordinal identities verified.

[F1]

Check-name evaluation and reconstruction of G: Check names evaluate to their ground sets for nonempty G and belong to a ground model containing their parameters.

[F2]

Forcing names and their rank: A set of pairs whose first coordinates are names is a name after bounding their name stages; every descendant of a name is a name.

[F3]

Valuation of names and M[G]: Valuation selects exactly the values of subnames having a coefficient in G.

[F4]

Check names without a largest condition: Check names are defined recursively from all conditions, with no largest condition required.

Proof

1.1

A set T of names has a common stage bound by F2, so S(T) is a name. By F3, each tau in T occurs in its valuation with every condition, and G nonempty therefore gives exactly $S (T)_{G} = {τ_{G} : τ \in T}$ . Apply this three times: the two inner values are ${σ_{G}}$ and ${σ_{G}, τ_{G}}$ , and the outer value is their unordered pair, precisely the Kuratowski ordered pair.

F2F3given

2.1

Replacement on I makes the set of pair names in the statement. Step 1.1 and F1 give its S-value as ${⟨ i, (τ_{i})_{G} ⟩ : i \in I}$ . Each index i has exactly one family value, so this is the graph of the claimed function even when different indices have equal values. Internal Pairing, product and Replacement perform these same finite constructions in M; F2–F4 and transitivity identify their outputs. Finally F1 applied to the set alpha gives the ordinal check identity, with no ordinal-preservation assertion about arbitrary names.

F1F2F3F4step 1.1∎

Depends on

Used by

Cohen-name valuation and dense-set meeting Example

Dependency tree · two levels

7 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

Karagila Definition 2.3 p6 and Exercises 2.6–2.7; explicit graph verification (standard reference, not scraped)