Lemma 14 ([Tame division from character tests]). In a DVR-integer bounded power-series ring in t, u , a divisor L with nonzero reduction at uniformizer =t=0 becomes distinguished up to a unit in one tame variable after a tame group-power …

Specialize a line 1+u_j=(1+x)^ n_j , one n_j=1 and others successively very highly 2-divisible to separate a lexicographically leading monomial on reduction (assign the dominant lex coordinates largest 2^ v_2(n_j) in its weighted order, large relative to the lower-coordinate orders of the chosen monomial). This works simultaneously for a finite list by using the product. The line extends to a coordinate change. To retain the indicated characteristic-zero generic ranks and nonvanishings at t=0 , in formal log coordinates use leading homogeneous polynomials, choosing the free integers n_j avoiding finitely many proper conditions compatibly with the prescribed valuations. The same regularity test applies over a finite local coefficient order by its closed-point reduction. If a bounded B is divisible by L after inverting 2 at every sufficiently high 2 -power character in t , then Weierstrass division in that tame variable proves L B integrally. At those specializations the divisor remains regular of the same degree (evaluation always means the parameter is generator value minus one); the monic polynomial quotient has no 2-torsion, so the integral remainder vanishes there. Its bounded coefficients vanish identically by one-variable Weierstrass. One may check vanishing componentwise where the coefficient order embeds in a product of DVRs preserving the residual regularity. In general bounded nonzero series conditions in several variables can be avoided by finite-order tests by iterating the one-variable assertion (also with remaining unspecialized variables). For a nonzero bounded one-variable series the valuation at high 2-power characters is eventually the minimum coefficient valuation plus the first degree attaining it times the valuation of the parameter, by unique dominance.