The Mathematics of Hidden-Set Decisions: Communication Constraints and Coverage Values

This working paper studies a one-shot finite Bayesian decision problem motivated by Mafia and Werewolf: an encoder observes a hidden subset of an R-element population, emits one of K symbols, and a decoder names one position, succeeding exactly when that position is hidden. For 1≤K≤R and any rational prior π, the optimal deterministic success probability is the weighted maximum-coverage value over subsets of at most K positions, attained by an explicit finite-choice encoder–decoder pair. This attainment is an exhaustive finite-choice existence result; we claim neither an efficient maximum-coverage algorithm nor an approximation ratio. Under the uniform prior on M-subsets, exact rational stochastic encoders and decoders cannot improve the closed-form value. The paper also characterizes decision-neutral deterministic records by a simple 1-design condition, proves deterministic data processing, and realizes the hit objective as an instance of g-vulnerability. Lean 4 machine-checks the finite chain using exact rational probabilities and explicit witnesses. Maximum coverage, finite decision rules, combinatorial designs, and quantitative information-flow principles are established theory; our contribution is their end-to-end machine-checked connection in one explicit model. After fixing a finite state, prior, message alphabet, and payoff, the formulation can also be reused in communication-constrained Bayesian decisions, finite information-leakage analyses, and combinatorial-design problems beyond Werewolf. The model does not derive a value for a full strategic Werewolf game or an agent-performance score.