Pith. sign in

REVIEW 1 minor 8 references

A Lean formalization exhibits a verified counter-model showing the cross-pair Thomsen condition cannot be derived from the ordinal axioms of additive conjoint measurement.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.3

2026-06-27 15:04 UTC pith:IBIHZXVF

load-bearing objection Lean formalization cleanly shows the Thomsen condition is independent of the listed ordinal axioms via a verified counter-model.

arxiv 2606.08902 v1 pith:IBIHZXVF submitted 2026-06-08 cs.LO econ.TH

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

Jingyuan Li , Ilia Tsetlin , Fan Wang This is my paper
classification cs.LO econ.TH
keywords Lean formalizationadditive conjoint measurementThomsen conditiondouble cancellationcounter-modelrepresentation theorymachine-checked proofdecision theory
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper delivers a machine-checked Lean proof that the cross-pair Thomsen or double-cancellation condition is irreducible from the four ordinal axioms of additive conjoint measurement: weak order, restricted solvability, the Archimedean condition, and tradeoff consistency. It establishes this by constructing and verifying the explicit model additiveRealBoolPref, which obeys all four axioms yet violates the Thomsen condition, with every strict standard sequence forming a non-dense arithmetic progression. Around this boundary the work mechanizes all the constructions that do follow, including continuous utility from separability, standard-sequence grids, bisection from connectedness, and global additive gluing. The entire development remains kernel-clean, depending only on basic Lean foundations, and includes a companion formalization of classical-lottery constructions and related results.

Core claim

The central claim is a machine-checked proof that the cross-pair Thomsen / double-cancellation (hexagon) condition is irreducible from the ordinal axioms of additive conjoint measurement. The proof rests on an explicit verified counter-model additiveRealBoolPref that satisfies weak order, restricted solvability, the Archimedean condition, and tradeoff consistency while failing the cross-pair condition; every strict standard sequence in the model is an arithmetic progression and hence non-dense. All public theorems are sorry-free conditional wrappers over this single irreducible structural input.

What carries the argument

The verified counter-model additiveRealBoolPref, which acts as an explicit witness that the four ordinal axioms do not entail the cross-pair Thomsen condition.

Load-bearing premise

The counter-model additiveRealBoolPref satisfies every listed ordinal axiom while violating the cross-pair Thomsen condition.

What would settle it

Demonstrating that additiveRealBoolPref fails to satisfy one of the ordinal axioms, such as tradeoff consistency or the Archimedean condition, would falsify the irreducibility result.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Continuous Debreu/Eilenberg utility from separability, standard-sequence grids, bisection methods from connectedness, and global additive gluing are all mechanized as derivable constructions.
  • All public theorems become sorry-free conditional wrappers over the single irreducible input.
  • A companion file formalizes local classical-lottery constructions, average-utility results, matching-frequency lemmas, and ambiguity-attitude statements.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The boundary identified here can be used to test whether other representation theorems in measurement theory similarly require an independent structural axiom.
  • The same counter-model technique could be applied to expected-utility or ambiguity models to isolate exactly which axioms are independent.
  • Kernel-clean formalizations of this kind make it feasible to check whether informal proofs in decision theory have inadvertently assumed the Thomsen condition.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 1 minor

Summary. The manuscript presents a Lean 4/Mathlib formalization of the additive representation theory for Classical Lottery in Action and the Wakker-Debreu-Koopmans layer. Its central claim 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), established by an explicit verified counter-model additiveRealBoolPref that satisfies all listed axioms yet violates the Thomsen condition (with every strict standard sequence an arithmetic progression). The work also mechanizes the derivable constructions: 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; the development depends only on propext, Classical.choice, and Quot.sound. A companion file formalizes local classical-lottery constructions, average-utility results, and ambiguity-attitude statements.

Significance. If the result holds, the work supplies a machine-certified boundary in additive conjoint measurement between derivable ordinal consequences and statements that must be assumed separately. The kernel-clean, sorry-free character with an explicit counter-model (non-dense standard sequences) provides concrete, reproducible evidence of irreducibility that is stronger than informal counter-examples. The mechanization of the full derivable layer (utilities, grids, gluing) and the classical-lottery components offers a verified foundation usable by applied decision-theory papers, directly addressing reproducibility concerns in the area.

minor comments (1)
  1. The abstract states that the counter-model satisfies 'every listed ordinal axiom' while violating the cross-pair condition; a brief explicit listing or cross-reference in §3 or the model definition would make the independence claim easier to verify at a glance without opening the Lean file.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment and the recommendation to accept the manuscript.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper's central result is a machine-checked Lean formalization proving irreducibility of the cross-pair Thomsen condition from the ordinal axioms of additive conjoint measurement via an explicit counter-model (additiveRealBoolPref) that satisfies weak order, restricted solvability, Archimedean condition, and tradeoff consistency while violating the condition. The development is kernel-clean, depends only on propext, Classical.choice and Quot.sound, and all public theorems are sorry-free. No derivation step reduces by construction to fitted inputs, self-definitions, or load-bearing self-citations; the formal verification is self-contained against the stated axioms and provides independent evidence of the independence result.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the formalization correctly encoding the four ordinal axioms and verifying that the counter-model satisfies them while violating the target condition; no free parameters or invented entities are introduced.

axioms (1)
  • domain assumption weak order, restricted solvability, Archimedean condition, and tradeoff consistency
    These are the ordinal axioms stated in the abstract from which irreducibility of the Thomsen condition is claimed.

pith-pipeline@v0.9.1-grok · 5786 in / 1382 out tokens · 38717 ms · 2026-06-27T15:04:17.106982+00:00 · methodology

0 comments
read the original 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

8 extracted references

  1. [1]

    Management Science, 2026

    Jingyuan Li, Ilia Tsetlin, and Fan Wang.Classical Lottery in Action: Quantifying Risk and Evaluating Uncertainty. Management Science, 2026

    2026

  2. [2]

    Wakker.Additive Representations of Preferences: A New Foundation of Decision Analysis

    Peter P. Wakker.Additive Representations of Preferences: A New Foundation of Decision Analysis. Kluwer Academic Publishers, 1989

    1989

  3. [3]

    Koopmans

    Gerard Debreu and Tjalling C. Koopmans. Additively decomposed quasiconvex functions. Mathematical Programming, 24:1–38, 1982

    1982

  4. [4]

    Krantz, R

    David H. Krantz, R. Duncan Luce, Patrick Suppes, and Amos Tversky.Foundations of Measure- ment, Volume I: Additive and Polynomial Representations. Academic Press, 1971. 11

    1971

  5. [5]

    https://github.com/ leanprover-community/mathlib4

    The Mathlib Community.The Lean mathematical library. https://github.com/ leanprover-community/mathlib4

  6. [6]

    https://www.isa-afp.org/

    The Isabelle Archive of Formal Proofs. https://www.isa-afp.org/

  7. [7]

    GitHub repository, 2026

    Jingyuan Li.Classical Lottery in Action: Lean 4 artifact companion. GitHub repository, 2026. https://github.com/jingyuanli-hk/classical-lottery-in-action-lean-artifact

    2026

  8. [8]

    GitHub repository, 2026

    Jingyuan Li.Wakker–Debreu–Koopmans Lean formalization. GitHub repository, 2026. https: //github.com/jingyuanli-hk/-wakker-debreu-koopmans-lean. 12

    2026