A Kernel-Clean Lean Mechanization of Classical Lottery in Action and the Wakker--Debreu--Koopmans Representation Layer
Jingyuan Li, Ilia Tsetlin, Fan Wang
cs.LO
Jun 8, 2026 · v1
TL;DR
Formalizes additive conjoint measurement and the Wakker-Debreu-Koopmans representation layer in Lean 4 with Mathlib.
Abstract
We present a Lean 4/Mathlib formalization of the additive representation theory behind Classical Lottery in Action and the Wakker-Debreu-Koopmans (WDK) layer it relies on. Our central result is a machine-checked proof that the cross-pair Thomsen / double-cancellation (hexagon) condition is irreducible from the ordinal axioms of additive conjoint measurement (weak order, restricted solvability, Archimedean condition, and tradeoff consistency). We exhibit an explicit verified counter-model (additiveRealBoolPref) satisfying all ordinal axioms yet failing the cross-pair condition, with every strict standard sequence being an arithmetic progression and hence non-dense. Around this boundary we mechanize the full derivable construction: continuous Debreu/Eilenberg utility from separability, standard-sequence grids, bisection methods from connectedness, and global additive gluing. All public theorems are sorry-free conditional wrappers over this single irreducible structural input. The development is kernel-clean, depending only on standard Lean foundations (propext, Classical.choice, Quot.sound). The companion file ClassicalLotteryInAction.lean formalizes local classical-lottery constructions, average-utility results, matching-frequency lemmas, and ambiguity-attitude statements used by the Management Science paper. This draws a precise, machine-certified line between what additive conjoint measurement can prove and what it must assume.
Problem
Additive conjoint measurement theory in economics relies on the cross-pair Thomsen (hexagon) condition as a primitive axiom, but it has not been formally demonstrated whether this condition is irreducible from the other ordinal axioms (weak order, restricted solvability, Archimedean condition, tradeoff consistency).
Approach
The authors present a Lean 4/Mathlib formalization of the Wakker-Debreu-Koopmans representation layer. They construct an explicit verified counter-model (additiveRealBoolPref) that satisfies all ordinal axioms yet fails the cross-pair condition, proving irreducibility. Around this boundary they mechanize the full derivable construction: continuous Debreu/Eilenberg utility from separability, standard-sequence grids, bisection methods, and global additive gluing. All public theorems are sorry-free conditional wrappers, and the development is kernel-clean (depending only on propext, Classical.choice, Quot.sound).
Results
The formalization provides a machine-certified proof that the cross-pair condition cannot be derived from the other ordinal axioms of additive conjoint measurement. A companion file formalizes local classical-lottery constructions including average-utility results and ambiguity-attitude statements. The entire artifact is kernel-axiom-clean and audited via explicit #print axioms regression files.
