STEP: 1506 / 公開日: 2026-08-28 / Test: 45/45 PASS / Lean 4: 12 theorem zero sorry / Type: STEP 1498 candidate ★核 実装
★ Peace Axiom #196 の operational tool 化: Rei-AIOS 全 layer 永久 TRUE 不変制約 (Theory #196) を pure function verdict tool として 実装。 payoff 変化 → positive-sum (TRUE 順守) / zero-sum (NEITHER 中立) / negative-sum (FALSE 違反 最悪) を 決定的に 判定。
❶ Peace Axiom #196 tool 化: STEP 1498 経済学 arc の 6 defer candidate 第 1 号 実装。 47 defer candidate 全体 の 2 番目 実装 (STEP 1499 shannon_entropy_verdict の 続編)。
❷ 決定表 7 case: empty/mismatch/negative → NEITHER (判定不能) / dead trade (両 0) → ZERO / positive-sum → TRUE / negative-sum → FALSE / zero-sum → NEITHER (中立)。
❸ Player 個別分析: 総 sum verdict に 加えて gained/lost/unchanged 各 player 数を 返却、 win-lose vs win-win の 判別可能。
| # | Condition | Verdict | Reason |
|---|---|---|---|
| 1 | before or after empty | NEITHER | empty_payoff_list |
| 2 | length mismatch | NEITHER | length_mismatch |
| 3 | any negative (NaN 含む) | NEITHER | negative_payoff |
| 4 | before total == after total == 0 | ZERO | dead_trade |
| 5 | after total > before total | TRUE (⊤) | positive_sum_peace_compliant |
| 6 | after total < before total | FALSE (⊥) | negative_sum_peace_violation |
| 7 | after total == before total (非零) | NEITHER | zero_sum_peace_neutral |
import { peaceAxiomVerdict } from './src/mcp/peace-axiom-verdict';
// A: 両方 up (positive-sum) → TRUE
const rA = peaceAxiomVerdict({ before: [10, 10], after: [15, 15] });
// { verdict: 'TRUE', reason: 'positive_sum_peace_compliant',
// totalDelta: 10, isPeaceCompliant: true, playersGained: 2, ... }
// B: win-lose net positive → TRUE (Peace 順守)
const rB = peaceAxiomVerdict({ before: [10, 10], after: [20, 5] });
// { verdict: 'TRUE', playersGained: 1, playersLost: 1, totalDelta: 5, ... }
// C: zero-sum (win-lose net zero) → NEITHER (Peace 中立)
const rC = peaceAxiomVerdict({ before: [10, 10], after: [15, 5] });
// { verdict: 'NEITHER', reason: 'zero_sum_peace_neutral', totalDelta: 0, ... }
// D: negative-sum (両方 down) → FALSE (Peace 違反 最悪 case)
const rD = peaceAxiomVerdict({ before: [10, 10], after: [5, 5] });
// { verdict: 'FALSE', isPeaceCompliant: false, playersLost: 2, ... }
// E: dead trade (両方 0) → ZERO
const rE = peaceAxiomVerdict({ before: [0, 0], after: [0, 0] });
// { verdict: 'ZERO', reason: 'dead_trade', ... }
ファイル: data/lean4-transfer/step1506_peace_axiom_verdict.lean
-- 総和 identity total_empty : total_payoff [] = 0 total_single : total_payoff [n] = n total_pair : total_payoff [a, b] = a + b -- Peace verdict 決定表 (★核) peace_positive_gives_true : positive-sum → TRUE (Peace 順守) peace_negative_gives_false : negative-sum → FALSE (Peace 違反) peace_zero_sum_gives_neither : zero-sum 非零 → NEITHER (中立) peace_dead_trade_gives_zero : 両方 0 → ZERO -- 累計効果 (transitive Peace) all_positive_empty : 空 pair → true all_positive_length_mismatch : mismatch → false all_positive_single_up : 単一 up step → true -- 総和 保存性 total_shift_up : 全 player k up → 総和 k*n 増 shift_up_gives_positive_total : k>0, 非空 → 総和 増加 (十分条件)
| Category | Tests | Cases |
|---|---|---|
| Guard (NEITHER) | 10 | empty / length mismatch / negative / NaN |
| ZERO | 4 | dead trade (両方 0) |
| TRUE (positive-sum) | 13 | 両方 up / 1 up 1 same / win-lose net positive |
| FALSE (negative-sum) | 7 | 両方 down / win-lose net negative |
| NEITHER (zero-sum) | 7 | win-lose net zero / all unchanged |
| Edge (single player) | 2 | single up |
| Determinism | 2 | same input → same output |
実行: npx tsx test/step1506-peace-axiom-verdict-test.ts
| # | tool | 入力 | 目的 | STEP |
|---|---|---|---|---|
| 1 | d8_verdict_from_measurement | value + noise + threshold | SNR verdict | 1350 |
| 2 | d8_verdict_from_multi_trial | p-value list + FDR α | BH FDR aggregate | 1371 |
| 3 | d8_verdict_from_sample_pair | 2 sample lists | Welch t-test + Cohen's d BOTH | 1376+1379 |
| 4 | shannonEntropyVerdict | frequency list | H(X) → 8 verdict | 1499 |
| 5 | peaceAxiomVerdict ★ | before/after payoffs | Peace Axiom #196 tool 化 | 1506 (本 tool) |
5 tool 揃った ことで 「1 値 / 2 値比較 / 多試行 / 分布 / ゲーム前後 payoff」 の 5 側面 D-FUMT₈ verdict 化 core 拡張。
❶ payoff は Nat (整数) 前提、 実数 payoff は Math.round で 前処理必要 (Rei stack の Nat verdict 統一 に 合わせる)。
❷ Peace Axiom = positive-sum は Rei 独自 operational 定義 (STEP 1498 で 明示)。 economics 学術界 では 単純化 と 見做される 可能性 (win-win negotiation 理論 は 存在 だが 「Peace = positive-sum」 の 一意 対応 は Rei 特有)。
❸ Lean 4 side は 決定表 骨格 4 verdict (TRUE/FALSE/NEITHER/ZERO) の 静的 identity、 累計効果 の 系列判定 は 別 tool (合意予定 defer)。
❹ 「世界初」 主張なし。 zero-sum game theory (von Neumann 1928) の Peace Axiom #196 operational 化。 novelty = Rei 独自 mapping と 5 tool 統一 API。
❺ 累計 defer 47 → 46 candidate (本 tool 実装 済)。