nash_equilibrium_verdict tool v0.1

STEP: 1520 / 公開日: 2026-08-28 / Test: 17/17 PASS / Lean 4: 6 theorem zero sorry / Type: STEP 1498 経済学 arc candidate #2 実装 (47 defer 全体 11 番目)

★ Nash 均衡 = SELF⟲ operational tool 化: 2-player payoff matrix → best response 相互不動点 探索 → 均衡数 → verdict (unique → SELF⟲ / multiple → BOTH / none → NEITHER)。 STEP 1498 経済学 arc の 核 identity を tool 化。

短答 (3 行)

❶ Nash 均衡 検知 tool: 2-player normal form game (aPayoffs / bPayoffs matrix) → 全 cell で best response 相互 check → 純戦略 Nash 均衡 検知。

❷ D-FUMT₈ SELF⟲ 経済領域 実装: unique Nash = SELF⟲ (Lawvere/Tang Nano/Halting/feedback/Nash/進化/metacognition/Liar 8 統一 の 経済 tool)。 multiple Nash = BOTH (coordination problem)。

❸ 14 姉妹 verdict tool 目。

決定表 (5 case)

#ConditionVerdictReason
1invalid matrix (非 rectangular, empty)NEITHERinvalid_matrix
2A/B dimension mismatchNEITHERdimension_mismatch
30 pure NashNEITHERno_pure_equilibrium
41 pure NashSELF ★unique_nash_equilibrium
5≥2 pure NashBOTHmultiple_equilibria

使用例

// Prisoner's Dilemma: unique Nash at (Defect, Defect)
nashEquilibriumVerdict({
  aPayoffs: [[3, 0], [5, 1]],  // A rows = Cooperate/Defect
  bPayoffs: [[3, 5], [0, 1]],  // B cols = Cooperate/Defect
});
// { verdict: 'SELF', equilibria: [{rowIndex:1, colIndex:1, aPayoff:1, bPayoff:1}],
//   reason: 'unique_nash_equilibrium' }

// Battle of the Sexes: 2 pure Nash (coordination problem)
nashEquilibriumVerdict({
  aPayoffs: [[3, 0], [0, 2]],
  bPayoffs: [[2, 0], [0, 3]],
});
// { verdict: 'BOTH', equilibriumCount: 2, reason: 'multiple_equilibria' }

// Matching Pennies: NO pure Nash (mixed strategy only)
nashEquilibriumVerdict({
  aPayoffs: [[1, -1], [-1, 1]],
  bPayoffs: [[-1, 1], [1, -1]],
});
// { verdict: 'NEITHER', equilibriumCount: 0, reason: 'no_pure_equilibrium' }

Lean 4 (6 theorem zero sorry)

nash_zero_gives_neither         : count=0 → NEITHER
nash_unique_gives_self          : count=1 → SELF ★ (unique Nash = fixpoint)
nash_multiple_gives_both        : count≥2 → BOTH
a_best_tie_gives_true           : tie → best response true
a_best_strict_gives_true        : strict better → true
a_best_lose_gives_false         : losing → false

Test coverage (17/17 PASS)

Guard 3 + SELF unique 6 + BOTH multiple 3 + NEITHER no-Nash 3 + 1x1 edge 1 + Determinism 1

Rei stack との 対応

Honest scope

❶ 純戦略 Nash のみ検知、 混合戦略 Nash (Nash 1950 theorem 保証、 Kakutani fixpoint) は 未実装 (matrix game LP 解法 別 tool candidate)。

❷ n×m matrix 完全対応、 n-player (>2) game は 未対応 (2-player normal form のみ)。

❸ 弱支配 / 強支配 均衡 refinement 未実装 (subgame perfect / Bayesian Nash 等)。

❹ 「世界初」 なし = Nash 1950 既知 D-FUMT₈ mapping、 novelty = SELF⟲ verdict の operational tool 化 + Rei stack SELF⟲ 8 統一 と 直結。

❺ 累計 defer 38 → 37。