Optimal Play in Caverna
A formal proof that the furnishing rush strategy is the unique weakly
dominant pure strategy in 2-player Caverna (the board game by Uwe Rosenberg),
verified in Lean 4 with
Mathlib.
Core Theorem (Weak Dominance).
For all opponents and all alternative strategies, the furnishing rush payoff
is at least as large, and strictly larger for at least one opponent. The unique
pure Nash equilibrium is the furnishing rush mirror match.
The formalization is complete