Prove
Lemma 31 ([Small coordinate stabilizers]). There is an absolute constant c_0>0…Lemma 30 ([Coordinate normal tests]). Let z_i/F_j≤U<z_j/F_j be an actual…Proposition
Every ascending same-characteristic geometric step preserves both natural dimension and n q up to fixed positive lower factors, as established in. The same holds for a same-characteristic nonlinear step by its quadratic degree bound and fixed positive field ratio. If the last cover crosses, a preceding same-characteristic cover leaves n' q' at least a fixed multiple of n_i q_i . A preceding crossing has the same consequence from n'≥(c n_i q_i) and q'≥2 at sufficiently large rank. The last crossing then gives the endpoint lower bound. If only the first cover crosses, it gives n'≥(c n_i q_i) , and the last cover preserves natural dimension up to a fixed factor. Decreasing c and increasing the fixed minimum-rank threshold, we obtain in every case n_ i+1 ≥(c n_i q_i). Write u=n_i q_i . Classical order formulas give a_i≤C_1 n_i^2 q_i≤C_2u^2. After the first step every additional comparison gives at least the map x↦F(x)=(c(2)x) . For fixed C_3 , (F((cu)))/((C_3u^2))⟶∞ (u⟶∞). If L(u)/R(u)⟶∞ and R(u)⟶∞ , then F(L(u))/(R(u))⟶∞ as well. Induction therefore shows that h+2 comparisons dominate E_h((C_3u^2)) , and hence E_h(a_i^C) when C_3≥CC_2 . This also proves the last assertion. The target prime characteristic need not be bounded in this argument: its only use in the iteration was q≥2 .