Strategic Response Obstruction

Abstract

A fixed-point-free strategic response prevents any predictor from being correct at every state.

Theorem 1.1 (Strategic response precludes a universal predictor).

$$(\forall y,tau(y)\ne y)\wedge (\forall f,\exists x,R(f,x)=tau(f(x)))\Rightarrow \neg \exists f,\forall x,R(f,x)=f(x).$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/Feedback/StrategicResponseObstruction.strategic_response_precludes_universal_predictor (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix a proposed predictor and choose the response state supplied by the strategic hypothesis. Universal correctness identifies the response with the prediction there, while strategic response identifies it with the twisted prediction. Their equality makes that prediction a fixed point of the twist, contradicting the fixed-point-free hypothesis.

Pinned Mathlib, Loogle, and D5 were searched before proving. Mathlib’s Function.IsFixedPt supplies the standard fixed-point predicate, but no library theorem has this predictor-dependent response hypothesis and universal-correctness conclusion.

References

• Truth anchor: D5/S0/Diagonal/Feedback/StrategicResponseObstruction.strategic_response_precludes_universal_predictor