IrrCert implies |b*c-a|>b*2^-n>0 using IR026. This is a semantic explanation backed by rational-sequence inequalities, not a kernel real-number predicate.
Method: native-order. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.