Prove
Proposition 17 ([Integral evaluation through the outer limit]). Let C_j be any…Lemma 18 ([Irreducibility on the characteristic-zero tests]). On an inner or…Proposition
At one Artin stage, a coordinate of a cochain in the image of a finite model is a locally constant function. The finitely many coordinates being used factor through one finite quotient of the absolute Galois group. Enlarge it to contain the Tate action at the required precision, the finitely many ring-class fields and quadratic characters currently in use, and all old finite data. Chebotarev realizes the conjugacy class of τu on this finite quotient, with a chosen place realizing the desired representative. It gives a rational prime inert in K , outside the old finite set. Because u is exactly Tate-trivial, its Frobenius tends to ρ_T(τ) ; in particular a_ℓ→0 and ℓ→-1 . Because u is exactly ring-class trivial, the square Frobenius on the K -prime is the identity on every retained ring-class field. The unramified local coordinate is therefore the stated Frobenius-square evaluation. Repeat at each finite stage with increasing precision. All conditions remain finite, and no density bound or prime-size bound is required. For an outer sequence do this separately for each inner sequence, retaining the relevant finite evaluation matrices and degree-two identities before taking the outer quotient. Approximate inner cycles cause no problem, by the integrality calculation in Proposition 17 ([Integral evaluation through the outer limit]). Previously imposed finite diagrams are unchanged.