Ilia Tsetlin | Searcharxiv

arXiv2026

A Kernel-Clean Lean Mechanization of Classical Lottery in Action and the Wakker--Debreu--Koopmans Representation Layer

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.

cs.LO↗

arXiv2026

Betting on Bets: Anytime-Valid Tests for Stochastic Dominance

How can we monitor, in real time, whether one uncertain prospect has any upside over another? To answer this question, we develop a novel family of sequential, anytime-valid tests for stochastic dominance (SD), a classical and popular notion for comparing entire distribution functions. The problem is distinct from that of testing mean dominance, and it is particularly useful when comparing distributions with similar means or with ordinal outcomes. We first derive powerful, nonparametric e-processes that quantify evidence against the null hypothesis that one prospect is stochastically dominated by another. For first-order SD, these e-processes are based on mixtures of growth-rate optimal e-variables, yielding a test of power one that retains validity under continuous monitoring. We then generalize the approach to sequential testing for higher-order SD and other integral stochastic orders. Empirically, we find that the tests are competitive in power with classical, non-anytime-valid SD tests. Our real-world application examines a controversial phenomenon in baseball analytics, known as the "third-time-through-the-order (3TTO) penalty," viewed as a monitoring problem. We close by sketching the complementary problem of testing whether a prospect has a definite upside, formalizing conditions under which we can derive a powerful anytime-valid test.

stat.ME↗