Formalize MFoGT Chapter 7.2–7.4

[lyw-ops]

Summary

Formalize and semantically audit MFoGT Chapter 7.2–7.4:

• complete the correlated-equilibrium information-extension API, including
  mixed contingent plans, behavioral realizations, canonical distributions,
  obedience, Nash-product inclusion, and finite convex-hull structure;
• add the Section 7.3 no-regret development: a reusable stochastic Blackwell
  projection theorem, external and internal regret matching, invariant
  measures, canonical Ionescu–Tulcea processes, calibration, Hannan sets,
  no-comparison-regret sets, and convergence to correlated equilibrium;
• add the Section 7.4 Bayesian-game development: primitive and reduced finite
  games, ex-ante/interim equilibrium equivalence, mixed/behavioral/
  distributional representations, finite equilibrium existence, standard
  Borel random-seed and disintegration results, nonatomic equilibrium, and all
  three parts of the Bayesian war-of-attrition example;
• update the knowledge blueprint and add a declaration-by-declaration semantic
  audit against MFoGT and the corresponding MSZ treatments.

Semantic and proof fixes

• distinguish source-literal mixed contingent plans from behavioral strategies
  and prove their realization and equilibrium equivalence;
• distinguish primitive states from reduced type profiles and prove payoff and
  equilibrium preservation;
• guard interim claims at positive-probability types and expose MSZ's
  full-support specialization without claiming type-dependent action sets;
• prove the source-literal calibration residual formula equal to the
  frequency-weighted conditional-frequency formula;
• construct the stochastic processes used by the no-regret propositions
  instead of leaving conditional-process hypotheses as an implicit existence
  claim;
• make every regularity assumption used by war-of-attrition uniqueness
  explicit and prove the corresponding regular classes are inhabited;
• keep the Harsanyi strategic form separate from MSZ's unformalized
  player-type agent normal form.

No textbook PDF, scan, OCR output, or generated blueprint site is included.

Validation

• lake build
• lake build EconCSLib.Examples
• python3 scripts/check_lean_placeholders.py EconCSLib
• python3 -m unittest tests/test_check_knowledge_references.py
• python3 scripts/check_knowledge_references.py docs/knowledge
• mdblueprint-check docs/knowledge --lean-root .
• git diff --check

mdblueprint-check reports zero errors and zero warnings. Two independent
#print axioms passes over the source-facing and non-vacuity theorem families
reported only propext, Classical.choice, and Quot.sound, with no
sorryAx. Under the explicitly stated hypotheses, the audit found no false
proposition in the covered Sections 7.2–7.4.