Tagewerk XXIV

Exact-census confirmation of the first EFX-nonexistence counterexample (Akrami–Mayorov–Mehlhorn–Srinivas–Weidenbach 2026)

A landmark 2026 result in a domain new to the ledger — fair division / discrete allocation — independently confirmed by exact exhaustive census. Whether an EFX (envy-free up to any good) allocation always exists was a central open problem. Akrami, Mayorov, Mehlhorn, Srinivas & Weidenbach (arXiv:2604.18216) resolve it negatively with a SAT-found instance: 3 agents, 8 goods, monotone valuations, and NO EFX allocation. Each agent i's valuation vᵢ is ordinal — vᵢ(A) is the rank (0..255) of the subset A in agent i's linear order over the 2⁸ = 256 subsets. Leibniz vendors the three arbitrary SAT-found rank tables verbatim from the paper's companion artifact and re-decides the counterexample by exact-integer exhaustive census: (1) each valuation is a valid monotone bijection onto {0..255} (∅→0, full→255; A⊂B ⟹ vᵢ(A)<vᵢ(B)) — a legitimate monotone valuation, exactly the class the EFX question is posed for; (2) NONE of the 3⁸ = 6561 allocations is EFX — for every allocation some agent EFX-envies another; (3) as a faithfulness cross-check, exactly 272 of the 5796 all-nonempty allocations violate exactly one of the 16 EFX-conditions, reproducing the paper's own reported statistic bit-for-bit and certifying the tables were ingested correctly. This is an audit of a SAT-found instance (the valuations are arbitrary and not reconstructible), decided by an exact-integer exhaustive procedure — no floating point, no LLM judgment. A full in-kernel decide census (6561 allocations × 256-entry lookups) exceeds the kernel's reduction budget, so the exact census is the decider; the authors separately formalized the SAT-encoding's correctness in Lean, making this the complementary instance-level check. Report-only, audit tier — no trust surface. LLMs propose nothing; an exact decision procedure decides.