An explicit map from a finite box with cardinality strictly exceeding a finite target box has two distinct inputs with the same output.
Method: native-induction. Induction: finite target cardinality. Risk: reuse-audit.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.