Integrate extensive game subgame restrictions

[Szher111]

Summary

This PR supersedes #14 and formalizes subgame-oriented results for finite
perfect-information GameTrees.

• add subtree and proper-subgame infrastructure for finite game trees;
• add root-scoped Nash and subgame-perfect equilibrium statements;
• prove subgame restriction lemmas for SPE;
• prove Nash/SPE equivalence when there are no proper subgames;
• add node/children decomposition lemmas for SPE;
• add backward-induction existence statements via optStrategy;
• add examples for Entry Deterrence, Ultimatum Game, Centipede Game, and simple
  finite trees.

The branch was rebuilt after #14 was closed. The current pushed commit is:

22a63e7eaa5f0c7f8a6e86ce0170184382ea54b2

Scope

Affected Lean modules:

• EconCSLib/GameTheory/ExtensiveGame/GameTree.lean
• EconCSLib/GameTheory/ExtensiveGame/GameTreeNE.lean
• EconCSLib/GameTheory/ExtensiveGame/GameTreeSPE.lean
• EconCSLib/GameTheory/ExtensiveGame/GameTreeStrategicForm.lean
• EconCSLib/GameTheory/ExtensiveGame/Zermelo.lean
• EconCSLib/GameTheory/ExtensiveGame/FiniteArenaExtraction.lean
• EconCSLib/GameTheory/ExtensiveGame/ImperfectInformation.lean
• EconCSLib/GameTheory/ExtensiveGame/Strategy.lean
• EconCSLib/Examples/SimpleGameTree.lean
• EconCSLib/Examples/EntryDeterrence.lean
• EconCSLib/Examples/UltimatumGame.lean
• EconCSLib/Examples/CentipedeGame.lean
• EconCSLib/Examples.lean
• EconCSLib/Foundation/Preference.lean

Verification

• lake build
• lake build EconCSLib.Examples
• python3 scripts/check_lean_placeholders.py EconCSLib passed
• git diff --check
• Blueprint checks run when docs/knowledge/ changed

Checked locally:

lake exe cache get
lake build EconCSLib.Examples
python3 scripts/check_lean_placeholders.py EconCSLib
git diff --check

Result:

Build completed successfully (1593 jobs).

No docs/knowledge/ files are changed in this PR, so the blueprint check is not
applicable.

Notes

This PR is limited to finite perfect-information game trees and pure strategies.
It does not attempt to formalize mixed strategies, belief systems, sequential
equilibrium, or general infinite games.

The table below gives the theoretical references and their correspondence to the
code diffs, following the request in #14.

Game-theoretic statement	Reference	Lean correspondence
Finite perfect-information extensive games can be represented by rooted game trees with terminal payoff vectors.	Maschler, Solan, and Zamir, Game Theory, Ch. 6-7.	GameTree, children, size in GameTree.lean; examples in SimpleGameTree.lean, EntryDeterrence.lean, UltimatumGame.lean, CentipedeGame.lean.
A subgame is the game induced by a node/subtree of the original extensive game.	MSZ, Ch. 7, subgames and subgame-perfect equilibrium.	Subtree, Subtree.head, Subtree.tail_mem, Subtree.child_mem, Subtree.trans in GameTree.lean.
A proper subgame is a subgame other than the whole game.	Standard subgame terminology used in SPE definitions.	ProperSubgame, ProperSubgame.toSubtree, ProperSubgame.ne, ProperSubgame.size_lt, properSubgame_Node_iff_exists_child_subtree in GameTree.lean.
SPE means Nash equilibrium in every subgame.	MSZ, Ch. 7, definition of subgame-perfect equilibrium.	IsSubgamePerfectOn, isSubgamePerfectOn_iff_forall_subtree_isNashAt, IsNashAt.toSubgamePerfectOn_of_forall_subtree_isNashAt in GameTreeNE.lean.
SPE restricts to subgames and gives Nash equilibrium in each subgame.	Direct consequence of the SPE definition.	IsSubgamePerfectOn.of_subtree, IsSubgamePerfectOn.toNashAt_of_subtree, IsSubgamePerfectOn.forall_subtree_isNashAt, IsSubgamePerfectOn.of_properSubgame, IsSubgamePerfectOn.toNashAt_of_properSubgame in GameTreeNE.lean.
If a game has no proper subgames, SPE and Nash at the root coincide.	Immediate consequence of the SPE definition.	HasOnlyRootSubgames in GameTree.lean; isSubgamePerfectOn_iff_isNashAt_of_hasOnlyRootSubgames, isSubgamePerfectOn_iff_isNashAt_of_no_properSubgame in GameTreeNE.lean.
SPE at a node decomposes into Nash at that node and SPE on child subgames.	Finite-tree structural decomposition of SPE.	isSubgamePerfectOn_Node_iff, IsSubgamePerfectOn.toNashAt_and_head_tail, isSubgamePerfectOn_Node_iff_children, IsSubgamePerfectOn.toNashAt_and_children in GameTreeNE.lean.
Finite perfect-information games have pure SPE by backward induction.	Kuhn-style backward-induction theorem; MSZ Ch. 7.	optStrategy_isSubgamePerfectOn, optStrategy_isNashAt, Kuhn_exists_SPE_on, Kuhn_exists_NE, Kuhn_exists_SPE_on_subtrees, Kuhn_exists_NE_on_subtrees in GameTreeNE.lean; Kuhn_exists_SPE in GameTreeSPE.lean.
The strategic-form game extracted from a finite game tree has Nash equilibria corresponding to root-level IsNashAt statements.	Strategic form associated with an extensive-form game.	profileStrategy, toStrategicGame_nash_iff_isNashAt, exists_toStrategicGame_nash_iff_exists_isNashAt, IsSubgamePerfectOn.toStrategicGame_nash in GameTreeStrategicForm.lean.
Entry Deterrence separates root Nash equilibrium from SPE by eliminating non-credible threats.	Standard entry-deterrence example motivating SPE as a refinement of Nash equilibrium.	entryDeterrenceSubgame, entryDeterrenceSubgame_properSubgame, stayOutFight_isNashAt_entryDeterrence, stayOutFight_not_isSubgamePerfectOn_entryDeterrence, enterAccommodate_isSubgamePerfectOn_entryDeterrence in EntryDeterrence.lean.
The finite Ultimatum Game illustrates subgame reasoning and pure SPE characterization.	Standard finite ultimatum game example; MSZ Exercise 7.5 is referenced in file comments.	IsNashProfile, nashProfile_isNash, RickSequentiallyRational, rickSequentiallyRational_iff, isSubgamePerfectProfile_iff, ultimatum_has_spe_on, ultimatum_optStrategy_spe_on, ultimatum_strategic_form_has_nash in UltimatumGame.lean.
Centipede-style finite games illustrate backward-induction outcomes and SPE reasoning.	Standard centipede-game backward-induction example.	centipedePrefixStop_isSubgamePerfectOn, centipedePrefixContinue_not_isNashAt, centipedeMSZStop_isSubgamePerfectOn_tree, centipedeMSZ100_stop_isSubgamePerfectOn in CentipedeGame.lean.

[zhanquen]

Dear Szher111, thanks for rebuilding.