proof

P18 Marginals ≠ tradeoffs

Lean spine source

Declarations: P18_marginal_preservation_not_tradeoff_preservation

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P18_marginal_preservation_not_tradeoff_preservation :
    ∃ p q : TradeoffProfile 2,
      sameMarginals p q ∧ ¬ sameTradeoffs p q :=
  ⟨tradeoffProfile0, tradeoffProfile1, same_marginals_profiles, different_tradeoff_profiles⟩