For an M by N integer matrix bounded by A>=1 and x in {0,...,2NA}^N, each image coordinate lies in [-2N²A²,2N²A²].
Method: native-induction. Induction: dot-product length. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.