You're welcome for the answer.
Option 1 means this: for all n > 0, charge(n) is possible/defined, so we should certainly check the values 0, 1 (penny), something typical like 1495, and then the maximum integer value.
Option 2 means this: for all n such that charge(n) is possible, n > 0. In this case, charge(1) might not be possible, but certainly charge(0) and charge(-1) are not possible. The minimum threshold of, for example, 1000 fits Option 2 and we would check in the contract that charge(999) is rejected.
Option 1 is exactly Option 2 with a threshold of 0.
It feels natural to to me to use both examples and property-based testing to check both options. I think this becomes a question of style/preference.
The big difference lies in interpretation: is the threshold of 1000 part of the essential contract or an implementation detail? In your case, I infer that it is part of the essential contract, in which case I expect three kinds of responses from charge(): (1) OK, (2) Rejected because the amount lies below the threshold, (3) Failed, and here is the reason/cause.
Maybe in other situations, the threshold is just an implementation detail. Maybe negative charges are allowed and treated as refunds, if they happen, but they are not required. Maybe this particular payment gateway vendor doesn't yet support refunds, and so their implementation conforms to the contract (no charge amount is rejected), even though sometimes payments fail (and negative amount is just another reason to fail, alongside disk full and network timeout). The contract can say, for example, "charge(n) is undefined for n <= 0", which means, "do whatever you want when n <= 0". This might be OK and this might be dangerous, depending on the situation.
And yes, it might be a violation of ISP to force clients to know details that they don't need to know. That's not always bad, but it's always worth reconsidering.