Luce (1959): Individual Choice Behavior [Luc59]

Formalizes §1.G (the jnd semiorder and the trace), §2.B's power-law Weber ratio, and Chapter 3's utility theory.

Chapter 3 treats choices among gambles: aρb is "outcome a if chance event ρ occurs, else b" (p. 78), and S(A,E) = (A × E × A) ∪ A collects gambles and pure alternatives. A decomposable preference structure ⟨A, E, P, Q⟩ (Definition 5) couples a choice function P over S(A,E) with an event choice function Q via Axiom 2: P(aρb, aσb) = P(a,b)·Q(ρ,σ) + P(b,a)·Q(σ,ρ).

Main results

• DecomposablePreference: Definition 5 (p. 78), Axiom 2 in full mixture form; gam_of_alt_eq_one is the reduced form P(aρb, aσb) = Q(ρ,σ) under perfect discrimination P(a,b) = 1, as used inside the proofs of Theorems 13–14.
• Complementation: Axiom 3 (p. 83), P(aρb, x) = P(bρ̄a, x), with E a Boolean algebra as Luce requires. NontrivialPreference: Axiom 4 (p. 83).
• q_compl_compl: Lemma 9 (p. 84), Q(ρ, σ) = Q(σ̄, ρ̄); v_mul_v_compl_const derives from it the constancy of v(ρ)·v(ρ̄), the source of the φ(ρ)φ(ρ̄) = constant clause of §3.D.3 (p. 89).
• Neutral / Favorable / Unfavorable: comparison of an event to its own complement — Luce's classes C(½), C(1), C(0) (Lemma 11, p. 85). neutral_indifferent is the first clause of Lemma 10 (p. 84); favorable_gt_unfavorable is the between-class ordering.
• The §3.B.2 chain: lemma5 (the cubic constraint, p. 80), eventPref_trans (Lemma 6), lemma7 (p. 81), and atMostThreeClasses — Lemma 8/Theorem 10 as a four-event pigeonhole. theorem11 (p. 82): Q is constant across ∼-classes; with Lemma 9 it yields both clauses of Lemma 10 (neutral_indifferent, neutral_of_indiff_neutral, p. 84).
• theorem12 (p. 84): given Axioms 3–5 (HasNeutralEvent is Axiom 5) and nondegeneracy, exactly three classes — Luce's C(1), C(½), C(0) (atLeastThreeClasses is Lemma 11, p. 85).
• theorem13 / theorem14: the two §3.D theorems (pp. 86, 89) behind Luce's proposed experiment; gam_of_factored is the observable consequence (p. 90) of the suggested local decomposition v(aρb) = w(a,b)·φ(ρ) of §3.D.3 — Luce offers the factoring as a hypothesis, not a theorem, and so does this file.

Formalization notes

Luce's P and Q are families of probability measures on subsets of size ≤ 3 (Definition 5); here both are total ChoiceFns, which is where the diagonal bites: binary x x = 1, so Axiom 2 needs its a ≠ b guard (axiom2_unguarded_false) and Axiom 3 its two x-guards (complementation_unguarded_false) — for Luce those instances are degenerate singleton choices. Ratio scales enter as ChoiceFn.BinaryRatioScaleOn, local to the gamble set under discussion, because Chapter 3 mixes imperfect discrimination among gambles with perfect discrimination among pure alternatives (P(a,b) = 1), which a globally positive scale cannot represent.

Axiom 1 lives in the structure (axiom1P/axiom1Q, in ChoiceFn.HasChoiceAxiom's two-clause form) exactly as Definition 5 demands; only the §3.C additional axioms and Theorem 10's nondegeneracy enter as per-theorem hypotheses, as in the book. The three-class theorems are stated representative-wise — among any four events two are equi-likely (atMostThreeClasses); three pairwise non-equivalent events to one of which every event is equivalent (theorem12) — avoiding quotient machinery; a Setoid-packaged corollary is natural future work. The three-class regime forces perfect discrimination Q ∈ {0, 1} between extreme classes, which is exactly what HasChoiceAxiom's deletion clause (and no globally positive ratio scale) tolerates.

§1.G: Just noticeable differences and the trace (pp. 34–37)

A jnd threshold π ∈ (1/2, 1) splits pairwise choice into a discriminable-preference relation L(π) and an indistinguishability relation I(π) (Definition 3, p. 34). Given the positive ratio scale delivered by Theorem 4, the pair satisfies Luce's semiorder axioms (Theorem 5, p. 35) — trichotomy, I-reflexivity, the interval condition, and no-sandwiching — and the trace ordering (Definition 4, p. 37) is a weak order coinciding with the ratio-scale order (Theorem 6, p. 37).

def Luce1959.jndL {A : Type u_1} (v : A → ℝ) (thr : ℝ) (x y : A) : Prop

The L(π) relation (Definition 3, p. 34): x L(π) y iff P(x, {x,y}) > π — x is discriminably preferred to y at threshold π, for 1/2 < π < 1.

Equations

• Luce1959.jndL v thr x y = (thr < Core.pairwiseProb v x y)

def Luce1959.jndI {A : Type u_1} (v : A → ℝ) (thr : ℝ) (x y : A) : Prop

The I(π) relation (Definition 3, p. 34): x I(π) y iff 1 - π ≤ P(x, {x,y}) ≤ π — x and y are indistinguishable at threshold π.

Equations

• Luce1959.jndI v thr x y = (1 - thr ≤ Core.pairwiseProb v x y ∧ Core.pairwiseProb v x y ≤ thr)

theorem Luce1959.jndI_symm {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (thr : ℝ) (x y : A) (h : jndI v thr x y) : jndI v thr y x

I(π) is symmetric: if x and y are indistinguishable, so are y and x.

theorem Luce1959.jndI_refl {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (thr : ℝ) (hthr_lower : 1 / 2 < thr) (_hthr_upper : thr < 1) (x : A) : jndI v thr x x

I-reflexivity: x I(π) x.

theorem Luce1959.jnd_trichotomy {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (thr : ℝ) (hthr_lower : 1 / 2 < thr) (_hthr_upper : thr < 1) (x y : A) : jndL v thr x y ∧ ¬jndL v thr y x ∧ ¬jndI v thr x y ∨ jndL v thr y x ∧ ¬jndL v thr x y ∧ ¬jndI v thr x y ∨ jndI v thr x y ∧ ¬jndL v thr x y ∧ ¬jndL v thr y x

Trichotomy: for any x, y, exactly one of xLy, yLx, or xIy holds.

theorem Luce1959.jndL_interval {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (thr : ℝ) (_hthr_lower : 1 / 2 < thr) (_hthr_upper : thr < 1) (x y z w : A) (hxy : jndL v thr x y) (hyz : jndI v thr y z) (hzw : jndL v thr z w) : jndL v thr x w

Interval condition: xLy ∧ yIz ∧ zLw → xLw.

theorem Luce1959.jndL_no_sandwich {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (thr : ℝ) (hthr_lower : 1 / 2 < thr) (hthr_upper : thr < 1) (x y z w : A) (hxy : jndL v thr x y) (hyz : jndL v thr y z) : ¬(jndI v thr x w ∧ jndI v thr w z)

No sandwiching: xLy ∧ yLz → ¬(xIw ∧ wIz) — no w can be indistinguishable from both endpoints of a discriminable chain.

theorem Luce1959.jndL_trans {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (thr : ℝ) (hthr_lower : 1 / 2 < thr) (hthr_upper : thr < 1) (x y z : A) (hxy : jndL v thr x y) (hyz : jndL v thr y z) : jndL v thr x z

L-transitivity: xLy ∧ yLz → xLz. Not one of the semiorder axioms — it follows from the interval condition instantiated at z := y, via I-reflexivity.

def Luce1959.traceGe {A : Type u_1} (v : A → ℝ) (x y : A) : Prop

The trace relation (Definition 4, p. 37): x ≥_T y iff P(x, z) ≥ P(y, z) for all z — dominance in every pairwise comparison against a common reference.

Equations

• Luce1959.traceGe v x y = ∀ (z : A), Core.pairwiseProb v y z ≤ Core.pairwiseProb v x z

theorem Luce1959.trace_iff_scale_ge {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (x y : A) : traceGe v x y ↔ v y ≤ v x

Theorem 6: the trace relation is equivalent to the scale ordering v(y) ≤ v(x).

theorem Luce1959.trace_iff_pairwiseProb_ge_half {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (x y : A) : traceGe v x y ↔ 1 / 2 ≤ Core.pairwiseProb v x y

Corollary: x ≥_T y iff P(x, y) ≥ 1/2.

theorem Luce1959.traceGe_refl {A : Type u_1} (v : A → ℝ) (x : A) : traceGe v x x

The trace is reflexive: x ≥_T x.

theorem Luce1959.traceGe_trans {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (x y z : A) (hxy : traceGe v x y) (hyz : traceGe v y z) : traceGe v x z

The trace is transitive: x ≥_T y ∧ y ≥_T z → x ≥_T z.

theorem Luce1959.traceGe_total {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (x y : A) : traceGe v x y ∨ traceGe v y x

The trace is total: for any x, y, either x ≥_T y or y ≥_T x. With traceGe_refl and traceGe_trans, the trace is a weak order (total preorder).

theorem Luce1959.traceGe_of_jndL {A : Type u_1} (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (thr : ℝ) (hthr : 1 / 2 < thr) (x y : A) (h : jndL v thr x y) : traceGe v x y

The trace agrees with L: if xLy for any π, then x ≥_T y.

§2.B: The power law and Weber's law (pp. 42–44)

For the power scale v(s) = sⁿ, [Luc59] derives the linear generalization of Weber's law: the just-noticeable intensity ratio at threshold π is (π/(1−π))^(1/n). stevens_jndL_intensity_ratio is the C = 0 inequality form, stated over StevensScale from Processing.Psychophysics.

theorem Luce1959.stevens_jndL_intensity_ratio (σ : Core.StevensScale) (thr : ℝ) (hthr_lower : 1 / 2 < thr) (hthr_upper : thr < 1) {s₁ s₂ : ℝ} (h₁ : 0 < s₁) (h₂ : 0 < s₂) (hL : jndL (fun (x : ℝ) => x ^ σ.n) thr s₁ s₂) : (thr / (1 - thr)) ^ (1 / σ.n) < s₁ / s₂

Weber ratio from the jnd (§2.B): if s₁ is discriminably preferred to s₂ at threshold π under a power scale with exponent n, the intensity ratio s₁/s₂ exceeds (π/(1-π))^(1/n).

structure Luce1959.Gamble (A : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

A gamble aρb (p. 78): outcome win if the chance event event occurs, else lose.

• win : A

  Outcome if the event occurs.

• event : E

  The conditioning chance event.

• lose : A

  Outcome if the event does not occur.

@[instance_reducible]

instance Luce1959.instDecidableEqGamble {A✝ : Type u_3} {E✝ : Type u_4} [DecidableEq A✝] [DecidableEq E✝] : DecidableEq (Gamble A✝ E✝)

Equations

• Luce1959.instDecidableEqGamble = Luce1959.instDecidableEqGamble.decEq

def Luce1959.instDecidableEqGamble.decEq {A✝ : Type u_3} {E✝ : Type u_4} [DecidableEq A✝] [DecidableEq E✝] (x✝ x✝¹ : Gamble A✝ E✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Luce1959.Alternative (A : Type u_3) (E : Type u_4) : Type (max (max u_4 u_3) u_3)

Luce's total alternative set S(A,E) = (A × E × A) ∪ A (p. 78): gambles together with the pure alternatives.

Equations

• Luce1959.Alternative A E = (Luce1959.Gamble A E ⊕ A)

structure Luce1959.DecomposablePreference (A : Type u_3) (E : Type u_4) [DecidableEq A] [DecidableEq E] : Type (max u_3 u_4)

A decomposable preference structure ⟨A, E, P, Q⟩ (Definition 5, p. 78): choice over gambles and pure alternatives (P), choice over events by subjective likelihood (Q), coupled by Axiom 2: P(aρb, aσb) = P(a,b)·Q(ρ,σ) + P(b,a)·Q(σ,ρ).

Deviations from Luce: P and Q are total ChoiceFns rather than families on ≤3-element subsets (Axiom 1 enters as the axiom1P/axiom1Q fields, in ChoiceFn.HasChoiceAxiom's two-clause form), and Axiom 2 carries an a ≠ b guard — at a = b it is unsatisfiable for a total P (axiom2_unguarded_false), and Luce's own uses all have P(a,b) ∉ {0, 1} or P(a,b) = 1 with a, b a genuine pair.

• P : Core.ChoiceFn (Alternative A E)

  Choice over S(A,E).

• Q : Core.ChoiceFn E

  Choice over events by subjective likelihood.

• axiom2 (a b : A) : a ≠ b → ∀ (ρ σ : E), self.P.binary (Sum.inl { win := a, event := ρ, lose := b }) (Sum.inl { win := a, event := σ, lose := b }) = self.P.binary (Sum.inr a) (Sum.inr b) * self.Q.binary ρ σ + self.P.binary (Sum.inr b) (Sum.inr a) * self.Q.binary σ ρ

  Axiom 2 (p. 78), in Luce's full mixture form.

• axiom1P : self.P.HasChoiceAxiom

  P satisfies Luce's Axiom 1, per Definition 5.

• axiom1Q : self.Q.HasChoiceAxiom

  Q satisfies Luce's Axiom 1, per Definition 5.

theorem Luce1959.axiom2_unguarded_false {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [Nontrivial E] [Inhabited A] (P : Core.ChoiceFn (Alternative A E)) (Q : Core.ChoiceFn E) (h : ∀ (a b : A) (ρ σ : E), P.binary (Sum.inl { win := a, event := ρ, lose := b }) (Sum.inl { win := a, event := σ, lose := b }) = P.binary (Sum.inr a) (Sum.inr b) * Q.binary ρ σ + P.binary (Sum.inr b) (Sum.inr a) * Q.binary σ ρ) : False

Without its a ≠ b guard, Axiom 2 is unsatisfiable for a total choice function: at a = b it forces P(aρa, aσa) = Q(ρ,σ) + Q(σ,ρ) = 1 in both argument orders, contradicting binary complementarity. In Luce's system P(a, a) is the degenerate singleton choice.

def Luce1959.DecomposablePreference.alt {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) (a b : A) : ℝ

Luce's P(a, b) for pure alternatives.

Equations

• dp.alt a b = dp.P.binary (Sum.inr a) (Sum.inr b)

def Luce1959.DecomposablePreference.gam {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) (g h : Gamble A E) : ℝ

Luce's P(g, h) for gambles.

Equations

• dp.gam g h = dp.P.binary (Sum.inl g) (Sum.inl h)

theorem Luce1959.DecomposablePreference.gam_of_alt_eq_one {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {a b : A} (hab : a ≠ b) (h1 : dp.alt a b = 1) (ρ σ : E) : dp.gam { win := a, event := ρ, lose := b } { win := a, event := σ, lose := b } = dp.Q.binary ρ σ

The reduced decomposition under perfect discrimination, as used inside the proofs of Theorems 13–14 (p. 87): if P(a,b) = 1 then P(aρb, aσb) = Q(ρ, σ).

Definition 6: the subjective likelihood order

def Luce1959.DecomposablePreference.EventPref {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) (ρ σ : E) : Prop

Definition 6 (p. 79): ρ ≿ σ iff Q(ρ, σ) ≥ ½ — ρ is deemed at least as likely as σ.

Equations

• dp.EventPref ρ σ = (1 / 2 ≤ dp.Q.binary ρ σ)

def Luce1959.DecomposablePreference.EventIndiff {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) (ρ σ : E) : Prop

Subjective equi-likelihood ρ ∼ σ: the symmetric part of Definition 6's ≿. On distinct events this is Q(ρ, σ) = ½ (eventIndiff_iff_eq_half); on the diagonal it holds since Q(ρ, ρ) = 1.

Equations

• dp.EventIndiff ρ σ = (dp.EventPref ρ σ ∧ dp.EventPref σ ρ)

theorem Luce1959.DecomposablePreference.eventIndiff_refl {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) (ρ : E) : dp.EventIndiff ρ ρ

theorem Luce1959.DecomposablePreference.EventIndiff.symm {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {ρ σ : E} (h : dp.EventIndiff ρ σ) : dp.EventIndiff σ ρ

theorem Luce1959.DecomposablePreference.eventIndiff_iff_eq_half {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {ρ σ : E} (hne : ρ ≠ σ) : dp.EventIndiff ρ σ ↔ dp.Q.binary ρ σ = 1 / 2

theorem Luce1959.DecomposablePreference.ne_of_not_eventIndiff {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {ρ σ : E} (h : ¬dp.EventIndiff ρ σ) : ρ ≠ σ

theorem Luce1959.DecomposablePreference.gt_half_or_of_not_eventIndiff {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {ρ σ : E} (h : ¬dp.EventIndiff ρ σ) : 1 / 2 < dp.Q.binary ρ σ ∨ 1 / 2 < dp.Q.binary σ ρ

Totality of ≿ in strict form: a non-equi-likely pair is strictly ordered one way or the other.

def Luce1959.DecomposablePreference.Nondegenerate {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) : Prop

The nondegeneracy hypothesis of Theorem 10 (p. 80): some genuine pair of alternatives is discriminated imperfectly and asymmetrically, P(a, b) ∉ {0, ½, 1}.

Equations

• dp.Nondegenerate = ∃ (a : A) (b : A), a ≠ b ∧ dp.alt a b ≠ 0 ∧ dp.alt a b ≠ 1 / 2 ∧ dp.alt a b ≠ 1

The three-class theorems (§3.B.2)

theorem Luce1959.DecomposablePreference.lemma5 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {a b : A} (hab : a ≠ b) (h0 : dp.alt a b ≠ 0) (hhalf : dp.alt a b ≠ 1 / 2) (h1 : dp.alt a b ≠ 1) {ρ σ τ : E} (hρσ : ρ ≠ σ) (hστ : σ ≠ τ) (hρτ : ρ ≠ τ) : dp.alt a b * dp.alt b a * (2 * (dp.Q.binary ρ σ + dp.Q.binary σ τ + dp.Q.binary τ ρ) - 3) + (dp.alt a b - dp.alt b a) ^ 2 * (dp.Q.binary ρ σ * dp.Q.binary σ τ * dp.Q.binary τ ρ - dp.Q.binary ρ τ * dp.Q.binary τ σ * dp.Q.binary σ ρ) = 0

Lemma 5 (p. 80), in denominator-cleared form: Luce's identity (K+1){2[Q(ρ,σ)+Q(σ,τ)+Q(τ,ρ)] − 3} + K²[Q(ρ,σ)Q(σ,τ)Q(τ,ρ) − Q(ρ,τ)Q(τ,σ)Q(σ,ρ)] = 0, K = P(a,b)/P(b,a) − 1, multiplied through by P(b,a)². From Axiom 2 and Theorem 2 for the gamble triple {aρb, aσb, aτb}, whose pairwise discrimination is imperfect whenever P(a,b) ∉ {0, 1}.

theorem Luce1959.DecomposablePreference.eventPref_trans {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} (hnd : dp.Nondegenerate) {ρ σ τ : E} (h1 : dp.EventPref ρ σ) (h2 : dp.EventPref σ τ) : dp.EventPref ρ τ

Lemma 6 (p. 80): ≿ is transitive (with gt_half_or_of_not_eventIndiff totality, a weak ordering of E).

theorem Luce1959.DecomposablePreference.eventIndiff_trans {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} (hnd : dp.Nondegenerate) {ρ σ τ : E} (h1 : dp.EventIndiff ρ σ) (h2 : dp.EventIndiff σ τ) : dp.EventIndiff ρ τ

∼ is transitive: with eventIndiff_refl and EventIndiff.symm, an equivalence relation (the content of Theorem 10's first clause).

theorem Luce1959.DecomposablePreference.lemma7 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} (hnd : dp.Nondegenerate) {ρ σ τ : E} (hρσ : ρ ≠ σ) (hστ : σ ≠ τ) (hρτ : ρ ≠ τ) (himp : dp.Q.ImperfectOn {ρ, σ, τ}) : dp.EventIndiff ρ σ ∨ dp.EventIndiff σ τ ∨ dp.EventIndiff ρ τ

Lemma 7 (p. 81): three distinct events, pairwise imperfectly discriminated, cannot lie in three distinct ∼-classes.

theorem Luce1959.DecomposablePreference.atMostThreeClasses {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} (hnd : dp.Nondegenerate) (ρ σ τ ω : E) : dp.EventIndiff ρ σ ∨ dp.EventIndiff ρ τ ∨ dp.EventIndiff ρ ω ∨ dp.EventIndiff σ τ ∨ dp.EventIndiff σ ω ∨ dp.EventIndiff τ ω

Lemma 8 (p. 81) / the partition clause of Theorem 10 (p. 80): in a nondegenerate decomposable preference structure, ∼ partitions the events into at most three classes — among any four events, two are subjectively equi-likely.

theorem Luce1959.DecomposablePreference.theorem11 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} (hnd : dp.Nondegenerate) {ρ ρ' σ σ' : E} (h1 : dp.EventIndiff ρ ρ') (h2 : dp.EventIndiff σ σ') (hρσ : ρ ≠ σ) (hρ'σ' : ρ' ≠ σ') : dp.Q.binary ρ σ = dp.Q.binary ρ' σ'

Theorem 11 (p. 82): Q is constant across ∼-classes — if ρ ∼ ρ' and σ ∼ σ' then Q(ρ, σ) = Q(ρ', σ'). Both comparisons must be genuine pairs: at ρ' = σ' the total-ChoiceFn diagonal Q(ρ', ρ') = 1 breaks the unguarded claim, which Luce's P(x, x) = ½ convention (p. 5) hides.

theorem Luce1959.DecomposablePreference.theorem13 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {a b c d : A} {ρ σ : E} (hab : a ≠ b) (hcd : c ≠ d) (ha1 : dp.alt a b = 1) (hc1 : dp.alt c d = 1) (himp : dp.P.ImperfectOn {Sum.inl { win := a, event := ρ, lose := b }, Sum.inl { win := a, event := σ, lose := b }, Sum.inl { win := c, event := ρ, lose := d }, Sum.inl { win := c, event := σ, lose := d }}) : dp.gam { win := a, event := ρ, lose := b } { win := c, event := ρ, lose := d } = dp.gam { win := a, event := σ, lose := b } { win := c, event := σ, lose := d }

Theorem 13 (p. 86): if P(a,b) = P(c,d) = 1 and "all pairwise discriminations in the set T = {aρb, aσb, cρd, cσd} are imperfect", then P(aρb, cρd) = P(aσb, cσd) — the step-function prediction of §3.D. The local ratio scale of Luce's proof is supplied by Theorem 3 (ChoiceFn.HasChoiceAxiom.binaryRatioScaleOn).

def Luce1959.DecomposablePreference.Complementation {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) : Prop

Axiom 3 (p. 83): "P(aρb, x) = P(bρ̄a, x), where ρ̄ denotes the complement of ρ" — aρb and bρ̄a are the same prospect relabeled. The two guards exclude x ∈ {aρb, bρ̄a}: for Luce those instances are degenerate singleton choices, and over a total ChoiceFn the unguarded axiom is unsatisfiable (complementation_unguarded_false).

Equations

• One or more equations did not get rendered due to their size.

theorem Luce1959.DecomposablePreference.complementation_unguarded_false {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] [Nontrivial A] (dp : DecomposablePreference A E) (h : ∀ (a b : A) (ρ : E) (x : Alternative A E), dp.P.binary (Sum.inl { win := a, event := ρ, lose := b }) x = dp.P.binary (Sum.inl { win := b, event := ρᶜ, lose := a }) x) : False

Without its guards, Axiom 3 is unsatisfiable for a total choice function: x := bρ̄a forces P(aρb, bρ̄a) = 1, and symmetrically P(bρ̄a, aρb) = 1, contradicting binary complementarity.

def Luce1959.DecomposablePreference.NontrivialPreference {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) : Prop

Axiom 4 (p. 83): some pair of alternatives and some pair of events are discriminated away from ½. Distinctness is explicit: Luce's P(a*, b*) presupposes a genuine pair (P(a, a) = 1 ≠ ½ would satisfy the inequality degenerately and break the determinant step of Lemma 9).

Equations

• dp.NontrivialPreference = ((∃ (a : A) (b : A), a ≠ b ∧ dp.alt a b ≠ 1 / 2) ∧ ∃ (ρ : E) (σ : E), ρ ≠ σ ∧ dp.Q.binary ρ σ ≠ 1 / 2)

theorem Luce1959.DecomposablePreference.q_compl_compl {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) (ρ σ : E) : dp.Q.binary ρ σ = dp.Q.binary σᶜ ρᶜ

Lemma 9 (p. 84): under Axioms 3–4, Q(ρ, σ) = Q(σ̄, ρ̄).

theorem Luce1959.DecomposablePreference.v_mul_v_compl_const {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] {v : E → ℝ} (hv : dp.Q.BinaryRatioScaleOn Set.univ v) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) (ρ σ : E) : v ρ * v ρᶜ = v σ * v σᶜ

Under a global binary ratio scale for Q, Lemma 9 pins v(ρ)·v(ρ̄) to a constant — the source of the φ(ρ)φ(ρ̄) = constant clause of the §3.D.3 decomposition (p. 89).

def Luce1959.DecomposablePreference.Neutral {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) (ρ : E) : Prop

An event indifferent to its own complement: membership in Luce's class C(½) (Lemma 11, p. 85).

Equations

• dp.Neutral ρ = (dp.Q.binary ρ ρᶜ = 1 / 2)

def Luce1959.DecomposablePreference.Favorable {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) (ρ : E) : Prop

An event deemed more likely than its complement: Luce's class C(1).

Equations

• dp.Favorable ρ = (1 / 2 < dp.Q.binary ρ ρᶜ)

def Luce1959.DecomposablePreference.Unfavorable {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) (ρ : E) : Prop

An event deemed less likely than its complement: Luce's class C(0).

Equations

• dp.Unfavorable ρ = (dp.Q.binary ρ ρᶜ < 1 / 2)

theorem Luce1959.DecomposablePreference.unfavorable_or_neutral_or_favorable {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) (ρ : E) : dp.Unfavorable ρ ∨ dp.Neutral ρ ∨ dp.Favorable ρ

Every event is unfavorable, neutral, or favorable.

theorem Luce1959.DecomposablePreference.neutral_compl_iff {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (ρ : E) : dp.Neutral ρᶜ ↔ dp.Neutral ρ

An event is neutral iff its complement is.

theorem Luce1959.DecomposablePreference.favorable_iff_unfavorable_compl {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (ρ : E) : dp.Favorable ρ ↔ dp.Unfavorable ρᶜ

An event is favorable iff its complement is unfavorable.

theorem Luce1959.DecomposablePreference.neutral_indifferent {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (hnd : dp.Nondegenerate) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) {ρ σ : E} (hρ : dp.Neutral ρ) (hσ : dp.Neutral σ) (hρσ : ρ ≠ σ) : dp.Q.binary ρ σ = 1 / 2

Two distinct neutral events are indifferent — the first clause of Lemma 10 (p. 84), "if ρ ∼ ρ̄ and σ ∼ σ̄, then ρ ∼ σ", via Theorem 11 and Lemma 9. Distinctness is required: Q(ρ, ρ) = 1.

theorem Luce1959.DecomposablePreference.favorable_gt_unfavorable {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] {v : E → ℝ} (hv : dp.Q.BinaryRatioScaleOn Set.univ v) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) {ρ σ : E} (hρ : dp.Favorable ρ) (hσ : dp.Unfavorable σ) : 1 / 2 < dp.Q.binary ρ σ

Favorable events are preferred to unfavorable ones: the between-class ordering C(1) > C(0) of the three-class picture (§3.C.2, p. 85), under a global ratio scale for Q.

theorem Luce1959.DecomposablePreference.theorem14 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (ax3 : dp.Complementation) {a b c d : A} {ρ σ : E} {v : Alternative A E → ℝ} (hab : a ≠ b) (hcd : c ≠ d) (hρσ : ρ ≠ σ) (hacbd : ¬(a = c ∧ b = d)) (ha1 : dp.alt a b = 1) (hd1 : dp.alt d c = 1) (hv : dp.P.BinaryRatioScaleOn {Sum.inl { win := a, event := ρ, lose := b }, Sum.inl { win := a, event := σ, lose := b }, Sum.inl { win := c, event := ρ, lose := d }, Sum.inl { win := c, event := σ, lose := d }, Sum.inl { win := d, event := ρᶜ, lose := c }, Sum.inl { win := d, event := σᶜ, lose := c }} v) : v (Sum.inl { win := a, event := ρ, lose := b }) * v (Sum.inl { win := d, event := ρᶜ, lose := c }) = v (Sum.inl { win := a, event := σ, lose := b }) * v (Sum.inl { win := d, event := σᶜ, lose := c })

Theorem 14 (p. 89): with Axiom 3, P(a,b) = P(d,c) = 1, and a local ratio scale over the six gambles involved, the scale satisfies v(aρb)·v(dρ̄c) = v(aσb)·v(dσ̄c). Together with Theorem 13 this is what "suggests that v may be of the form v(aρb) = w(a,b)·φ(ρ)" (§3.D.3).

def Luce1959.DecomposablePreference.HasNeutralEvent {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) : Prop

Axiom 5 (p. 84): some event is subjectively as likely as its complement.

Equations

• dp.HasNeutralEvent = ∃ (ε : E), dp.Q.binary ε εᶜ = 1 / 2

theorem Luce1959.DecomposablePreference.neutral_of_indiff_neutral {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (hnd : dp.Nondegenerate) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) {ρ σ : E} (hρ : dp.Neutral ρ) (h : dp.EventIndiff σ ρ) : dp.Neutral σ

The second clause of Lemma 10 (p. 84): anything equi-likely with a neutral event is itself neutral — C(½) is exactly the neutral class.

theorem Luce1959.DecomposablePreference.atLeastThreeClasses {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (hnd : dp.Nondegenerate) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) (ax5 : dp.HasNeutralEvent) : ∃ (ε : E) (ρ : E), ¬dp.EventIndiff ε ρ ∧ ¬dp.EventIndiff ε ρᶜ ∧ ¬dp.EventIndiff ρ ρᶜ

Lemma 11 (p. 85): with Axioms 3–5 and nondegeneracy there are at least three classes — a neutral event, a non-neutral event, and its complement are pairwise non-equivalent.

theorem Luce1959.DecomposablePreference.theorem12 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (hnd : dp.Nondegenerate) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) (ax5 : dp.HasNeutralEvent) : ∃ (ρ₁ : E) (ρ₂ : E) (ρ₃ : E), (¬dp.EventIndiff ρ₁ ρ₂ ∧ ¬dp.EventIndiff ρ₁ ρ₃ ∧ ¬dp.EventIndiff ρ₂ ρ₃) ∧ ∀ (σ : E), dp.EventIndiff σ ρ₁ ∨ dp.EventIndiff σ ρ₂ ∨ dp.EventIndiff σ ρ₃

Theorem 12 (p. 84): given Axioms 3–5 and a nondegenerately discriminated pair of alternatives, ∼ partitions the events into exactly three classes: three pairwise non-equivalent events to one of which every event is equivalent.

theorem Luce1959.DecomposablePreference.gam_of_factored {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {S : Set (Gamble A E)} {v : Alternative A E → ℝ} {w : A → A → ℝ} {φ : E → ℝ} (hv : dp.P.BinaryRatioScaleOn (Sum.inl '' S) v) (hφ : ∀ (τ : E), 0 < φ τ) (hfac : ∀ (x y : A) (τ : E), { win := x, event := τ, lose := y } ∈ S → v (Sum.inl { win := x, event := τ, lose := y }) = w x y * φ τ) {a b c d : A} {ρ : E} (h₁ : { win := a, event := ρ, lose := b } ∈ S) (h₂ : { win := c, event := ρ, lose := d } ∈ S) (hacbd : ¬(a = c ∧ b = d)) : dp.gam { win := a, event := ρ, lose := b } { win := c, event := ρ, lose := d } = w a b / (w a b + w c d)

The observable content of the §3.D.3 suggested factoring v(aρb) = w(a,b)·φ(ρ) (pp. 89–90): between gambles on the same event the event weight cancels, so binary choice follows the Luce rule on the outcome weights alone — "the step function described in theorem 13 can have only one step intermediate between 0 and 1" (p. 90). Luce offers the factoring as a hypothesis consistent with Theorems 13–14, not a theorem; accordingly it enters here as a hypothesis.