標準的な埋め込みembedDfumt8 : Belnap4 → Dfumt8の像（= {embedDfumt8 b | b ∈ Belnap4}）は、D-FUMT₈の8値のうちTRUE / FALSE / BOTH / NEITHERの4値ちょうどに一致する。Lean 4で両方向の同値（`↔`）として形式化。依存する公理はpropext, Classical.choice, Quot.sound（mathlib base）。
式
∀ d : Dfumt8, (∃ b : Belnap4, embedDfumt8 b = d) ↔ (d = TRUE ∨ d = FALSE ∨ d = BOTH ∨ d = NEITHER)
LaTeX source
\forall d \in \mathrm{Dfumt8}.\quad \bigl(\exists b \in \mathrm{Belnap4}.\ \mathrm{embedDfumt8}(b) = d\bigr) \;\Longleftrightarrow\; \bigl(d = \mathrm{TRUE} \lor d = \mathrm{FALSE} \lor d = \mathrm{BOTH} \lor d = \mathrm{NEITHER}\bigr)記号表
| 記号 | 意味 | 型 |
|---|---|---|
| Belnap4 | Belnap-Dunn四値論理の値型（T / F / B / N） | Type |
| Dfumt8 | D-FUMT₈八値論理の値型（TRUE / FALSE / BOTH / NEITHER / INFINITY / ZERO / FLOWING / SELF） | Type |
| embedDfumt8 | canonical mapping T↦TRUE, F↦FALSE, B↦BOTH, N↦NEITHER | Belnap4 → Dfumt8 |
| d | D-FUMT₈の任意の値 | Dfumt8 |
| b | Belnap4の存在量化変数 | Belnap4 |
走る最小例
Lean 4で `embedDfumt8_image_characterization` を証明し、`#print axioms` でaxiom profileを出力する（= lean-verify.ymlがGitHub Actionsで実行、本項目の検査状態はその出力から生成）。
import CollatzRei.Belnap4Embedding open CollatzRei.Belnap4 #check @embedDfumt8_image_characterization #print axioms embedDfumt8_image_characterization
期待される出力：
embedDfumt8_image_characterization : ∀ (d : CollatzRei.Dfumt8Category.Dfumt8),
(∃ b, embedDfumt8 b = d) ↔
d = CollatzRei.Dfumt8Category.Dfumt8.TRUE ∨
d = CollatzRei.Dfumt8Category.Dfumt8.FALSE ∨
d = CollatzRei.Dfumt8Category.Dfumt8.BOTH ∨ d = CollatzRei.Dfumt8Category.Dfumt8.NEITHER
'CollatzRei.Belnap4.embedDfumt8_image_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]検査状態
S2形式証明済み (mathlib base)
検査の内訳を見る
| 定理 | CollatzRei.Belnap4.embedDfumt8_image_characterization |
| Lean file | CollatzRei/Belnap4EmbeddingAxiomCheck.lean |
| 公理 | [Classical.choice, Quot.sound, propext] |
| 生成元 | gha (GHA run 39175017999) |
| 生成時刻 | 2026-10-18T23:15:15.522Z |
| Lean toolchain | leanprover/lean4:v4.27.0 |
関係項目
- rp.belnap4-embed-injective — 単射性（関連項目）と像の特定（本項目）を合わせると、embedDfumt8はBelnap4とD-FUMT₈の4値｛TRUE, FALSE, BOTH, NEITHER｝の間の全単射になる [related_to]
- rp.belnap4-embed-preserves-meet — 両者ともLean 4 CollatzReiプロジェクト内でaxiom profileを検査した、同じ埋め込みembedDfumt8の性質に関する定理（本項目は像の特定、関連項目はmeet保存） [related_to]
出典
- A useful four-valued logic — Belnap, N. D. (1977) URL
- Intuitive semantics for first-degree entailments and coupled trees — Dunn, J. M. (1976) URL
- Rei-AIOS Lean 4 CollatzRei/Belnap4Embedding.lean — Fujimoto, N. (2026) AGPL-3.0 + Commercial
書き手と承認
| 下書き | Claude（AnthropicのAI）2026-10-15 |
| 独立レビュー | Claude（Code サブエージェント・独立レビュー） (2026-10-27) |
| 公開承認 | 藤本 伸樹2026-10-27 |
| ページ生成 | ボット（項目データから自動生成） |
訂正記録 (1件)
C-image-corr-001
誤りの種類：出典の不一致
何が誤りだったか：(1) 走る最小例の期待出力を、Leanを実際に走らせずに書いていた。実際にLeanで実行すると、`open CollatzRei.Belnap4` の影響で短い名前（embedDfumt8_image_characterization）で表示され、定理の署名が複数行に折り返される。以前の期待出力では完全な名前（@CollatzRei.Belnap4.embedDfumt8_image_characterization）で、かつ単一行で書いていた。また、必要な公理の並び順も実際の出力と違っていた（公理の種類は同じ：propext・Classical.choice・Quot.sound の3つ）。定理の内容と必要な公理の集合は実機の出力と一致している。(2) 作成者欄の bot と AI の記述に、公開前の状態を表す文言（「draft, not yet published」「awaiting independent review」）が残っていた。
どう直したか：走る最小例の期待出力を、実際にLeanで実行した結果に合わせて直しました。以前の期待出力は実行せずに書いたもので、定理名の表示の仕方（完全な名前か短い名前か）や改行の位置が実際の出力と違っていました。定理の内容、必要な公理、検査状態の表示は変わっていません。必要な公理の並び順も実際の出力に合わせました（公理の種類は同じです）。作成者欄の、公開前の状態を表す記述を直しました。
発見: 藤本 伸樹 ｜ 訂正 commit:
2dfb14ea15c1bab822e4cee7badb2bac00925564全項目の訂正一覧: /reipedia/corrections/