For each positive rational eta and natural A, construct t with (A+1)*2^(-t)<eta by an explicit natural bound; prove power monotonicity.
Method: native-induction. Induction: natural exponent. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.