---
name: project-step1555-lean4-mystery-verifier-2026-08-29
description: STEP 1555 v0.3 Lean 4 formalization arc 4/5 — mystery-reasoning-connector verifier 2 条件 (uniqueness + necessity) を Lean 4 で abstract formalize、 8 theorem 全 axiom-free
metadata: 
  node_type: memory
  type: project
  originSessionId: c922ed16-8768-46a2-904a-a44edbee09b5
  modified: 2026-08-28T23:32:43.308Z
---

# STEP 1555: v0.3 Lean 4 formalization (arc 4/5)

**Date**: 2026-08-29
**Arc**: v0.3 5-step arc (4/5)
**Files**:
- `data/lean4-mathlib/CollatzRei/MysteryReasoningVerifier.lean` (7 theorem + 1 instance、 全 axiom-free)
- `data/lean4-mathlib/MysteryReasoningVerifierAxiomCheck.lean` (`#print axioms` 検証)

## 実装

TS 実装 (`src/mcp/mystery-reasoning-connector.ts`) の abstract model を Lean 4 で formalize。

### 抽象型
```lean
abbrev Suspect := Nat
structure Fact where id : Nat deriving DecidableEq
structure Spec where
  suspects : List Suspect
  providedFacts : List Fact
  expectedCulprit : Suspect
  runCircuit : List Fact → List Suspect
```

### 検証器 2 条件 (核心定義)
```lean
def isUniqueCorrect (s : Spec) : Prop :=
  s.runCircuit s.providedFacts = [s.expectedCulprit]

def isNecessary (s : Spec) : Prop :=
  ∀ f ∈ s.providedFacts,
    s.runCircuit (s.providedFacts.filter (fun x => x.id ≠ f.id)) ≠ [s.expectedCulprit]

def isWellPosed (s : Spec) : Prop :=
  isUniqueCorrect s ∧ isNecessary s
```

### 8 Theorem (全 axiom-free 検証済み)

1. `wellPosed_implies_uniqueCorrect` — well-posed → uniqueness (And.left)
2. `wellPosed_implies_necessary` — well-posed → necessity (And.right)
3. `redundant_implies_not_necessary` — 冗長 fact 存在 → necessity 破綻
4. `wellPosed_no_redundant` — well-posed spec に冗長 fact なし (Corollary of 3)
5. `empty_facts_uniqueness_iff` — 空 facts の uniqueness 等価変形
6. `empty_facts_trivially_necessary` — 空 facts は vacuously necessary
7. `fair_play_by_construction` — runCircuit は providedFacts の関数 (構造保証、 trivially rfl)
8. `isUniqueCorrect_decidable` (instance) — uniqueness の decidability

## Axiom profile (全 axiom-free 検証)

`#print axioms` 出力:
```
'wellPosed_implies_uniqueCorrect' does not depend on any axioms
'wellPosed_implies_necessary' does not depend on any axioms
'redundant_implies_not_necessary' does not depend on any axioms
'wellPosed_no_redundant' does not depend on any axioms
'empty_facts_uniqueness_iff' does not depend on any axioms
'empty_facts_trivially_necessary' does not depend on any axioms
'fair_play_by_construction' does not depend on any axioms
'isUniqueCorrect_decidable' does not depend on any axioms
```

**全 8 theorem が propext / Classical.choice / Quot.sound など axiom を一切参照しない完全 axiom-free**。 Rei Lean 4 collection の "zero-axiom floor" (現在 94/333 = 28.2%) に 8 theorem 追加候補。

## Build 結果

- `lake build CollatzRei.MysteryReasoningVerifier`: **461 jobs succeeded, 6.1s** (build 成功)
- `lake env lean MysteryReasoningVerifierAxiomCheck.lean`: **8 theorem 全 axiom-free** 出力

## Honest scope

- 本 file は verifier 2 条件の 論理的関係のみ formalize。 各 chip (contradiction/timeline/alibi/elimination/common_feature) の soundness/completeness は本 file scope 外 (v0.4+ defer)。
- runCircuit は abstract function として type-only。 具体的な 5 chip の合成としての実装は Lean 4 side には持ち込まず (TS 側実装のみ)。 「TS 実装が本 file の仕様を満たす」 は independent verification で確認する形。
- 「mystery verifier formalization で世界初」 主張ゼロ。 constraint satisfaction meta-theory の standard adaptation で novelty は Rei stack 内での position (STEP 1538 engine の formal specification layer) のみ。
- Theorem 3 は 単方向 (→) のみ。 iff 版 (双方向) は Classical logic なしで示すには追加 decidability 前提が要り、 現在 unidirectional で pedagogical value 十分と判断。

## STEP 1548 chip 昇格との対応

STEP 1548 で contradiction/timeline chip に elimination 昇格を追加したが、 これらは runCircuit の具体的 chip implementation に該当し、 本 formalization では abstract function として吸収される (Spec.runCircuit の behavior に含まれる)。 Chip 個別の formal 化は v0.4+ defer。