Pardon me if I repeat someone. Q causes the answer of the calculator, so if we set calculator's answer counterfactually we lose dependency between Q and the calculator, and so we don't have any knowledge of the counterfactual Q. Whereas if we had a formula R of comparable logical complexity to Q, drawn from a class of formula pairs with 90% correlation of values, then the dependency is bidirectional and counterfactually setting R we gain the knowledge about the counterfactual Q. Does "in the counterfactual you trust an old calculator instead of your proof" mean that you don't agree (with this analysis)? (I have the impression that the problem statement drifted somewhat from "counterfactual" to a more "conditional" interpretation where we don't sever any dependencies.)