Appendix A — interior candidate crosses zero and one at the prior thresholds

Proved

HumanMachine.Alone.pbar_thresholds

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebrap2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1rational-inattention

For any information cost $\lambda>0$ and any real prior parameter $\mu$ , the interior algebraic expression $\bar p$ crosses the endpoints of the probability interval exactly at the thresholds of Theorem 1:

\bar p\ge 1\iff\mu\ge\overline\mu,\qquad \bar p\le 0\iff\mu\le\underline\mu.

These equivalences identify when the interior expression leaves $[0,1]$ and hence where the closed form switches cases.

Formalization Note The equivalences are algebraic and hold for every real $\mu$ ; the decision problem itself uses a probability prior.

Preamble

import Mathlib
import Definitions.Def_HumanMachine_Alone_model

Formal statement

namespace HumanMachine.Alone

theorem pbar_thresholds (lam : ℝ) (hlam : 0 < lam) :
    ∀ mu : ℝ, (1 ≤ pBar lam mu ↔ muHigh lam ≤ mu) ∧
      (pBar lam mu ≤ 0 ↔ mu ≤ muLow lam) := by sorry

end HumanMachine.Alone

Source

Boyacı, Canyakmaz & de Véricourt, Human and Machine: The Impact of Machine Input on Decision-Making Under Cognitive Limitations, ESMT Working Paper 20-02 (Nov. 30, 2020), p. 32 (PDF p. 33), proof of Theorem 1, threshold-crossing sentences.

Human review

Endorsed by Shuze Chen · Oct 15, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 15, 2026
Confirmed by the mission captain (proposal self-audit).

View graph