---
name: project-step1557-chip-lean4-v04-2026-08-29
description: STEP 1557 v0.4 arc 1/5 — 5 chip 個別 Lean 4 semantic formalization、 11 theorem proved (3 axiom-free + 6 propext-only + 2 propext+Quot.sound)
metadata: 
  node_type: memory
  type: project
  originSessionId: c922ed16-8768-46a2-904a-a44edbee09b5
  modified: 2026-08-28T23:46:10.533Z
---

# STEP 1557: v0.4 Chip 個別 Lean 4 formalization (arc 1/5)

**Date**: 2026-08-29
**Files**: `data/lean4-mathlib/CollatzRei/MysteryChipSemantics.lean` (11 theorem) / `MysteryChipSemanticsAxiomCheck.lean`

## 抽象型

- `Suspect { id, attrs: Attribute → Option Bool, claimedLocation, claimedTime }`
- `PersonFact { attribName, requiredPolarity }` (「attribute」 は Lean 4 keyword で回避)
- `RecordFact { place, capturedSuspect, recordedTime }`
- `TestimonyFact { speaker, claimedTime, claimedPlace }`

## Chip semantic (5 chip)

1. **eliminationChipEliminates** — attrs match check
2. **commonFeatureChipEliminates** — List.any of elimination
3. **alibiChipEliminates** — claimedLocation ∧ claimedTime ↔ record confirm
4. **contradictionDetected** — testimony vs record dominance (v0.3)
5. **timelineImpossible** — needed > gap (v0.3)

## 11 Theorem (全 proved)

| Theorem | Axiom profile |
|---|---|
| 1. elimination_sound | **axiom-free** |
| 2. elimination_preserves_match | propext |
| 3. elimination_undefined_preserves | **axiom-free** |
| 4. commonFeature_sound | propext + Quot.sound |
| 5. commonFeature_preserves_all_match | propext + Quot.sound |
| 6. alibi_sound | propext |
| 7. alibi_no_claim_preserves | propext |
| 8. alibi_no_time_preserves | propext |
| 9. contradiction_sound | propext |
| 10. timeline_sound | **axiom-free** |
| 11. timeline_feasible | propext + Quot.sound |

- **3 完全 axiom-free** (elimination_sound / elimination_undefined_preserves / timeline_sound)
- **6 propext-only** (Lean 4 標準 constructor axiom)
- **2 propext + Quot.sound** (Mathlib simp lemma 経由)

STEP 1555 の全 8 完全 axiom-free と比較して 「実装 chip の semantic 化 は Mathlib 依存で propext 混入」 の観察。 STEP 1555 は abstract verifier layer で標準論理演算のみ使用、 実 impl 化で複雑化する pattern。

## Build 結果

- `lake build CollatzRei.MysteryChipSemantics`: **461 jobs succeeded, 6.7s**
- `lake env lean MysteryChipSemanticsAxiomCheck.lean`: 11 theorem 全 profile 出力

## Honest scope

- 各 chip の TS 実装との 1:1 対応は取らず、 論理骨格のみ formalize
- Soundness (eliminated ⇒ 該当性の証拠) は各 chip について定式化済
- **Completeness (該当性なし ⇒ eventually eliminated) は 一部 chip のみ**:
  - elimination / common_feature / alibi: preserve-condition として直接示せる (theorem 2, 3, 5, 7, 8)
  - contradiction / timeline v0.3: 「exactly 1 caught liar / impossible」 の構造前提が要り、 部分的な必要条件のみ (theorem 9, 10, 11)
- 「chip verifier で世界初」 主張ゼロ、 pattern matcher の standard semantic formalization
- Attribute renaming (`attribute` → `attribName`) は Lean 4 keyword collision 回避