No, actually any proof that supplies a bound must also have some least bound that can be derived from that proof. It could be a calculation that starts from the

No, actually any proof that supplies a bound must also have some least bound that can be derived from that proof. It could be a calculation that starts from the bound, or it could be some calculation with a result that tells you what the bound is. To me it seems very unlikely that the actual bound was exactly 70000000 in either case. It _could_ be that some super-expensive calculation is required for each candidate bound, and Zhang guessed 70000000 as a starting point and did the calculation for that number, which succeeded, but he didn't bother repeating it for any smaller numbers because it would cost him too much. But if that was the case, that would be interesting in itself.