Strict Separation Impossibility

Abstract

Common outcome utilities and homogeneous report costs forbid opposite strict preferences.

Theorem 1.1 (Common utilities forbid opposite strict report preferences).

$\forall T h e t a, R, O : Type, t h e t a, t h e t a_{p r im e} : T h e t a, r_{t h e t a}, r_{t h e t a_{p r im e}} : R, M : R \to O, u : T h e t a \to O \to R e a l, c : R \to R e a l, \forall o : O, u (t h e t a, o) = u (t h e t a_{p r im e}, o) \Rightarrow \neg ((u (t h e t a, M (r_{t h e t a})) - c (r_{t h e t a}) > u (t h e t a, M (r_{t h e t a_{p r im e}})) - c (r_{t h e t a_{p r im e}})) \land (u (t h e t a_{p r im e}, M (r_{t h e t a_{p r im e}})) - c (r_{t h e t a_{p r im e}}) > u (t h e t a_{p r im e}, M (r_{t h e t a})) - c (r_{t h e t a}))) .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/StrictSeparationImpossibility.strict_separation_impossible (✓ std3). ∎

Source. Repository-derived.

Commentary.

A mechanism is represented by its result map from reports to outcomes. Both types evaluate every outcome with the same utility, and the report-cost function is independent of type.

The public conclusion rules out the conjunction in which the first type strictly prefers its report and the second type strictly prefers the other report. Transferring the first inequality across the common utility equality contradicts the second.

Repository and pinned-library searches found no exact mechanism theorem. The proof applies equality rewriting and the asymmetry of strict order.

References

Truth anchor: D5/S3/ConceptDynamics/StrictSeparationImpossibility.strict_separation_impossible

Keyboard shortcuts

trureturing Blueprint

Strict Separation Impossibility

Abstract

References