Payoff-free structural carriers for extensive games

This module contains only the representation-neutral dynamics used by the minimal EFG core.

Main definitions

• Arena — states, dependent legal actions, and transitions.
• Arena.IsTerminal — terminality as absence of legal actions.
• ControlledGame — an Arena with a root and player-control labels.
• Arena.ofFin — a small constructor for explicitly finite arenas.

No payoff, objective, probability law, finiteness assumption, decidability assumption, or information structure is stored in these carriers. In particular, mover s = none is only a non-player-control label. A chance law, when desired, belongs to a separate stochastic semantics layer.

This state-space representation permits merging paths, cycles, and infinite state or action types. History unfolding is provided separately.

structure Arena : Type (max (u_1 + 1) (u_2 + 1))

A game arena: the pure dynamics of an extensive-form game.

States, actions, and transitions are stored without players, payoffs, or probability. A state is terminal iff Action s is empty.

• State : Type u_1

  The state space.

• Action : self.State → Type u_2

  Available actions at each state. Empty means terminal.

• next (s : self.State) : self.Action s → self.State

  Transition function from a state and one legal action.

def Arena.IsTerminal (A : Arena) (s : A.State) : Prop

A state is terminal if there are no available actions.

Equations

• A.IsTerminal s = IsEmpty (A.Action s)

def Arena.IsDecision (A : Arena) (s : A.State) : Prop

A state is a decision point if it has at least one available action.

Equations

• A.IsDecision s = Nonempty (A.Action s)

theorem Arena.isTerminal_iff_not_isDecision (A : Arena) (s : A.State) : A.IsTerminal s ↔ ¬A.IsDecision s

Terminal and decision states are complementary.

structure ControlledGame (N : Type u_1) extends Arena : Type (max (max u_1 (u_2 + 1)) (u_3 + 1))

A payoff-free controlled extensive-game skeleton.

ControlledGame adds only a distinguished initial state and a mover label to the pure Arena dynamics. It deliberately stores no objective, payoff, probability law, finiteness, decidability, or information data.

At a nonterminal state, mover s = none means only that the state is not controlled by a strategic player. It does not itself supply a chance distribution. The mover label at a terminal state is semantically ignored.

• State : Type u_3
• Action : self.State → Type u_2
• next (s : self.State) : self.Action s → self.State
• init : self.State

  The initial state (root of the controlled game).

• mover : self.State → Option N

  Who controls each state. none means non-player-controlled.

@[reducible, inline]

abbrev ControlledGame.ofArena {N : Type u_1} (arena : Arena) (init : arena.State) (mover : arena.State → Option N) : ControlledGame N

Add an initial state and mover assignment to an ordinary arena.

Equations

• ControlledGame.ofArena arena init mover = { toArena := arena, init := init, mover := mover }

@[simp]

theorem ControlledGame.ofArena_toArena {N : Type u_1} (arena : Arena) (init : arena.State) (mover : arena.State → Option N) : (ofArena arena init mover).toArena = arena

@[simp]

theorem ControlledGame.ofArena_init {N : Type u_1} (arena : Arena) (init : arena.State) (mover : arena.State → Option N) : (ofArena arena init mover).init = init

@[simp]

theorem ControlledGame.ofArena_mover {N : Type u_1} (arena : Arena) (init : arena.State) (mover : arena.State → Option N) (state : arena.State) : (ofArena arena init mover).mover state = mover state

@[reducible, inline]

abbrev ControlledGame.arena {N : Type u_1} (G : ControlledGame N) : Arena

The arena of a payoff-free controlled game.

Equations

• G.arena = G.toArena

@[reducible, inline]

abbrev ControlledGame.actions {N : Type u_1} (G : ControlledGame N) (s : G.State) : Type u_2

Available actions at a state.

Equations

• G.actions s = G.Action s

@[reducible, inline]

abbrev ControlledGame.isTerminal {N : Type u_1} (G : ControlledGame N) (s : G.State) : Prop

A state is terminal.

Equations

• G.isTerminal s = G.IsTerminal s

def ControlledGame.isPlayerState {N : Type u_1} (G : ControlledGame N) (s : G.State) (i : N) : Prop

A state is controlled by player i.

Equations

• G.isPlayerState s i = (G.mover s = some i)

def ControlledGame.isNonPlayerState {N : Type u_1} (G : ControlledGame N) (s : G.State) : Prop

A nonterminal state carrying the non-player-control label.

This predicate deliberately supplies no probability law.

Equations

• G.isNonPlayerState s = (G.mover s = none ∧ ¬G.IsTerminal s)

@[reducible, inline]

abbrev ControlledGame.isChanceState {N : Type u_1} (G : ControlledGame N) (s : G.State) : Prop

Compatibility name for a non-player-controlled nonterminal state.

This structural predicate does not assert that a chance law exists. Stochastic layers may interpret such a state as chance only after supplying the relevant law.

Equations

• G.isChanceState s = G.isNonPlayerState s

def ControlledGame.NoChance {N : Type u_1} (G : ControlledGame N) : Prop

Every nonterminal state has a strategic mover.

Equations

• G.NoChance = ∀ (s : G.State), ¬G.isTerminal s → ∃ (i : N), G.mover s = some i

def Arena.ofFin (n : ℕ) (nActions : Fin n → ℕ) (next : (s : Fin n) → Fin (nActions s) → Fin n) : Arena

Build an arena from a Fin-indexed state space with finite action types. Terminal states have nActions s = 0.

Equations

• Arena.ofFin n nActions next = { State := Fin n, Action := fun (s : Fin n) => Fin (nActions s), next := next }