Set epsilon=1/(4*K*S*J), all factors positive. A hypothetical |c-z|<=epsilon yields upper bound<=1/(2K), plus at most1/(4K) finite-evaluation error, contradicting the lower bound1/K. Establish the required rational implications, not a general real-order decision principle.
Method: native-order. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.