Harding, Gerstenberg, and Icard (2025): A Communication-First Account of Explanation

On the model of Harding, Gerstenberg and Icard an answer to "why FACT?" is a message in a Rational Speech Act game, after Frank and Goodman, whose literal meaning is actual causation and whose speaker is useful rather than informative, after Sumers and colleagues. The literal listener conditions a prior over causal situations on the message (2); the listener acts in a decision problem by the softmax of expected reward (3), RSA.policy; the speaker maximizes the reward of the listener's action, RSA.actionUtility (4), less the message's cost (6), speaker; the pragmatic listener is the posterior of the speaker at the prior (7); and the goodness of an explanation is the gain in expected reward over acting on the prior alone (8), goodness. When the listener's interests are unknown the decision problem is the manipulation game (Definition 2), whose reward for a variable is the probability over contexts that intervening on it changes FACT, manipulationReward. In the roof example (Example 2) citing the thatched roof and citing the drought are equally informative but not equally useful, since only the former bears on replacing a roof (Table 1), so at any rationality the listener replaces the roof more readily after the former, RoofReplacement.policy_replace_lt. In the late-meeting example (Example 3) citing the tardiness is worth giving although the listener already knows it: the speaker cites the birthday exactly in the conjunctive world, so the pragmatic listener infers from her not doing so that tardiness alone is the cause, and the goodness of the message is positive, LateMeeting.goodness_pos. In the milk example (Example 4) citing both culprits is worth more than citing one, but a sufficient cost difference makes the speaker prefer the shorter message, MilkTheft.speaker_prefers_short. The interpretation sets are the paper's, and for the late meeting they are derived from actual causation in the worlds' causal models.

Implementation notes

The agents are kept at finite rationality, where the paper takes the limit, and each claim is stated for the rationalities it needs. Actual causation is the witness form of the Halpern–Pearl definition, actualCause, which the paper leaves open to any extant account: some contingency, an intervention on other variables, under which the cause is but-for the effect in the actual context. A negative membership follows from the graph when no path runs from the cited variable to the fact. Priors are uniform, as in the examples.

TODO

• Table 4, the manipulation-game rewards of Example 2, from the four structural models and a product prior over the contexts; the roof and milk interpretation sets from actual causation.

References

• [HGI25]
• [HP05]
• [SHGH24]
• [FG12]

The communication game, section 3

noncomputable def HardingGerstenbergIcard2025.speakerScore {W : Type u_1} {M : Type u_2} {A : Type u_3} [MeasurableSpace M] [Fintype A] [MeasurableSpace A] (β : ℝ) (cost : M → ℝ) (π : ProbabilityTheory.Kernel M A) (R : A → W → ℝ) (w : W) (m : M) : EReal

The speaker scores a message by rationality times utility, less cost.

Equations

• HardingGerstenbergIcard2025.speakerScore β cost π R w m = ↑(β * RSA.actionUtility π R m w - cost m)

noncomputable def HardingGerstenbergIcard2025.speaker {W : Type u_1} {M : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype M] [MeasurableSpace M] [Fintype A] [MeasurableSpace A] (β : ℝ) (cost : M → ℝ) (π : ProbabilityTheory.Kernel M A) (R : A → W → ℝ) : ProbabilityTheory.Kernel W M

The speaker (6) is the softmax of utility less cost at rationality β.

Equations

• HardingGerstenbergIcard2025.speaker β cost π R = ProbabilityTheory.Kernel.softmax (HardingGerstenbergIcard2025.speakerScore β cost π R)

noncomputable def HardingGerstenbergIcard2025.goodness {W : Type u_1} {M : Type u_2} {A : Type u_3} [MeasurableSpace M] [Fintype A] [MeasurableSpace A] (πL πPrior : ProbabilityTheory.Kernel M A) (R : A → W → ℝ) (m : M) (w : W) : ℝ

The goodness (8) of a message at a world is the listener's expected reward after the message less what acting on the prior alone would have earned.

Equations

• HardingGerstenbergIcard2025.goodness πL πPrior R m w = RSA.actionUtility πL R m w - RSA.actionUtility πPrior R m w

instance HardingGerstenbergIcard2025.instIsFiniteKernelSpeaker {W : Type u_1} {M : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype M] [MeasurableSpace M] [Fintype A] [MeasurableSpace A] (β : ℝ) (R : A → W → ℝ) (cost : M → ℝ) (π : ProbabilityTheory.Kernel M A) : ProbabilityTheory.IsFiniteKernel (speaker β cost π R)

instance HardingGerstenbergIcard2025.instIsMarkovKernelSpeakerOfNonempty {W : Type u_1} {M : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype M] [MeasurableSpace M] [Fintype A] [MeasurableSpace A] (β : ℝ) (R : A → W → ℝ) (cost : M → ℝ) (π : ProbabilityTheory.Kernel M A) [Nonempty M] : ProbabilityTheory.IsMarkovKernel (speaker β cost π R)

theorem HardingGerstenbergIcard2025.speaker_real_lt_iff {W : Type u_1} {M : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype M] [MeasurableSpace M] [DiscreteMeasurableSpace M] [Fintype A] [MeasurableSpace A] {β : ℝ} (R : A → W → ℝ) (cost : M → ℝ) (π : ProbabilityTheory.Kernel M A) {m m' : M} {w : W} : ((speaker β cost π R) w).real {m} < ((speaker β cost π R) w).real {m'} ↔ β * RSA.actionUtility π R m w - cost m < β * RSA.actionUtility π R m' w - cost m'

Row preference of the speaker is comparison of utility less cost.

theorem HardingGerstenbergIcard2025.speaker_real_of_pair {W : Type u_1} {M : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype M] [MeasurableSpace M] [DiscreteMeasurableSpace M] [Fintype A] [MeasurableSpace A] {β : ℝ} (R : A → W → ℝ) (cost : M → ℝ) (π : ProbabilityTheory.Kernel M A) {m m' : M} {w : W} (hmm' : m ≠ m') (hall : ∀ (c : M), c = m ∨ c = m') : ((speaker β cost π R) w).real {m} = (β * (RSA.actionUtility π R m w - RSA.actionUtility π R m' w) - (cost m - cost m')).sigmoid

With two messages, the speaker's share of one is the logistic function of the scaled difference in utility less the difference in cost.

The manipulation game, Definition 2

noncomputable def HardingGerstenbergIcard2025.manipulationReward {U : Type u_1} {V : Type u_2} [DecidableEq V] [Fintype U] (P : U → ℝ) (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (X fact : V) : ℝ

The reward of intervening on X in a model (Definition 2) is the probability, over contexts drawn with weights P, that intervening on X changes FACT.

Equations

• HardingGerstenbergIcard2025.manipulationReward P M X fact = ∑ u : U, P u * if M.solve (Function.update ⊥ X ↑true) u fact ≠ M.solve (Function.update ⊥ X ↑false) u fact then 1 else 0

Actual causation, the literal meaning of "because"

def HardingGerstenbergIcard2025.actualCause {U : Type u_1} {V : Type u_2} [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (u : U) (cause effect : V) : Prop

In the context u, cause is an actual cause of effect in witness form when both hold and, under some contingency I intervening on other variables, the cause is but-for the effect. This is [HP05]'s definition without the restriction on contingencies that the paper leaves to any extant account.

Equations

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

Example 3: the late meeting

inductive HardingGerstenbergIcard2025.LateMeeting.V : Type

The endogenous variables are Bob's tardiness, his forgetting the birthday, and Charlie's crossness.

• T : V
• B : V
• C : V

@[instance_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instDecidableEqV : DecidableEq V

Equations

• HardingGerstenbergIcard2025.LateMeeting.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instFintypeV : Fintype V

Equations

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

@[instance_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instReprV : Repr V

Equations

• HardingGerstenbergIcard2025.LateMeeting.instReprV = { reprPrec := HardingGerstenbergIcard2025.LateMeeting.instReprV.repr }

def HardingGerstenbergIcard2025.LateMeeting.instReprV.repr : V → ℕ → Std.Format

Equations

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

def HardingGerstenbergIcard2025.LateMeeting.edgesT : Finset (V × V)

Tardiness alone bears on crossness.

Equations

• HardingGerstenbergIcard2025.LateMeeting.edgesT = {(HardingGerstenbergIcard2025.LateMeeting.V.T, HardingGerstenbergIcard2025.LateMeeting.V.C)}

def HardingGerstenbergIcard2025.LateMeeting.edgesConj : Finset (V × V)

Tardiness and the forgotten birthday both bear on crossness.

Equations

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

structure HardingGerstenbergIcard2025.LateMeeting.Context : Type

The context settles whether Bob was late and whether he forgot the birthday.

• T : Bool
• B : Bool

def HardingGerstenbergIcard2025.LateMeeting.semT : CausalModel Context V fun (x : V) => Bool

The model in which tardiness alone causes crossness.

Equations

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

def HardingGerstenbergIcard2025.LateMeeting.semConj : CausalModel Context V fun (x : V) => Bool

The conjunctive model, in which both are needed.

Equations

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

@[instance_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instDecidableRelVAdjGraphContextBoolSemT : DecidableRel semT.graph.Adj

Equations

• HardingGerstenbergIcard2025.LateMeeting.instDecidableRelVAdjGraphContextBoolSemT w v = HardingGerstenbergIcard2025.LateMeeting.instDecidableRelVAdjGraphContextBoolSemT._aux_1 w v

@[instance_reducible]

instance HardingGerstenbergIcard2025.LateMeeting.instDecidableRelVAdjGraphContextBoolSemConj : DecidableRel semConj.graph.Adj

Equations

• HardingGerstenbergIcard2025.LateMeeting.instDecidableRelVAdjGraphContextBoolSemConj w v = HardingGerstenbergIcard2025.LateMeeting.instDecidableRelVAdjGraphContextBoolSemConj._aux_1 w v

instance HardingGerstenbergIcard2025.LateMeeting.instIsAcyclicContextVBoolSemT : semT.IsAcyclic

instance HardingGerstenbergIcard2025.LateMeeting.instIsAcyclicContextVBoolSemConj : semConj.IsAcyclic

def HardingGerstenbergIcard2025.LateMeeting.context : Context

In the context Bob knows, he was late and forgot the birthday.

Equations

• HardingGerstenbergIcard2025.LateMeeting.context = { T := true, B := true }

theorem HardingGerstenbergIcard2025.LateMeeting.actualCause_T_semT : actualCause semT context V.T V.C

"Because T" is true in both worlds and "because B" in the conjunctive world. These are the interpretation sets of Example 3, derived from actual causation with the empty contingency.

theorem HardingGerstenbergIcard2025.LateMeeting.actualCause_T_semConj : actualCause semConj context V.T V.C

theorem HardingGerstenbergIcard2025.LateMeeting.actualCause_B_semConj : actualCause semConj context V.B V.C

theorem HardingGerstenbergIcard2025.LateMeeting.not_actualCause_B_semT : ¬actualCause semT context V.B V.C

"Because B" is false in the tardiness-only world, the negative membership of Example 3, since no path runs from the birthday to crossness, so under no contingency is it but-for crossness.

@[reducible, inline]

abbrev HardingGerstenbergIcard2025.LateMeeting.World : Type

The worlds are the tardiness-only model 0 and the conjunctive model 1.

Equations

• HardingGerstenbergIcard2025.LateMeeting.World = Fin 2

@[reducible, inline]

abbrev HardingGerstenbergIcard2025.LateMeeting.Msg : Type

The messages are "because T", 0, and "because B", 1.

Equations

• HardingGerstenbergIcard2025.LateMeeting.Msg = Fin 2

@[reducible, inline]

abbrev HardingGerstenbergIcard2025.LateMeeting.Act : Type

The actions of Table 3 are to apologize for the tardiness alone, 0, or for both, 1.

Equations

• HardingGerstenbergIcard2025.LateMeeting.Act = Fin 2

def HardingGerstenbergIcard2025.LateMeeting.sem : Msg → Finset World

The interpretation sets (Example 3).

Equations

• HardingGerstenbergIcard2025.LateMeeting.sem = ![{0, 1}, {1}]

def HardingGerstenbergIcard2025.LateMeeting.reward : Act → World → ℝ

In Table 3, apologizing for what is the cause earns 1, and otherwise −1.

Equations

• HardingGerstenbergIcard2025.LateMeeting.reward a w = if a = w then 1 else -1

@[reducible, inline]

noncomputable abbrev HardingGerstenbergIcard2025.LateMeeting.μ : MeasureTheory.Measure World

The uniform prior over the worlds.

Equations

• HardingGerstenbergIcard2025.LateMeeting.μ = ProbabilityTheory.uniformOn Set.univ

@[reducible, inline]

noncomputable abbrev HardingGerstenbergIcard2025.LateMeeting.L0 : ProbabilityTheory.Kernel Msg World

The literal listener (2) conditions the uniform prior on the interpretation set.

Equations

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

@[reducible, inline]

noncomputable abbrev HardingGerstenbergIcard2025.LateMeeting.prior : ProbabilityTheory.Kernel Msg World

The prior as a listener who has heard nothing.

Equations

• HardingGerstenbergIcard2025.LateMeeting.prior = ProbabilityTheory.Kernel.const HardingGerstenbergIcard2025.LateMeeting.Msg HardingGerstenbergIcard2025.LateMeeting.μ

theorem HardingGerstenbergIcard2025.LateMeeting.expectedReward_L0 (a : Act) : RSA.expectedReward L0 reward 0 a = 0 ∧ RSA.expectedReward L0 reward 1 a = if a = 1 then 1 else -1

theorem HardingGerstenbergIcard2025.LateMeeting.expectedReward_prior (m : Msg) (a : Act) : RSA.expectedReward prior reward m a = 0

theorem HardingGerstenbergIcard2025.LateMeeting.policy_L0_both {βL : ℝ} : ((RSA.policy βL L0 reward) 1).real {1} = (2 * βL).sigmoid ∧ ((RSA.policy βL L0 reward) 0).real {1} = 1 / 2

After "because B" the listener apologizes for both with a share above one half, and after "because T" with exactly one half.

theorem HardingGerstenbergIcard2025.LateMeeting.policy_prior_half {βL : ℝ} (m : Msg) : ((RSA.policy βL prior reward) m).real {1} = 1 / 2

theorem HardingGerstenbergIcard2025.LateMeeting.utility_L0 {βL : ℝ} : RSA.actionUtility (RSA.policy βL L0 reward) reward 0 0 = 0 ∧ RSA.actionUtility (RSA.policy βL L0 reward) reward 0 1 = 0 ∧ RSA.actionUtility (RSA.policy βL L0 reward) reward 1 0 = 1 - 2 * (2 * βL).sigmoid ∧ RSA.actionUtility (RSA.policy βL L0 reward) reward 1 1 = 2 * (2 * βL).sigmoid - 1

By the speaker's utilities (4), "because T" is worth nothing in either world, and "because B" less than nothing in the tardiness-only world and more in the conjunctive one.

theorem HardingGerstenbergIcard2025.LateMeeting.half_lt_sigmoid {βL : ℝ} (hβ : 0 < βL) : 1 / 2 < (2 * βL).sigmoid

theorem HardingGerstenbergIcard2025.LateMeeting.speaker_cites_B_iff {βL βS : ℝ} (hβL : 0 < βL) (hβS : 0 < βS) (c : ℝ) : ((speaker βS (fun (x : Msg) => c) (RSA.policy βL L0 reward) reward) 0).real {1} < ((speaker βS (fun (x : Msg) => c) (RSA.policy βL L0 reward) reward) 0).real {0} ∧ ((speaker βS (fun (x : Msg) => c) (RSA.policy βL L0 reward) reward) 1).real {0} < ((speaker βS (fun (x : Msg) => c) (RSA.policy βL L0 reward) reward) 1).real {1}

The speaker cites the birthday exactly in the conjunctive world (equal costs).

theorem HardingGerstenbergIcard2025.LateMeeting.μ_singleton (w : World) : μ {w} ≠ 0 ∧ μ.real {w} = 1 / 2

noncomputable def HardingGerstenbergIcard2025.LateMeeting.S (βL βS c : ℝ) : ProbabilityTheory.Kernel World Msg

The speaker of Example 3 at equal costs c.

Equations

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

instance HardingGerstenbergIcard2025.LateMeeting.instIsFiniteKernelWorldMsgS (βL βS c : ℝ) : ProbabilityTheory.IsFiniteKernel (S βL βS c)

instance HardingGerstenbergIcard2025.LateMeeting.instIsMarkovKernelWorldMsgS (βL βS c : ℝ) : ProbabilityTheory.IsMarkovKernel (S βL βS c)

theorem HardingGerstenbergIcard2025.LateMeeting.S_apply_ne_zero (βL βS c : ℝ) (w : World) (m : Msg) : ((S βL βS c) w) {m} ≠ 0

theorem HardingGerstenbergIcard2025.LateMeeting.comp_S_ne_zero (βL βS c : ℝ) : (μ.bind ⇑(S βL βS c)) {0} ≠ 0

theorem HardingGerstenbergIcard2025.LateMeeting.S_real_lt {βL βS : ℝ} (hβL : 0 < βL) (hβS : 0 < βS) (c : ℝ) : ((S βL βS c) 1).real {0} < ((S βL βS c) 0).real {0}

"Because T" is likelier from the tardiness-only world than from the conjunctive one.

noncomputable def HardingGerstenbergIcard2025.LateMeeting.PL (βL βS c : ℝ) : ProbabilityTheory.Kernel Msg World

The pragmatic listener (7).

Equations

• HardingGerstenbergIcard2025.LateMeeting.PL βL βS c = RSA.listener HardingGerstenbergIcard2025.LateMeeting.μ ⇑(HardingGerstenbergIcard2025.LateMeeting.S βL βS c)

instance HardingGerstenbergIcard2025.LateMeeting.instIsMarkovKernelMsgWorldPL (βL βS c : ℝ) : ProbabilityTheory.IsMarkovKernel (PL βL βS c)

theorem HardingGerstenbergIcard2025.LateMeeting.pragmatic_T {βL βS : ℝ} (hβL : 0 < βL) (hβS : 0 < βS) (c : ℝ) : μ.real {0} < ((PL βL βS c) 0).real {0}

The pragmatic listener hearing "because T" raises the tardiness-only world above its prior, since the speaker would have cited the birthday in the conjunctive world.

theorem HardingGerstenbergIcard2025.LateMeeting.goodness_pos {βL βS : ℝ} (hβL : 0 < βL) (hβS : 0 < βS) (c : ℝ) : 0 < goodness (RSA.policy βL (PL βL βS c) reward) (RSA.policy βL prior reward) reward 0 0

By goodness (8), citing the tardiness is worth giving, although Bob already knew it.

Example 2: the roof replacement

@[reducible, inline]

abbrev HardingGerstenbergIcard2025.RoofReplacement.World : Type

The worlds are the roof-only model 0, the drought-only model 1, the conjunctive 2 and the disjunctive 3, all at the context where the roof is thatched and there was a drought.

Equations

• HardingGerstenbergIcard2025.RoofReplacement.World = Fin 4

@[reducible, inline]

abbrev HardingGerstenbergIcard2025.RoofReplacement.Msg : Type

The messages are "because R", 0, and "because D", 1.

Equations

• HardingGerstenbergIcard2025.RoofReplacement.Msg = Fin 2

@[reducible, inline]

abbrev HardingGerstenbergIcard2025.RoofReplacement.Act : Type

The actions of Table 1 are to replace the roof, 0, or not, 1.

Equations

• HardingGerstenbergIcard2025.RoofReplacement.Act = Fin 2

def HardingGerstenbergIcard2025.RoofReplacement.sem : Msg → Finset World

The interpretation sets of Example 2.

Equations

• HardingGerstenbergIcard2025.RoofReplacement.sem = ![{0, 2, 3}, {1, 2, 3}]

def HardingGerstenbergIcard2025.RoofReplacement.reward : Act → World → ℝ

In Table 1, replacing earns 0 everywhere, and not replacing earns 1 in the drought-only world and −1 elsewhere.

Equations

• HardingGerstenbergIcard2025.RoofReplacement.reward a w = if a = 0 then 0 else if w = 1 then 1 else -1

@[reducible, inline]

noncomputable abbrev HardingGerstenbergIcard2025.RoofReplacement.L0 : ProbabilityTheory.Kernel Msg World

Equations

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

theorem HardingGerstenbergIcard2025.RoofReplacement.L0_conj_eq : (L0 0).real {2} = (L0 1).real {2}

The two messages are equally informative, in that the conjunctive world is as likely after either.

theorem HardingGerstenbergIcard2025.RoofReplacement.expectedReward_L0 : RSA.expectedReward L0 reward 0 0 = 0 ∧ RSA.expectedReward L0 reward 0 1 = -1 ∧ RSA.expectedReward L0 reward 1 0 = 0 ∧ RSA.expectedReward L0 reward 1 1 = -1 / 3

theorem HardingGerstenbergIcard2025.RoofReplacement.policy_replace_lt {βL : ℝ} (hβ : 0 < βL) : ((RSA.policy βL L0 reward) 1).real {0} < ((RSA.policy βL L0 reward) 0).real {0}

The two messages are not equally useful, since at any rationality the listener replaces the roof more readily after "because R" than after "because D".

Example 4: the milk theft

@[reducible, inline]

abbrev HardingGerstenbergIcard2025.MilkTheft.World : Type

The worlds are the contexts in which Charlie alone (0), Dana alone (1), or both (2) drank the milk, in the disjunctive model.

Equations

• HardingGerstenbergIcard2025.MilkTheft.World = Fin 3

@[reducible, inline]

abbrev HardingGerstenbergIcard2025.MilkTheft.Msg : Type

The messages are "because C", 0, "because D", 1, and "because C and D", 2.

Equations

• HardingGerstenbergIcard2025.MilkTheft.Msg = Fin 3

@[reducible, inline]

abbrev HardingGerstenbergIcard2025.MilkTheft.Act : Type

The actions of Table 5 are to confront Charlie (0), Dana (1), or both (2).

Equations

• HardingGerstenbergIcard2025.MilkTheft.Act = Fin 3

def HardingGerstenbergIcard2025.MilkTheft.sem : Msg → Finset World

The interpretation sets of Example 4.

Equations

• HardingGerstenbergIcard2025.MilkTheft.sem = ![{0, 2}, {1, 2}, {2}]

def HardingGerstenbergIcard2025.MilkTheft.reward : Act → World → ℝ

Table 5.

Equations

• HardingGerstenbergIcard2025.MilkTheft.reward = ![![1, -1, 0], ![-1, 1, 0], ![0, 0, 1]]

@[reducible, inline]

noncomputable abbrev HardingGerstenbergIcard2025.MilkTheft.L0 : ProbabilityTheory.Kernel Msg World

Equations

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

theorem HardingGerstenbergIcard2025.MilkTheft.expectedReward_L0_conj (a : Act) : RSA.expectedReward L0 reward 2 a = if a = 2 then 1 else 0

theorem HardingGerstenbergIcard2025.MilkTheft.expectedReward_L0_C : RSA.expectedReward L0 reward 0 0 = 1 / 2 ∧ RSA.expectedReward L0 reward 0 1 = -1 / 2 ∧ RSA.expectedReward L0 reward 0 2 = 1 / 2

theorem HardingGerstenbergIcard2025.MilkTheft.policy_L0 {βL : ℝ} (hβ : 0 < βL) : ((RSA.policy βL L0 reward) 2).real {0} < ((RSA.policy βL L0 reward) 2).real {2} ∧ ¬((RSA.policy βL L0 reward) 0).real {0} < ((RSA.policy βL L0 reward) 0).real {2}

After "because C and D" confronting both is the strictly preferred action; after "because C" it is tied with confronting Charlie.

theorem HardingGerstenbergIcard2025.MilkTheft.speaker_prefers_short {βL βS : ℝ} (cost : Msg → ℝ) (h : βS * (RSA.actionUtility (RSA.policy βL L0 reward) reward 2 2 - RSA.actionUtility (RSA.policy βL L0 reward) reward 0 2) < cost 2 - cost 0) : ((speaker βS cost (RSA.policy βL L0 reward) reward) 2).real {2} < ((speaker βS cost (RSA.policy βL L0 reward) reward) 2).real {0}

With a sufficient cost difference the speaker prefers the shorter message although it is less useful, the redundancy trade-off of section 4.4.1.