Fixed finite-fragment verification for the Jech–Sochor socks transfer

Write the atoms as $a_{n,i}$ for $n\in \omega$ and $i<2$. The group swaps members within each pair $P_n=\{a_{n,0},a_{n,1}\}$; its normal filter is generated by finite pointwise supports. F1 makes $(P_n{)}_{n\in \omega }$ symmetric. If a choice graph had finite support, swapping a pair disjoint from that support would fix the graph and its input while moving its selected value, a contradiction.

Fix an ordinal power-iterate height $\alpha$ large enough to contain $\omega$, the pair sequence and its graph, every possible choice graph from $\omega$ to ${\bigcup }_n{P}_n$, and every intermediate singleton, unordered pair and Kuratowski ordered-pair code used to express $T$; $\alpha =\omega +\omega$ is more than enough for these fixed finite-rank coding operations. No finite iterate suffices, because the von Neumann naturals have unbounded finite rank. A graph is a subset of $\omega \times {\bigcup }_n{P}_n$, so this one ordinal height bounds every hypothetical witness. The pure parameter $\omega$ is fixed by the embedding. Encode the ZFA ambient source with distinct atom tags and set tags; F5's atom/set distinction prevents an atom from being identified with the empty set. The tagged interpretation uses ambient AC to well-order the atom set and make the pure coordinate copy required by F2.

Apply F2 at height $\alpha$ in a pure-forcing generic outer universe. Its set $A^{\ast }$ and symmetric ZF model $W$ carry the relevant power iterates, including the pair sequence and all possible choice graphs. For each fixed formula in $\mathrm{\Delta }$, the formal proof of the HS-model axioms uses finitely many ambient Separation and Replacement instances. In the unbounded Separation case, the proof first establishes almost universality, closes under the eight Gödel operations, and then proceeds by formula complexity; an existential step collects all least-rank witnesses before projecting. Replacement bounds the ambient functional image and cuts it by the resulting internal Separation certificate. Direct subname cuts are used only for bounded formulas. Thus the instances actually needed for $\mathrm{\Delta }$ have a finite ambient axiom support.

Use the carried pair-sequence parameter and the pure parameter $\omega$ to express the typed assertion $\theta$ that this particular sequence has no choice graph. The recursive translation in F2 fixes pure sets, so it fixes each finite ordinal and $\omega$; the chosen ordinal height contains them. Every candidate graph for this sequence lies in a named carried sort by step 1.2. Singleton and unordered-pair codes, hence Kuratowski ordered-pair codes, are preserved because their intermediate sets lie in the carried hierarchy and their membership relations are preserved. Atomic equality and membership, including those involving the fixed parameters, are preserved, and the base atom sort is opaque. F3's typed-formula induction therefore transports $\theta$ from step 1.1 to $W$. This yields the existential ZF sentence $T$ because the copied sequence is a witness. It does not assert the false converse that any witness to $T$ in either universe must be this particular sequence.

For the fixed $\mathrm{\Delta }$, collect the finitely many ZFA source instances, pure-forcing and HS-model instances, and transfer formulas used in steps 1.1–2.1. F4 gives a countable transitive model of a sufficiently large fixed finite ZFC source fragment; its constructible interpretation supplies the particular GCH instances required by the construction. The tagged construction inside it supplies the finite ZFA+AC ambient source. The set forcing and symmetric submodel construction are formalizable from those selected instances, and yield in the ambient theory a set model of every member of $\mathrm{\Delta }$. Enlarging the source fragment finitely absorbs the proof's exact reflection, genericity, name-rank and soundness instances. This selection is external and may depend on $\mathrm{\Delta }$; it asserts neither a single PA-total selector nor a full-ZFC countable transitive model.