For k>=1 and z²<=2*2^(2k)<(z+1)², 1<=z/2^k and the interval [z/2^k,(z+1)/2^k] has width 2^-k; enclosures are compatible across precisions.
Method: native-order. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.