For every v, construct z with z²<=v<(z+1)² by a bounded binary-search or existing division trace; establish uniqueness of z.
Method: native-induction. Induction: search interval length. Risk: reuse-audit.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.