The Mathematics of Mafia and Werewolf: Fixed-Schedule Random-Elimination Benchmarks

This working paper studies a two-type finite-population elimination process with a fixed periodic schedule, as a random-elimination benchmark for Mafia and Werewolf rather than an unrestricted communication-and-voting game. We formalize the process in Lean 4 and prove an exact order-dependent falling-factorial invariant for every fixed finite schedule, together with finite scaling certificates at the threshold scale \(Rd/r\). For the alternating day–night schedule, the classical Mafia/Werewolf benchmark is recovered as a machine-checked special case under explicitly matched transition and stopping conventions, with distinct odd- and even-population Gaussian limit profiles. We also establish finite protection certificates. The results do not claim values for unrestricted strategic play. A version-pinned audit identifies localized statement, model-connection, and approximation-boundary issues in retained prior sources without overturning their principal conclusions.