Atomic forcing is well-founded and definable

For input names $\sigma ,\tau$ form a set C by starting with those names, adjoining all first coordinates of their entries, iterating this operation through omega, and taking the union. Replacement and Union give a set closed under subnames. On $C\times C$ order pairs by the lexicographic order of $(\max ({\mathrm{rk}}_P(u),{\mathrm{rk}}_P(v)),\min ({\mathrm{rk}}_P(u),{\mathrm{rk}}_P(v)))$. This relation is well-founded: in a nonempty subset take the least first rank, then the least second rank. It is setlike since the domain is a set. Lowering one coordinate strictly lowers its sorted rank pair; swapping coordinates leaves the complexity unchanged.

At $(u,v)$ define a subset $E(u,v)$ of P by the equality clause of F1 with both subset clauses expanded. Its only equality calls involve a subname of u and a subname of v, in either order; these have strictly smaller complexity. Thus a supplied predecessor function determines membership of every p in $E(u,v)$ by quantifiers over sets P, u and v. Separation forms the unique subset. F2 supplies all these subsets on $C\times C$. Then the subset and membership relations are uniquely specified by F1 using these E-values; no recursive call to the same equality pair is needed.

For any two descendant-closed cones containing an input pair, their intersection remains descendant-closed. Induction on sorted rank pairs shows the E-values agree there, since their defining clauses use identical smaller pairs. The derived subset and membership values agree as well. Accordingly the formula asserting that the canonical cone recursion has p in its designated value defines the atomic relation independently of the cone. Every putative solution restricts to this recursion, so uniqueness follows.

Inside transitive M the canonical cone formed in step 1.1 is the same set: first-coordinate extraction, each finite iteration, and its omega-union agree, and M has actual omega. F3 identifies its ranks. Induct on the common rank pairs. Every condition, coefficient and subname quantified over in the expanded equality clauses is in the identical set on both sides; all predecessor E-values agree by induction. Equality therefore agrees, and the derived subset and membership clauses agree for the same reason. All recursions and restricted forcing sets exist inside M by its ZF axioms. This proves atomic absoluteness without comparing power sets of name levels, using AC, or asserting that a class of all names is a set.