pareto_frontier_verdict tool v0.1

STEP: 1522 / 公開日: 2026-08-28 / Test: 28/28 PASS / Lean 4: 7 theorem zero sorry / Type: STEP 1498 経済学 arc candidate 実装 (economics 3rd tool)

★ 経済学 tool trio 完成: peace_axiom_verdict (STEP 1506) + nash_equilibrium_verdict (STEP 1520) + **pareto_frontier_verdict (本 STEP)** = D-FUMT₈ 経済学 arc の 核 3 identity (positive-sum + Nash SELF⟲ + Pareto BOTH) の tool 実装 完了。

短答 (3 行)

❶ Pareto 支配 判定 tool: allocation set + queryIndex → 支配関係 → verdict (dominated FALSE / frontier BOTH / dominant TRUE / invalid NEITHER)。

❷ D-FUMT₈ BOTH 経路: frontier tradeoff → BOTH (STEP 1379 Cohen's d BOTH 経路 と 同型、 誰かの利得↑ = 誰かの利得↓ 必要)。

❸ 16 姉妹 verdict tool 目。

決定表 (6 case)

#ConditionVerdictReason
1invalid (empty, non-rect)NEITHERinvalid_input
2negative payoffNEITHERinvalid_value
3queryIndex out of rangeNEITHERindex_out_of_range
4query dominated by anotherFALSEdominated_inefficient
5query on Pareto frontierBOTH ★pareto_frontier_tradeoff
6query dominates all othersTRUEdominant_optimal

使用例

// [1,1] dominated by [2,2] → FALSE
paretoFrontierVerdict({
  allocations: [[1, 1], [2, 2]],
  queryIndex: 0,
});
// { verdict: 'FALSE', dominators: [1] }

// [3,1] on Pareto frontier (incomparable with [1,3]) → BOTH
paretoFrontierVerdict({
  allocations: [[3, 1], [1, 3], [2, 2]],
  queryIndex: 0,
});
// { verdict: 'BOTH', frontierIndices: [0, 1, 2] }

// [5,5] strictly dominates [1,1], [2,2] → TRUE
paretoFrontierVerdict({
  allocations: [[5, 5], [1, 1], [2, 2]],
  queryIndex: 0,
});
// { verdict: 'TRUE', dominated: [1, 2] }

// 3-player 対応
paretoFrontierVerdict({
  allocations: [[1, 1, 1], [2, 2, 2]],
  queryIndex: 0,
});
// { verdict: 'FALSE', numPlayers: 3 }

Lean 4 (7 theorem zero sorry)

pareto_equal_no_dominate            : (a,b) vs (a,b) → 支配なし
pareto_strict_dominates             : 全 strict better → 支配
pareto_one_strict_dominates         : 1 strict + 1 equal → 支配
pareto_one_loss_no_dominate         : 1 loss → 支配不能
pareto_verdict_dominated_false      : dominated → FALSE
pareto_verdict_dominant_true        : dominates all → TRUE
pareto_verdict_frontier_both        : frontier → BOTH ★

Test coverage (28/28 PASS)

Guard 4 + FALSE dominated 3 + BOTH frontier 3 + TRUE dominant 2 + Edge single/identical/3-player 5 + Frontier detection 6 + Determinism 5

Rei stack との 対応

Honest scope

❶ 純粋 Pareto (strict) のみ、 弱 Pareto / lexicographic 未 embed。

❂ n-player 完全対応、 ただし 全 pairwise comparison O(n²·m) 計算量。

❸ 効用比較可能性 (utility comparability) 前提、 順序尺度のみ で 済む cases も 別 candidate。

❹ 「世界初」 なし = Pareto 1906 既知 D-FUMT₈ mapping。

❺ 累計 defer 36 → 35 (STEP 1521 + 本 STEP で 2 tool 追加)。