---
name: Paper 77 — LeanDFumt 8値論理 Lean 4 ライブラリ公開
description: D-FUMT₈ proof-theoretic anchor 完成. 29 zero-sorry 定理, Mathlib 非依存 5秒 build, Apache-2.0, 公開 GitHub repo + v1.0.0 release + Zenodo DOI 19596351
type: project
originSessionId: a08149e8-f1de-4fbc-b4eb-fb2cec8fad21
---
# Paper 77 — LeanDFumt (2026-04-16)

**Why:** チャット版 Claude の「Lean5 by Rei」hallucinate を訂正後、藤本さん要請で **戦略 ① ライブラリ方式** 採用. Lean 4 fork ではなく additive library として実装. これで Rei の D-FUMT₈ 三角 anchor (Schnorr ceiling Paper 69 + QuTiP floor Papers 75/76 + Lean proof anchor Paper 77) 完成.

**How to apply:** 今後の Rei Lean4 形式化 (Paper 73/74 拡張等) で `LeanDFumt` を `lake require`. 8値の判定が必要な場面で `DFUMT8.asProp` 経由で Mathlib 互換に統合.

## 公開リポジトリ

- **GitHub**: https://github.com/fc0web/lean-d-fumt8 (Apache-2.0)
- **Release v1.0.0**: https://github.com/fc0web/lean-d-fumt8/releases/tag/v1.0.0
- **Zenodo**: https://doi.org/10.5281/zenodo.19596351
- **IA**: https://archive.org/details/rei-aios-paper-77-1776266085754
- **Qiita**: https://qiita.com/fc0web/items/1bb2bd3dc87cdcaba8e8
- **Harvard**: https://doi.org/10.7910/DVN/KC56RY

## ライブラリ構造

```
LeanDFumt/
  Basic.lean           inductive DFUMT8 + neg/and/or/implies + sanity examples
  Theorems.lean        29 zero-sorry algebraic properties
  PropEmbedding.lean   toBool / toTernary / asProp + Decidable instance
LeanDFumt.lean         re-exports
lakefile.toml          Lake manifest (Mathlib 非依存)
lean-toolchain         leanprover/lean4:v4.27.0
```

**Build 時間**: ~5 秒 (cold), ~1 秒 (warm). Mathlib 依存の通常 Lean 4 project (~30 分) より 2 桁高速.

## 29 zero-sorry 定理 group breakdown

| Group | Count |
|---|---:|
| Negation (neg_TRUE, neg_BOTH_self, neg_neg_classical 等) | 8 |
| Conjunction (and_FALSE_left/right, restricted NEITHER, classical TRUE) | 4 |
| Disjunction (or_TRUE_left/right, restricted NEITHER/FALSE) | 5 |
| Idempotency (and_idem, or_idem 全 8 値) | 2 |
| Commutativity (classical pair) | 2 |
| Implication (classical truth table 4 + D-FUMT₈ extensions 3) | 7 |
| Numeric anchor (toFloat_TRUE_pos via native_decide) | 1 |

## 戦略選定の正直な記録

| 戦略 | Lean 4 変更 | Mathlib 互換 | 工程 | 採用 |
|---|---|---|---|---|
| **① Library** (採用) | なし | full | 1 セッション | ✅ |
| ② Metaprogram | なし | full | 1 ヶ月 | 将来 |
| ③ Fork (Prop8 kernel) | 大規模 | 破断 | 数年 | **却下** |

戦略 ③ は Mathlib 200,000+ 定理を全廃するため実用上自滅。チャット版 Claude が「Rei が Lean5 を作っている」と hallucinate していたが、実際は ③ ではなく ① を採用.

## 設計上の正直な制限

- `and` / `or` の operational priority ordering により、「直感的に成り立ちそう」な式 (例: `NEITHER ∧ a = NEITHER`) が `a = FALSE` で破綻 (FALSE absorption が勝つ)
- そういった非ユニバーサル式は restricted-quantifier theorem として正直に明示 (例: `and_NEITHER_left_no_FALSE`)
- 詳細は README "Asymmetric semantics" 節 + 論文 § 4

## 累計

- 論文累計: **76 本** (Papers 1-77, 56/59 欠番)
- 全 4/4 サイト完全投稿
- D-FUMT₈ 三角 anchor 完成: Schnorr (Paper 69) + QuTiP (75/76) + Lean (77)

## 戦略的含意

1. **世界初の公開 8値論理 Lean 4 ライブラリ** (我々の知る限り)
2. **Rei の D-FUMT₈ proof-theoretic anchor 完成** — 残り未着手なし
3. Mathlib 非依存で **5 秒 build** = 他研究者の採用障壁が極小
4. Apache-2.0 で **fork / 改変 / 商用利用 全て自由**

## 次手候補

1. **Paper 73 / 74 を LeanDFumt で書き直す** (β-shift discriminator FUNNEL を `asProp .BOTH` で表現等)
2. **Metaprogram tactics 追加** (`dfumt8_simp`, `neither_intro`) — 戦略 ②
3. **Mathlib operator instances** (DFUMT8 を CommMonoid/Lattice として) — 慎重設計要
4. **Lean Zulip 投稿** — コミュニティ周知