Luce's Utility Decomposition Theory (Chapter 3) @cite{luce-1959}

@cite{luce-1959} extends the choice axiom from simple alternatives to gambles — uncertain prospects of the form "get outcome a if event ρ occurs, otherwise get outcome b." The key result is a decomposition theorem: the subjective value of a gamble factors multiplicatively into a component that depends only on the outcomes and a component that depends only on the event.

Architecture

This module formalizes:

1. Gambles (§3.A): An outcome aρb means "receive a if event ρ, else b."
2. Decomposition Axiom (Axiom 2): When outcomes are fixed, choice between gambles depends only on the events.
3. Monotonicity Axiom (Axiom 3): Preferred outcome + preferred event → preferred gamble.
4. Luce ratio scales (§2a): The Luce choice axiom applied to event and gamble choice functions, providing ratio-scale representations Q(ρ,σ) = v(ρ)/(v(ρ)+v(σ)).
5. Three equivalence classes (Theorem 12): Under the Luce choice axiom, events classified as neutral relative to a reference are indifferent: Q(ρ,σ) = ½.
6. Scale decomposition (§3.D): v(aρb) = w(a,b) · φ(ρ) — gamble value factors into outcome value × event weight.
7. RSA bridge: RSA's additive utility structure utility = informativity - cost follows from Luce's decomposition in log-space.

structure Core.Event : Type

An event in a decision problem. Events are the uncertain conditions under which outcomes are determined.

• id : ℕ

@[implicit_reducible]

instance Core.instDecidableEqEvent : DecidableEq Event

Equations

• Core.instDecidableEqEvent = Core.instDecidableEqEvent.decEq

def Core.instDecidableEqEvent.decEq (x✝ x✝¹ : Event) : Decidable (x✝ = x✝¹)

Equations

• Core.instDecidableEqEvent.decEq { id := a } { id := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.instReprEvent : Repr Event

Equations

• Core.instReprEvent = { reprPrec := Core.instReprEvent.repr }

def Core.instReprEvent.repr : Event → ℕ → Std.Format

Equations

• Core.instReprEvent.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "id" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.id)).group) " }"

structure Core.Gamble (Outcome : Type u_1) : Type u_1

A gamble aρb: receive outcome a if event ρ occurs, else outcome b. (@cite{luce-1959}, §3.A)

• win : Outcome

  Outcome if event occurs

• event : Event

  The conditioning event

• lose : Outcome

  Outcome if event does not occur

@[implicit_reducible]

instance Core.instDecidableEqGamble {Outcome : Type u_1} [DecidableEq Outcome] : DecidableEq (Gamble Outcome)

Equations

• Core.instDecidableEqGamble g₁ g₂ = if h : g₁.win = g₂.win ∧ g₁.event = g₂.event ∧ g₁.lose = g₂.lose then isTrue ⋯ else isFalse ⋯

Choice functions for Luce Chapter 3

Following the deeper unification: there is ONE canonical ChoiceFn (in RationalAction.lean), with a binary view cf.binary x y := cf.prob {x, y} x. Luce Chapter 3's gamble/outcome/event choice functions are all ChoiceFn-typed; the type-specific names below are abbrevs as semantic markers. Binary-style theorems use cf.binary x y notation.

@[reducible, inline]

abbrev Core.GambleChoiceFn (Outcome : Type u_2) [DecidableEq Outcome] : Type u_2

A gamble choice function: cf.binary g₁ g₂ = cf.prob {g₁, g₂} g₁ is the probability of choosing gamble g₁ over g₂ (@cite{luce-1959}, §3.A).

Equations

• Core.GambleChoiceFn Outcome = Core.ChoiceFn (Core.Gamble Outcome)

@[reducible, inline]

abbrev Core.OutcomeChoiceFn (Outcome : Type u_2) [DecidableEq Outcome] : Type u_2

An outcome choice function: cf.binary a b is the probability of choosing outcome a over b. Used for the outcome-only component of decomposition.

Equations

• Core.OutcomeChoiceFn Outcome = Core.ChoiceFn Outcome

@[reducible, inline]

abbrev Core.EventChoiceFn : Type

An event choice function: Q.binary ρ σ is the probability of preferring event ρ over σ (extracted when outcomes are held fixed).

Equations

• Core.EventChoiceFn = Core.ChoiceFn Core.Event

structure Core.DecompositionAxiom {Outcome : Type u_1} [DecidableEq Outcome] (P : GambleChoiceFn Outcome) : Type

Decomposition Axiom (@cite{luce-1959}, Axiom 2): When comparing gambles with fixed outcomes (same a, same b), the choice probability depends only on the events.

P(aρb, aσb) = Q(ρ, σ) for some event choice function Q.

• eventChoice : EventChoiceFn

  The extracted event choice function

• decomp (a b : Outcome) (ρ σ : Event) : ChoiceFn.binary P { win := a, event := ρ, lose := b } { win := a, event := σ, lose := b } = ChoiceFn.binary self.eventChoice ρ σ

  Fixed outcomes ⟹ choice depends only on events

structure Core.MonotonicityAxiom {Outcome : Type u_1} [DecidableEq Outcome] (P : GambleChoiceFn Outcome) (outcomeChoice : OutcomeChoiceFn Outcome) (eventChoice : EventChoiceFn) : Prop

Monotonicity Axiom (@cite{luce-1959}, Axiom 3): If outcome a is preferred to b (P(a,b) ≥ ½) and event ρ is preferred to σ (Q(ρ,σ) ≥ ½), then gamble aρb is preferred to bσa.

This captures the intuition that a better outcome under a more favorable event should be preferred to a worse outcome under a less favorable event.

• mono (a b : Outcome) (ρ σ : Event) : ChoiceFn.binary outcomeChoice a b ≥ 1 / 2 → ChoiceFn.binary eventChoice ρ σ ≥ 1 / 2 → ChoiceFn.binary P { win := a, event := ρ, lose := b } { win := b, event := σ, lose := a } ≥ 1 / 2

structure Core.EventLuceScale (Q : EventChoiceFn) : Type

A Luce ratio scale for an event choice function: Q(ρ,σ) = v(ρ)/(v(ρ)+v(σ)) for some positive scoring function v. This is the event-level analog of the Luce choice rule from RationalAction.

• v : Event → ℝ
• v_pos (ρ : Event) : 0 < self.v ρ
• luce_rule (ρ σ : Event) : ChoiceFn.binary Q ρ σ = self.v ρ / (self.v ρ + self.v σ)

structure Core.GambleLuceScale {Outcome : Type u_1} [DecidableEq Outcome] (P : GambleChoiceFn Outcome) : Type u_1

A Luce ratio scale for a gamble choice function: P(g₁,g₂) = v(g₁)/(v(g₁)+v(g₂)) for some positive scoring function v. This is the gamble-level Luce choice axiom (@cite{luce-1959}, Chapter 1 applied to gamble alternatives).

• v : Gamble Outcome → ℝ
• v_pos (g : Gamble Outcome) : 0 < self.v g
• luce_rule (g₁ g₂ : Gamble Outcome) : ChoiceFn.binary P g₁ g₂ = self.v g₁ / (self.v g₁ + self.v g₂)

inductive Core.EventClass : Type

An event ρ is favorable relative to an outcome preference P(a,b) ≥ ½ if Q(ρ, σ₀) > ½ for the neutral event σ₀. Intuitively: ρ makes the preferred outcome more likely.

• favorable : EventClass
• neutral : EventClass
• unfavorable : EventClass

@[implicit_reducible]

instance Core.instDecidableEqEventClass : DecidableEq EventClass

Equations

• Core.instDecidableEqEventClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.instReprEventClass : Repr EventClass

Equations

• Core.instReprEventClass = { reprPrec := Core.instReprEventClass.repr }

def Core.instReprEventClass.repr : EventClass → ℕ → Std.Format

Equations

• Core.instReprEventClass.repr Core.EventClass.favorable prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.EventClass.favorable")).group prec✝
• Core.instReprEventClass.repr Core.EventClass.neutral prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.EventClass.neutral")).group prec✝
• Core.instReprEventClass.repr Core.EventClass.unfavorable prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.EventClass.unfavorable")).group prec✝

noncomputable def Core.classifyEvent (Q : EventChoiceFn) (ref ρ : Event) : EventClass

Classify an event based on its choice probability against a reference event. (@cite{luce-1959}, §3.C)

Equations

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

theorem Core.threeClasses (Q : EventChoiceFn) (hScale : EventLuceScale Q) (ref ρ σ : Event) (hρ : classifyEvent Q ref ρ = EventClass.neutral) (hσ : classifyEvent Q ref σ = EventClass.neutral) : ChoiceFn.binary Q ρ σ = 1 / 2

Neutral class indifference (@cite{luce-1959}, Theorem 12): Under the Luce choice axiom, events classified as neutral relative to a reference event are indifferent to each other: Q(ρ, σ) = ½.

If v(ρ) = v(ref) (neutral) and v(σ) = v(ref) (neutral), then v(ρ) = v(σ), hence Q(ρ,σ) = v(ρ)/(v(ρ)+v(σ)) = ½.

Note: For favorable and unfavorable events, same-class membership does NOT imply indifference — events within these classes can have different v-values and thus Q(ρ,σ) ≠ ½. See favorable_over_unfavorable for the between-class ordering.

theorem Core.favorable_over_unfavorable (Q : EventChoiceFn) (hScale : EventLuceScale Q) (ref ρ σ : Event) (hρ : classifyEvent Q ref ρ = EventClass.favorable) (hσ : classifyEvent Q ref σ = EventClass.unfavorable) : ChoiceFn.binary Q ρ σ > 1 / 2

Between-class ordering: favorable events are preferred over unfavorable events. If v(ρ) > v(ref) (favorable) and v(σ) < v(ref) (unfavorable), then v(ρ) > v(σ), hence Q(ρ,σ) > ½.

theorem Core.favorable_over_neutral (Q : EventChoiceFn) (hScale : EventLuceScale Q) (ref ρ σ : Event) (hρ : classifyEvent Q ref ρ = EventClass.favorable) (hσ : classifyEvent Q ref σ = EventClass.neutral) : ChoiceFn.binary Q ρ σ > 1 / 2

Between-class ordering: favorable events are preferred over neutral events.

structure Core.ScaleDecomposition (Outcome : Type u_2) : Type u_2

A gamble value function that factors into outcome value × event weight. (@cite{luce-1959}, §3.D)

v(aρb) = w(a,b) · φ(ρ) where:

• w(a,b) depends only on the outcomes
• φ(ρ) depends only on the event

• outcomeValue : Outcome → Outcome → ℝ

  Outcome value component

• eventWeight : Event → ℝ

  Event weight component

• outcomeValue_nonneg (a b : Outcome) : 0 ≤ self.outcomeValue a b

  Non-negativity

• eventWeight_nonneg (ρ : Event) : 0 ≤ self.eventWeight ρ

noncomputable def Core.ScaleDecomposition.gambleValue {Outcome : Type u_1} (sd : ScaleDecomposition Outcome) (g : Gamble Outcome) : ℝ

The gamble value under a scale decomposition.

Equations

• sd.gambleValue g = sd.outcomeValue g.win g.lose * sd.eventWeight g.event

theorem Core.scaleDecomposition {Outcome : Type u_1} [DecidableEq Outcome] (P : GambleChoiceFn Outcome) (hDecomp : DecompositionAxiom P) (hLuce : GambleLuceScale P) (ρ₀ : Event) (a₀ b₀ : Outcome) : ∃ (sd : ScaleDecomposition Outcome), ∀ (g₁ g₂ : Gamble Outcome), sd.gambleValue g₁ + sd.gambleValue g₂ > 0 → ChoiceFn.binary P g₁ g₂ = sd.gambleValue g₁ / (sd.gambleValue g₁ + sd.gambleValue g₂)

Scale decomposition theorem (@cite{luce-1959}, §3.D): Under the Luce choice axiom and the decomposition axiom, the choice probability for gambles can be represented as a Luce choice rule with scores that factor as v(aρb) = w(a,b) · φ(ρ).

The construction: fix a reference event ρ₀ and reference outcomes a₀, b₀.

• w(a,b) := v(a,ρ₀,b) (gamble value with reference event)
• φ(ρ) := v(a₀,ρ,b₀) / v(a₀,ρ₀,b₀) (event weight normalized by reference)

The decomposition axiom ensures that v(g)/v(g.win,ρ₀,g.lose) depends only on the event, so v(g) = w(g.win,g.lose) · φ(g.event).

RSA Bridge

Luce's decomposition theorem justifies the additive structure of RSA utility.

In RSA, the speaker's utility is: utility(u, w) = log P(w|u) - cost(u)

This additive structure in log-space corresponds to multiplicative structure in ratio-scale space: score(u, w) = exp(α · utility) = exp(α · log P(w|u)) · exp(-α · cost(u)) = informativity^α · exp(-α · cost)

Luce's decomposition v(aρb) = w(a,b) · φ(ρ) provides the axiomatic foundation:

• The "outcome" dimension corresponds to the communicative goal (informativity)
• The "event" dimension corresponds to the production process (cost)
• The multiplicative factoring is derived from IIA + monotonicity, not stipulated

structure Core.RSAUtilityDecomposition : Type

RSA utility as a Luce decomposition instance.

The speaker's score exp(α · (log P(w|u) - cost(u))) factors as:

• outcome component: P(w|u)^α (informativity)
• event component: exp(-α · cost(u)) (production ease)

This factoring means the Luce choice axiom guarantees that informativity and cost contribute independently to the speaker's choice, which is a substantive empirical prediction (not a modeling convenience).

• α : ℝ

  Rationality parameter

• informativity : ℝ

  Informativity: P(w|u) for each utterance-world pair

• cost : ℝ

  Cost of utterance

• informativity_nonneg : 0 ≤ self.informativity

  Informativity is a probability

• informativity_le_one : self.informativity ≤ 1

noncomputable def Core.RSAUtilityDecomposition.score (d : RSAUtilityDecomposition) : ℝ

RSA speaker score factors multiplicatively, following Luce decomposition.

Equations

• d.score = d.informativity ^ d.α * Real.exp (-d.α * d.cost)

theorem Core.rsa_utility_decomposition (d : RSAUtilityDecomposition) (hinfo_pos : 0 < d.informativity) : Real.log d.score = d.α * Real.log d.informativity - d.α * d.cost

The RSA utility decomposition: log(score) = α · log(informativity) - α · cost. This additive structure in log-space is what Luce's Chapter 3 derives from the decomposition axioms.