Add a payoff-free structural core for extensive-form games

[lyw-ops]

Summary

This PR introduces a narrow, payoff-free structural foundation for Arena-based extensive-form games:

• split universal dynamics (Arena) from controlled dynamics (ControlledGame), while retaining ExtensiveGame N U as the existing state-payoff compatibility layer;
• use isNonPlayerState as the canonical structural name for a nonterminal state without a player mover, while retaining isChanceState as a compatibility alias that supplies no probability law;
• move finite transition reachability out of the historical Subgame module;
• add occurrence-sensitive dependent histories and history unfolding;
• add measure-free complete legal plays that cover both genuinely infinite play and finite play by terminal stuttering;
• add a payoff-free observed/information carrier with information-indexed pure strategies and player relabeling;
• expose these declarations through the opt-in Interface.StructuralCore facade.

Design boundary

The structural core deliberately assumes no finiteness, decidable equality, termination, probability law, objective, payoff semantics, recall condition, or equilibrium concept. Those properties can be supplied later as separate certificates and semantic layers. This keeps the same carriers usable for finite computation, infinite games, logical games, and analytic models.

Interface.StructuralCore has the following exact EFG implementation closure:

1. Structural.Basic
2. Structural.Reachability
3. Structural.History
4. Execution.CompletePlay
5. Observed.Controlled

The facade is opt-in in this pre-stability PR; EconCSLib.lean is intentionally unchanged.

Compatibility

Execution.Reachability and Execution.History remain compatibility imports of their canonical Structural.* owners. Subgame.lean imports the extracted reachability module and removes only the declarations moved there. Its existing Play import is retained so current downstream modules do not lose their historical transitive dependency. The existing Strategy, Play, Subgame, BehaviorStrategy, and finite Arena modules all build against the new ExtensiveGame extends ControlledGame representation.

Regression coverage

• HistoryDiamond imports Structural.History directly and proves that two distinct action occurrences remain distinct histories even when they reach the same endpoint state.
• TerminalMoverIgnored verifies that a mover label on a terminal state creates no decision-information coordinate.
• StructuralCoreImportBoundary checks the intended public structural declarations from the narrow facade, including the canonical and compatibility non-player-state names, and guards against payoff-aware declarations leaking through the facade.

Verification

• lake build
• lake build EconCSLib.Examples
• python3 scripts/check_lean_placeholders.py EconCSLib
• git diff --check

All checks pass on a clean branch based on current upstream main.

[jiajunma]

Looks good