Report 5: The Two-Prior Witness and the M5 Negatives
Conditional Admissibility Judgments, Technical Report Series
Internal working document. Every definition and result below is verified in Lean 4 against Mathlib; each environment cites the corresponding Lean declaration in the form File.lean · Name. The witness lives in the test tree (test/CAJTest/TwoPrior.lean, namespace CAJTest), deliberately outside the library: the library CAJ carries the general theory, the test tree its concrete models. The Lean sources are authoritative where this report and the code differ.
1 Introduction
The positive results of Report 4 say what the commensuration thesis yields: the E-admissibility class, minimally. This report supplies the negatives that make those results bite, all witnessed by a single small, fully designed decision problem — two states, three acts, two priors:
- M5(a) — incommensurability within SEU (Theorem 2): no SEU judgment gives the two extreme SEU judgments even a fair hearing (the weak condition of Report 2), a fortiori none suspends between them. The change between them is not commensurable within K_{\mathrm{SEU}} — but it is within K_{\mathrm{Eadm}} (Proposition 2). This is Levi’s argument in miniature, and it shows the closure of Report 4 is strict: K_{\mathrm{SEU}} is not join-closed.
- M5(b) — the convexity wedge (Theorem 4): the two-prior credal state is not choice-equivalent to its convex hull; the even mixture of the priors admits an act both extreme priors reject. Commensuration closure never forces convex closure.
- M5(c) — the β-violation (Theorem 3): the pair’s E-admissibility judgment satisfies Sen’s α but violates β — hence WARP — already at the vacuous supposition. The β-corollary of Report 4 is realized, not hypothetical.
The report also records the design rationale of the witness (every numerical choice is load-bearing; see the callout in Section 2) and a commutation sanity check.
2 The witness context
Definition 1 (The two-prior context) The decision context is:
- States: X = \{F, T\} (in Lean,
Bool, with F =false, T =true); - Suppositions: the full powerset of X;
- Acts: A = \{a_0, a_1, a_2\} (in Lean,
Fin 3); - Menus: every nonempty set of acts.
The utility is state-dependent payoff:
| state F | state T | |
|---|---|---|
| a_0 (safe) | 6/5 | 6/5 |
| a_1 (bet on F) | 2 | 0 |
| a_2 (bet on T) | 0 | 2 |
All the credal-context side conditions of Report 3 hold trivially: every set is in the algebra, every utility range and menu is finite.
Lean: TwoPrior.lean · twoPriorCtx, payoff, twoPriorCC; the powerset algebra is Smoke.lean · powersetAlgebra. Named events and menus: eFalse, eTrue; fullMenu = \{a_0, a_1, a_2\}, menu01 = \{a_0, a_1\}, menu02 = \{a_0, a_2\}.
Definition 2 (The two priors) Since the algebra is the powerset of a two-element state space, a fap is exactly a pair of nonnegative weights summing to 1 (the general weights-to-fap construction is finFap). Define:
p_0(F) = \tfrac{7}{10},\ p_0(T) = \tfrac{3}{10};
\qquad
p_1(F) = \tfrac{3}{10},\ p_1(T) = \tfrac{7}{10}.
p_0 favors the bet on F; p_1 the bet on T. The credal pair is P := \{p_0, p_1\}.
Lean: TwoPrior.lean · finFap, finFap_p, w0, w1, prior0, prior1, credalPair; atom values prior0_eFalse etc.
The safe payoff 6/5 is chosen strictly inside the interval (1, 7/5), and both endpoints matter.
- Below 7/5: under each extreme prior the favored bet has expected utility 7/5 > 6/5, so each extreme prior rejects the safe act — this drives the Levi/SSK exclusion pattern (Theorem 1) and the β-violation.
- Above 1: under the even mixture of the two priors each bet has expected utility 1 < 6/5, so the mixture uniquely favors the safe act — this drives the convexity wedge (Theorem 4).
- Not equal to 1: with safe payoff exactly 1, the even mixture would tie all three acts, its SEU judgment would suspend the issue between the extreme judgments on every menu, and M5(a) would be false — a single prior would commensurate the change. The witness must sit off the tie.
The weights 7/10–3/10 are symmetric and comfortably away from the threshold weight 3/5 that appears in the proof of Theorem 2.
3 The expected-utility table
Throughout, judgments are evaluated at the vacuous supposition \top (where every fap is non-null). Write \mathrm{wEU}_q := \mathrm{wEU}_q (\top, \cdot) for the unnormalized expected utility of Report 3.
Lemma 1 (Generic expected utilities) For every fap q on the witness algebra: \mathrm{wEU}_q(a_0) = \tfrac{6}{5}, \qquad \mathrm{wEU}_q(a_1) = 2\, q(\{F\}), \qquad \mathrm{wEU}_q(a_2) = 2\, q(\{T\}), and q(\{F\}) + q(\{T\}) = 1.
Lean: TwoPrior.lean · wEU_top_act0, wEU_top_act1, wEU_top_act2, q_split.
Proof. The utility range of a_0 on \top is \{6/5\} with level set all of X, so the sum defining \mathrm{wEU} (Report 3) has the single term \tfrac{6}{5} \cdot q(X) = \tfrac{6}{5}. The range of a_1 is \{0, 2\} with level sets \{T\} and \{F\} respectively; the term at 0 vanishes and the term at 2 is 2 \, q(\{F\}). Symmetrically for a_2. The split identity is additivity on the disjoint atoms \{F\} \cup \{T\} = X plus normalization. \square
Specializing to the two priors and the mixture (computed by Lemma 1 and the atom values):
| p_0 | p_1 | \tfrac12 p_0 + \tfrac12 p_1 | |
|---|---|---|---|
| a_0 (safe) | 6/5 | 6/5 | 6/5 |
| a_1 (bet on F) | 7/5 | 3/5 | 1 |
| a_2 (bet on T) | 3/5 | 7/5 | 1 |
Lean: TwoPrior.lean · wEU_prior0_act0 … wEU_prior1_act2; mixture atoms uniformP_eFalse, uniformP_eTrue.
4 Choice sets
All six SEU choice sets needed below follow from the table by reading off the maxima; the Lean proofs check each act against each menu by direct computation.
Proposition 1 (SEU choice sets at \top) \begin{array}{l|ccc} & \{a_0,a_1,a_2\} & \{a_0,a_1\} & \{a_0,a_2\} \\\hline C_{\{p_0\}} & \{a_1\} & \{a_1\} & \{a_0\} \\ C_{\{p_1\}} & \{a_2\} & \{a_0\} & \{a_2\} \end{array}
Lean: TwoPrior.lean · seu_prior0_full, seu_prior1_full, seu_prior0_menu01, seu_prior1_menu01, seu_prior0_menu02, seu_prior1_menu02.
Proof. Read the table. Under p_0: on the full menu a_1 (7/5) strictly beats a_0 (6/5) and a_2 (3/5); on \{a_0, a_1\} likewise a_1 wins; on \{a_0, a_2\} the safe act (6/5) strictly beats a_2 (3/5). Under p_1, symmetrically with the roles of the bets swapped. Every maximum is strict, so every choice set is a singleton, and p_i(\top) = 1 \neq 0 throughout. \square
Theorem 1 (The Levi/SSK pattern) The E-admissibility judgment of the credal pair chooses exactly the two bets from the full menu: C_P(\top, \{a_0, a_1, a_2\}) = \{a_1, a_2\}, so the safe act is E-inadmissible — excluded despite being no prior’s worst option and the only act that is second-best by both lights. On the submenu \{a_0, a_1\}, by contrast, both acts are E-admissible: C_P(\top, \{a_0, a_1\}) = \{a_0, a_1\}.
Lean: TwoPrior.lean · eAdm_pair_full, safe_excluded, eAdm_pair_menu01.
Proof. By M1 (Report 3), C_P is the pointwise union of the two SEU choice sets. On the full menu: \{a_1\} \cup \{a_2\} = \{a_1, a_2\}. On \{a_0, a_1\}: \{a_1\} \cup \{a_0\} = \{a_0, a_1\}. \square
The full-menu verdict is the classic E-admissibility phenomenon (Levi; Seidenfeld–Schervish–Kadane): an act can be uniformly moderate — never optimal for any member of the credal state — and hence excluded, even though intuitively it is the natural compromise. Here it is not the target of criticism but the engine of the negatives: the submenu verdict keeps the safe act alive, and the tension between the two verdicts is precisely a β-violation (Theorem 3).
5 M5(a): incommensurability within the SEU class
Theorem 2 (No SEU judgment gives the extremes a fair hearing) There is no fap q such that C_{\{q\}} gives C_{\{p_0\}} and C_{\{p_1\}} a fair hearing (Report 2). Consequently no SEU judgment suspends the issue between them.
Lean: TwoPrior.lean · no_seu_fairHearing, no_seu_suspends.
Proof. Suppose C_{\{q\}} gives both a fair hearing. All four choice sets of Proposition 1 on the two submenus are nonempty singletons, so fair hearing forces C_{\{q\}}’s choice set to contain each of them:
- meeting C_{\{p_0\}}(\top, \{a_0,a_1\}) = \{a_1\} forces a_1 \in C_{\{q\}}(\top, \{a_0,a_1\}), i.e. \mathrm{wEU}_q(a_0) \le \mathrm{wEU}_q(a_1): \ \tfrac{6}{5} \le 2\, q(\{F\});
- meeting C_{\{p_1\}}(\top, \{a_0,a_1\}) = \{a_0\} forces a_0 \in C_{\{q\}}(\top, \{a_0,a_1\}), i.e. 2\, q(\{F\}) \le \tfrac{6}{5};
- meeting C_{\{p_1\}}(\top, \{a_0,a_2\}) = \{a_2\} and C_{\{p_0\}}(\top, \{a_0,a_2\}) = \{a_0\} likewise forces 2\, q(\{T\}) = \tfrac{6}{5}.
So q(\{F\}) = q(\{T\}) = \tfrac{3}{5}, whence q(\{F\}) + q(\{T\}) = \tfrac{6}{5} \neq 1, contradicting Lemma 1’s split identity. Since suspension implies fair hearing (Report 2), no SEU judgment suspends either. \square
The proof exhibits the structural obstruction cleanly: fair hearing at singleton choice sets means agreement, and no single coherent prior can agree with p_0 about the menu \{a_0, a_1\} and with p_1 about \{a_0, a_2\} — the two agreements pin its atom probabilities to values that violate additivity. Suspension between SEU judgments demands more probability than a coherent prior has to give.
Corollary 1 (M5(a), class form) The change C_{\{p_0\}} \rightsquigarrow C_{\{p_1\}} is not weakly commensurable — a fortiori not commensurable — within K_{\mathrm{SEU}}. In particular K_{\mathrm{SEU}} is not join-closed, so the closure of Report 4 is strict: K_{\mathrm{SEU}} \subsetneq K_{\mathrm{Eadm}}.
Lean: TwoPrior.lean · not_weaklyCommensurable_KSEU, not_commensurable_KSEU.
Proof. A commensurating (or fairly-hearing) member of K_{\mathrm{SEU}} is by definition C_{\{q\}} for some fap q, contradicting Theorem 2. If K_{\mathrm{SEU}} were join-closed, Report 2’s internal-commensurability theorem would commensurate the change within it. \square
Proposition 2 (Levi’s move in miniature) The same change is commensurable within K_{\mathrm{Eadm}}: the E-admissibility judgment of the union credal state — here C_P itself, since P = \{p_0\} \cup \{p_1\} — suspends the issue.
Lean: TwoPrior.lean · commensurable_KEadm.
Proof. K_{\mathrm{Eadm}} is join-closed (Report 4) and contains both extreme judgments (singleton credal states); apply internal commensurability. The intermediary produced is the join, which by Report 4’s M3 is C_{\{p_0\} \cup \{p_1\}} = C_P. \square
Together, Corollary 1 and Proposition 2 are the project’s central contrast realized in the smallest possible arena. An SEU agent contemplating the change from p_0 to p_1 — a perfectly ordinary reversal of opinion about a coin’s bias — has, within her own theory of rational states, no state from which the change can be adjudicated without begging the question. The minimal repair is to admit the two-membered credal state P, and with it E-admissibility. Nothing in the repair asks for the mixtures in between: that is M5(b).
6 M5(c): the β-violation realized
Theorem 3 (The pair’s judgment violates β (hence WARP) at \top) C_P satisfies Sen’s α at \top but violates Sen’s β — and therefore WARP — at \top.
Lean: TwoPrior.lean · eAdm_pair_not_senBetaAt, eAdm_pair_not_warpAt; the α instance is the example following them.
Proof. α holds at every supposition for every E-admissibility judgment (Report 4). For β, the witness pattern of Report 4 is exhibited by m' = \{a_0, a_1\} \subseteq m = \{a_0, a_1, a_2\} with acts a_0, a_1: by Theorem 1, a_0, a_1 \in C_P(\top, m'), \qquad a_0 \notin C_P(\top, m), \qquad a_1 \in C_P(\top, m). Two acts jointly admissible from the submenu fail to stand or fall together in the full menu; β fails, and WARP fails with it (WARP implies β, Report 1). \square
The mechanism is exactly the one diagnosed abstractly in Report 4: different joinands vouch for the two acts on the submenu (p_0 for a_1, p_1 for a_0), and only one of the vouchers survives enlargement. Combined with Proposition 2, this instantiates the β-corollary: the commensurating intermediary that Levi’s move provides for the change C_{\{p_0\}} \rightsquigarrow C_{\{p_1\}} is itself a WARP-violating judgment. Dynamic rationality is purchased at a static price, and the price is paid at the vacuous supposition — no exotic conditioning is involved.
7 M5(b): the convexity wedge realized
Definition 3 (The even mixture) Let u := \tfrac12 p_0 + \tfrac12 p_1, so u(\{F\}) = u(\{T\}) = \tfrac12. By construction u \in \mathrm{conv}(P).
Lean: TwoPrior.lean · uniformP, uniformP_eFalse, uniformP_eTrue, uniformP_mem_hull.
Theorem 4 (M5(b): the pair is not convex-equivalent) The safe act is SEU-admissible (indeed uniquely optimal) under u from the full menu; hence a_0 \in C_{\mathrm{conv}(P)}(\top, \text{full}) while a_0 \notin C_P(\top, \text{full}). Therefore C_P \neq C_{\mathrm{conv}(P)}: the credal pair is not convex-equivalent (Report 4, M4), and convexification strictly coarsens its judgment.
Lean: TwoPrior.lean · safe_in_seu_uniform, not_convexEquivalent.
Proof. By the expected-utility table, under u the safe act scores 6/5 against 1 for each bet, so it is the unique maximizer on the full menu, and u(\top) = 1 \neq 0: thus a_0 \in C_{\{u\}}(\top, \text{full}). Since u \in \mathrm{conv}(P), the existential characterization of E-admissibility (Report 3) gives a_0 \in C_{\mathrm{conv}(P)}(\top, \text{full}). But a_0 \notin C_P(\top, \text{full}) by Theorem 1. The two judgments differ at (\top, \text{full}), refuting convex equivalence. \square
This completes the wedge announced in Reports 3 and 4. The commensuration thesis moved the SEU theorist to K_{\mathrm{Eadm}} (Corollary 1, Proposition 2); every step of that derivation used unions and joins, never mixtures; and here is a credal state where the mixture makes a choice-relevant difference — \mathrm{conv}(P) admits the compromise act that P rejects. Whether to convexify is therefore a genuine further question, on which commensuration is silent. (Which answer is right is a substantive matter the formal development does not adjudicate; what it proves is that the two commitments are independent.)
8 Commutation sanity check
As a use of Report 4’s machinery in the witness: conditioning p_0 on \{F\} (probability 7/10 \neq 0) and judging at the vacuous supposition agrees, menu by menu, with judging p_0 at the conjoined supposition \{F\} \sqcap \top: C_{\{p_0|_{\{F\}}\}}(\top, m) = C_{\{p_0\}}(\{F\} \sqcap \top,\, m).
Lean: TwoPrior.lean · prior0_eFalse_ne_zero and the closing example, instantiating seu_condition_C.
9 Formalization notes
| Report item | Lean declaration (file · name) |
|---|---|
| Definition 1 | TwoPrior.lean · twoPriorCtx, payoff, twoPriorCC, fullMenu, menu01, menu02, eFalse, eTrue; Smoke.lean · powersetAlgebra |
| Definition 2 | TwoPrior.lean · finFap, finFap_p, w0, w1, prior0, prior1, credalPair |
| Lemma 1 | TwoPrior.lean · wEU_top_act0/1/2, q_split |
| EU table | TwoPrior.lean · prior0_eFalse …, wEU_prior0_act0 … wEU_prior1_act2 |
| Proposition 1 | TwoPrior.lean · seu_prior0_full, seu_prior1_full, seu_prior0_menu01, seu_prior1_menu01, seu_prior0_menu02, seu_prior1_menu02 |
| Theorem 1 | TwoPrior.lean · eAdm_pair_full, safe_excluded, eAdm_pair_menu01 |
| Theorem 2 | TwoPrior.lean · no_seu_fairHearing, no_seu_suspends |
| Corollary 1 | TwoPrior.lean · not_weaklyCommensurable_KSEU, not_commensurable_KSEU |
| Proposition 2 | TwoPrior.lean · commensurable_KEadm |
| Theorem 3 | TwoPrior.lean · eAdm_pair_not_senBetaAt, eAdm_pair_not_warpAt |
| Definition 3, Theorem 4 | TwoPrior.lean · uniformP, uniformP_mem_hull, safe_in_seu_uniform, not_convexEquivalent |
| Commutation check | TwoPrior.lean · prior0_eFalse_ne_zero + closing example |
Encoding remarks:
- Weights to faps.
finFapbuilds a fap on the powerset algebra of any finite type from a nonnegative weight function summing to 1 (probability of a set = sum of its weights, viaFinsetsums);finFap_pevaluates it against any explicitFinsetenumeration. This is the reusable part of the witness file. - Concrete computation style. The context is marked
@[reducible]so instance search sees through it; membership facts are computed byrwwith the specificwEU_…equations followed bynorm_num, withdecidehandlingFin 3andBoolcase splits. The library-sideMininstance on events is bridged to the concrete context by a one-lineinstanceso that⊓notation applies (Report 1’s conjunction). - The fair-hearing refutation is four instantiations and
linarith: each of the four forced memberships yields one linear inequality in q(\{F\}), q(\{T\}) (via Lemma 1), and the split identity closes the system. The proof is robust to the particular weights so long as the safe payoff stays off the tie (see the design callout). - Library/test separation. Nothing in
CAJdepends on the witness; the negatives are facts about the general theory, established in its test suite. A journal presentation would state M5 as “there exists a context and credal pair such that …” — the Lean statement is exactly that, with the existential witnessed by construction.