If the fixed c sequence equals a/b at every accuracy, IR061 identifies its jets with AuxJet; IR048/49/59/64 contradict one another. Conclude not(c=a/b) for b>0, without a Markov axiom.
Method: native-search. Induction: none. Risk: high.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.