OpenGame.lean

View source on GitHub

OpenGame

An open game is a lens-like object with five type parameters: strategy (St), observation (X), action (Y), result (R), and coresult (S). Three operations: play (forward pass), coplay (backward pass), and bestResponse (equilibrium condition).

structure OpenGame (St X Y R S : Type*) where
  play : St → X → Y
  coplay : St → X → R → S
  bestResponse : X → (Y → R) → St → Prop

Ghani, Hedges, Winschel & Zahn (2018), Definition 2.1. arXiv: 1603.04641

OpenGame.seq / OpenGame.par

Sequential composition: game G plays first, game H plays using G's output. The backward channel threads results back through both games. Parallel composition: games G and H play simultaneously on independent inputs (monoidal product).

def OpenGame.seq (G : OpenGame St₁ X Y S T)
    (H : OpenGame St₂ Y Z R S) :
    OpenGame (St₁ × St₂) X Z R T

def OpenGame.par (G : OpenGame St₁ X₁ Y₁ R₁ S₁)
    (H : OpenGame St₂ X₂ Y₂ R₂ S₂) :
    OpenGame (St₁ × St₂) (X₁ × X₂) (Y₁ × Y₂) (R₁ × R₂) (S₁ × S₂)

vcgOpenGame

The VCG auction as an open game. Strategy is the full auction state. Observation is a query point. Action is the winning advertiser. Note: bestResponse ignores the continuation argument k and directly encodes a no-profitable-deviation condition at the current auction state. This is nonstandard — in typical open games, bestResponse depends on the continuation. Here the condition is continuation-independent, which makes it stronger than standard Nash (closer to dominant-strategy behavior). The actual DSIC theorem with its truthfulness hypothesis lives in Strategyproof.lean.

def vcgOpenGame : OpenGame (Auction ι E) E ι ℝ ℝ where
  play := fun auc x => winner auc x
  coplay := fun _auc _x r => r
  bestResponse := fun x _k auc =>
    ∀ (i : ι) (r' : Report E),
      playerUtility auc i x ≥
        playerUtility (auc.withReport i r') i x

composed_equilibria_decompose

Hedges' Theorem 4.3: Nash equilibria of sequentially composed games decompose into component equilibria. A strategy profile is Nash for G.seq H iff the component strategies are Nash for their respective games with appropriately threaded continuations.

theorem composed_equilibria_decompose ... :
    (G.seq H).isNashEquilibrium x k (s₁, s₂) ↔
    (G.bestResponse x ... s₁ ∧ H.bestResponse ... k s₂)

; Hedges Thm 4.3: equilibria decompose

; Game G: bid truthfully (value = 3.0)
(define (G-best bid) (= bid 3.0))

; Game H: auctioneer picks highest bid
(define (H-best bids) #t)  ; deterministic, always optimal

; Composed game: G feeds H
(define (composed-best bid all-bids)
  (and (G-best bid) (H-best all-bids)))

(define bid 3.0)
(define all-bids '(3.0 2.5 4.0))

(display "G equilibrium:        ") (display (G-best bid)) (newline)
(display "H equilibrium:        ") (display (H-best all-bids)) (newline)
(display "Composed equilibrium: ") (display (composed-best bid all-bids)) (newline)
(display "Decomposition holds:  ")
(display (eq? (composed-best bid all-bids)
              (and (G-best bid) (H-best all-bids))))
(newline)

# Hedges Thm 4.3: equilibria decompose

# Game G: advertiser bids (truthful = bid your value)
def G_play(bid, x): return bid
def G_best(bid): return bid == 3.0  # truthful value is 3.0

# Game H: auctioneer picks highest bid
def H_play(bids): return bids.index(max(bids))
def H_best(bids): return True  # deterministic, always "optimal"

# Sequential composition: G feeds H
def composed_best(bid, all_bids):
    return G_best(bid) and H_best(all_bids)

# Test: is truthful bidding an equilibrium of the composed game?
bid = 3.0
all_bids = [3.0, 2.5, 4.0]

comp = composed_best(bid, all_bids)
g_eq = G_best(bid)
h_eq = H_best(all_bids)

print(f"G equilibrium:        {g_eq}")
print(f"H equilibrium:        {h_eq}")
print(f"Composed equilibrium: {comp}")
print(f"Decomposition holds:  {comp == (g_eq and h_eq)}")
print()
print("Thm 4.3: check the parts, get the whole.")

DSIC composition, characterized

Hedges' decomposition theorem covers Nash, Bayesian-Nash, and subgame-perfect equilibria. It does not cover dominant-strategy incentive compatibility. DSIC doesn't compose in general — lying in stage 1 can give a payoff through stage 2's interface.

The sufficient condition is argmax-stability: the optimal report in each mechanism is independent of the other mechanism's outcome. Equivalently, "i-insensitive continuations" — player i's upstream report cannot affect i's downstream payoff. Additive separability of valuations is the sharp necessary condition for a mechanism-independent guarantee; any ε-violation admits a rectangle-test counterexample. The k-mechanism generalization requires k-way stability, not pairwise — the same structural gap as pairwise versus mutual independence in probability.

This auction pipeline satisfies the condition because the publisher filter is exogenous. The characterization currently lives in the docstring and in Vector Space; mechanized Lean proofs of the sufficient and necessary directions are still to be written.

Connections

• Strategyproof.lean — proves vcg_is_nash_equilibrium using this framework
• GaussianOptimality.lean — the capstone theorem this feeds into
• Ghani, Hedges, Winschel & Zahn (2018) — compositional game theory, Theorem 4.3
• Hedges (2017) — morphisms of open games
• Hedges (2018) — subgame-perfect equilibria in open games
• Bolt, Hedges & Zahn (2023) — Bayesian open games
• Kura et al. (2026) — indexed graded monad for welfare tracking