BToM-derived credence

The bridge from Bayesian Theory of Mind inference to an agent credence: the observer's estimate of an agent's credence in φ is the belief-marginal expectation of φ's truth value (BToMModel.beliefExpectation). This is the pragmatic grounding — reasoning about an interlocutor's mental state — that produces the credence the (semantic) epistemic-threshold predicates consume ([YZXW+25], [BJEST17]).

Main results

• btomCredence — credence as the BToM belief-marginal expectation.
• btomCredence_eq_world_expectation — under identity perception/belief, this collapses to the world-marginal expectation (the RSA-BToM bridge).

noncomputable def Core.btomCredence {F : Type u_1} [CommSemiring F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] (model : BToMModel F A P B D S M W) (eval : B → (W → Bool) → F) (a : A) (φ : W → Bool) : F

Agent credence derived from BToM belief-marginal inference.

Given a BToM model with belief type B and an evaluation function eval : B → (W → Bool) → F that computes how belief state b rates proposition φ, the observer estimates the agent's credence after observing action a:

Pr_obs(Agent, φ | a) = Σ_b P(b | a) · eval(b, φ)

This is BToMModel.beliefExpectation applied to fun b => eval b φ, grounding the abstract AgentCredence in concrete BToM inference.

When B = W and eval b φ = if φ b then 1 else 0 (the RSA-BToM bridge's perfect-knowledge assumption), this reduces to the L1 listener's expected truth-value under their world posterior.

Polymorphic in F so it composes with both ℚ-valued (exact computation) and ℝ-valued models.

Equations

• Core.btomCredence model eval a φ = model.beliefExpectation (fun (b : B) => eval b φ) a

theorem Core.identity_belief_eq_world_marginal {F : Type u_1} [CommSemiring F] {A : Type u_2} {D : Type u_3} {S : Type u_4} {M : Type u_5} {W : Type u_6} [DecidableEq W] [Fintype W] [Fintype D] [Fintype S] [Fintype M] (model : BToMModel F A W W D S M W) (h_percept : ∀ (w p : W), model.perceptModel w p = if p = w then 1 else 0) (h_belief : ∀ (p b : W), model.beliefModel p b = if b = p then 1 else 0) (a : A) (b : W) : model.beliefMarginal a b = model.worldMarginal a b

theorem Core.btomCredence_eq_world_expectation {F : Type u_1} [CommSemiring F] {A : Type u_2} {D : Type u_3} {S : Type u_4} {M : Type u_5} {W : Type u_6} [DecidableEq W] [Fintype W] [Fintype D] [Fintype S] [Fintype M] (model : BToMModel F A W W D S M W) (h_percept : ∀ (w p : W), model.perceptModel w p = if p = w then 1 else 0) (h_belief : ∀ (p b : W), model.beliefModel p b = if b = p then 1 else 0) (eval : W → (W → Bool) → F) (a : A) (φ : W → Bool) : btomCredence model eval a φ = ∑ w : W, model.worldMarginal a w * eval w φ

For identity-perception BToM models, btomCredence is the world-marginal-weighted evaluation of φ.

This connects the abstract btomCredence to concrete RSA inference: when the BToM model has identity perception/belief (as in the RSA-as-BToM bridge), computing agent credence via BToM belief marginals is the same as computing the L1 listener's expected truth-value.

btomCredence(model, eval, a, φ)
  = Σ_b beliefMarginal(a, b) · eval(b, φ)
  = Σ_w worldMarginal(a, w) · eval(w, φ)    [by identity_belief_eq_world_marginal]

The second line is exactly the L1 listener's posterior expectation (via L1_eq_btom_worldMarginal in RSA.Core.Config).