Theorem 9.1 ([Eventual equality for every CPT sentence]). For every sentence ψ of full CPT with counting over τ , there is L_ψ such that for every L≥L_ψ , A_b⁰ ψ A_b¹ ψ.

Fix ψ first. Choose the integer q from Lemma 26 ([Polynomial invariant evaluation family]) and the width m from Lemma 27 ([Bounded-width description of a CPT evaluation]). For each L , put s=2L(q_3N+1)^2+1, M= L^ 7/4 . For i∈0,1 , let D_ L,i ^ (s) consist of the objects of (A_ b^i ) such that the object and each recursive member have a K -support of length at most s . Give this domain membership, the atom predicate, and the original input relations, false whenever any argument is not an atom. The family T_ψ(A_ b^i ) is H -invariant, membership-transitive and of size at most N^q , for large L . Corollary 15 therefore gives T_ψ(A_ b^i )⊆D_ L,i ^ (s) . The domain is membership-transitive and contains all atoms and pure HF sets: an atom supports itself, and a pure set is fixed by every atom permutation. Thus it satisfies all the domain requirements of Lemma 27 ([Bounded-width description of a CPT evaluation]). For the fixed q,m , Corollary 21 ([Widths at the support scale]) supplies all the quantitative hypotheses of Theorem 8.1 ([Transfer through small supports]) on sufficiently large grids: the two analytical expansions are C^M -equivalent, equal C^M types of tuples of length at most 2,ms determine K -orbits, and 4,m+1s≤M . These are nonempty finite structures in the same binary vocabulary, and K acts by automorphisms of both expansions. The supported domains computed from the expansions have the same underlying sets D_ L,i ^ (s) , since supports depend on the atom action of K , which did not change. The theorem gives C^m equivalence with the additional analytical relations; forgetting those relations gives D_ L,0 ^ (s) ≡_ C^m D_ L,1 ^ (s) . The larger group H was used only on the original input and its evaluation family. No assertion that H preserves the analytical expansion is needed. Both inputs have size N , so the same formula ψ_N , with the same numerical cutoffs and ordinal predicates, describes their evaluations. Lemma 27 ([Bounded-width description of a CPT evaluation]) and the displayed C^m equivalence therefore give equal truth values for ψ on the two inputs. All inequalities hold eventually in L after fixing ψ,q,m , which proves the quantified assertion.