AI summaryⓘ
The authors created a computer-checked (formalized) proof about how certain mathematical rules for measuring preferences add up, especially those used in classical lottery theory. They show that a key condition called the cross-pair Thomsen or hexagon condition cannot be simplified using only the basic rules of additive conjoint measurement. They provide an explicit example that meets these basic rules but fails the hexagon condition. Around this result, they formalized the entire mathematical construction needed to build continuous utility functions and related concepts, ensuring all proofs are exact and free of gaps. Their work clearly maps out what can and cannot be proven from the fundamental assumptions in this measurement theory.
Additive Conjoint MeasurementClassical LotteryCross-Pair Thomsen ConditionDouble CancellationOrdinal AxiomsStandard SequenceDebreu UtilityLean 4 FormalizationMachine-Checked ProofArchimedean Condition
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.