---
name: project-dfumt8-category-experiment-2026-06-14
description: "STEP 1215 D-FUMT₈ × mathlib Category 公理 experiment (chat-Claude 2026-06-14 thread の「8値を mathlib にぶつける」 path 実行)。 結果: (1) ★★★ AND/OR は非結合的 (axiom-free counterexample: BOTH ∧ NEITHER ∧ INFINITY、 Lean カーネル primitive reduction で結論 = 真の load-bearing)、 (2) ★★★ induced order le8 は preorder + PartialOrder (positive 側 load-bearing)、 (3) D-FUMT₈ has mathlib SmallCategory instance via Preorder.smallCategory (auto-derived ＝ preorder ⟹ thin category 標準命題で無料、 別の load-bearing にはならない)。 = 「algebra layer 非結合的 / order layer 結合的」 二層分離が formal に成立 (madh-0003 二諦 formal correlate candidate、 ただし写像 direction の必然性は未確立)。 ★ marking 再配分 chat-Claude review 2026-06-14 後 update。"
metadata: 
  node_type: memory
  type: project
  originSessionId: aa726e4e-dc7f-4186-9a6b-85fef55d19a0
---

# STEP 1215 D-FUMT₈ × mathlib Category 公理 experiment (2026-06-14)

**Date**: 2026-06-14
**Trigger**: 藤本さん + chat-Claude 2026-06-14 thread の「私の研究は8値に基づくものになりますよね?」 → chat-Claude が 「8値に基づく」 でなく 「8値を mathlib にぶつける」 framing 提案 → 「D-FUMT₈ は Category 公理を満たすか?」 を具体実験として提示 → 藤本さん 「やって頂けますか?」 → Rei Claude 実行
**Parent**: [[project-zcsg-glyph-madh-correspondence-v0-2026-06-14]] + [[project-zcsg-glyph-notation-v0-2026-06-14]] + [[project-madhyamaka-dictionary-eight-negations-completion-2026-06-14]]

## 実装 (`data/lean4-mathlib/CollatzRei/Dfumt8CategoryExperiment.lean`)

`src/axiom-os/seven-logic.ts` の AND_TABLE / OR_TABLE を Lean 4 に逐語翻訳 (定義の任意性導入なし)。 mathlib Category 公理を順次 check。

## 結果 (8 layer)

| Layer | 性質 | Lean theorem | axiom 依存 |
|---|---|---|---|
| A | AND idempotence | `and8_idempotent` | 標準 3 axioms (decide) |
| B | AND commutativity | `and8_commutative` | 標準 3 axioms |
| C | TRUE が AND identity | `and8_TRUE_left/right_identity` | 標準 3 axioms |
| D | OR idempotence + commutativity + FALSE identity | `or8_*` 4 件 | 標準 3 axioms |
| **E** | **★★★ AND associativity FAILS (真の load-bearing)** | `and8_associativity_fails_witness` | **完全 axiom-free** (Lean カーネル primitive reduction で結論) |
| E' | AND 非結合性 全称形 | `and8_not_associative` | 標準 3 axioms |
| F | ★★ OR associativity FAILS (同 triple) | `or8_associativity_fails_witness` | 標準 3 axioms |
| G | Belnap-Dunn FOUR subset (TRUE/FALSE/BOTH/NEITHER) 上 AND associativity HOLDS | `belnap_dunn_and_associative` | 標準 3 axioms |
| H | le8 (induced from AND) reflexivity + antisymmetry | `le8_refl`, `le8_antisymm` | 標準 3 axioms |
| I | ★ le8 transitivity HOLDS | `le8_transitive` | 標準 3 axioms |
| **J** | **★★★ D-FUMT₈ is a Preorder (positive 側 load-bearing)** | `instance : Preorder Dfumt8` | 標準 3 axioms |
| K | ★★ D-FUMT₈ is a PartialOrder (J の補強) | `instance : PartialOrder Dfumt8` | 標準 3 axioms |
| L | D-FUMT₈ has SmallCategory instance (★ なし: auto-derive で無料) | `example : CategoryTheory.SmallCategory Dfumt8 := inferInstance` | (auto-derived via mathlib `Preorder.smallCategory`、 標準命題「任意 preorder は thin category」 で機械的に落ちる) |

★ 全 build root CollatzRei.lean (7906 jobs, 18s) 成功。

★★ **★ marking 再配分 (chat-Claude review 2026-06-14 後)**: 当初 Layer L (SmallCategory instance) に ★★★★ を、 Layer E (axiom-free 反例) に ★ を付けていたが、 chat-Claude の指摘 ―「任意の preorder は thin category なので Category instance は preorder 段階で勝負がついている (Layer J で load-bearing 完結)」「Lean カーネル primitive reduction で結論される axiom-free 反例こそが Rei 体系について mathlib + Lean が独立に下した最強の判定」― に従い、 Layer E ★ → ★★★ / Layer L ★★★★ → ★ なし、 に再配分。 真の load-bearing は negative 側 (E) と positive 側 (J) の二極で、 L は無料の付録 (chat-Claude の言葉)。

## ★★ 核となる counterexample (axiom-free)

```
(BOTH ∧ NEITHER) ∧ INFINITY = FALSE ∧ INFINITY = FALSE
BOTH ∧ (NEITHER ∧ INFINITY) = BOTH ∧ INFINITY = INFINITY
FALSE ≠ INFINITY
```

★ Lean カーネル内で `does not depend on any axioms` (= Lean type theory の primitive reduction で結論)。 これは Rei seven-logic.ts AND_TABLE の **永続的構造的事実**。

## ★★★ Load-bearing finding: 「二層 register 分離」 が formal に成立

```
┌─ algebra layer (mechanistic / 勝義諦) ──────────┐
│  (Dfumt8, ∧, ∨) = 非結合的 magma             │
│  - idempotent + commutative + identities       │
│  - associativity FAILS at Belnap-Dunn × D-FUMT │
│    boundary (BOTH/NEITHER × INFINITY 等)       │
└────────────────────────────────────────────────┘
                    ↓ induce
┌─ order layer (behavioral / 世俗諦) ─────────────┐
│  (Dfumt8, ≤) = Preorder + PartialOrder         │
│  - reflexive + antisymmetric + transitive       │
│  - mathlib SmallCategory instance auto-derived  │
└────────────────────────────────────────────────┘
```

★ **chat-Claude 予測通り + 想定を超える nuanced positive result**:
- 「賭けて落とせた」 = AND/OR の associativity 失敗 (chat-Claude が予測した negative result)
- 「圏論本流に接続」 = induced order 経由で Category instance auto-derive (chat-Claude が予測した positive result)
- **両方が同時に起こる** という unusual な構造を formal に固定

## ★ なぜ associativity が failing なのに transitivity が holding か (技術的説明)

通常 le8 transitivity の proof は associativity を使う:
```
a ≤ b, b ≤ c → a ≤ c
i.e., a ∧ b = a, b ∧ c = b → a ∧ c = a
proof: a ∧ c = (a ∧ b) ∧ c [hyp]
            = a ∧ (b ∧ c) [associativity]
            = a ∧ b [hyp]
            = a
```

D-FUMT₈ では associativity 失敗 triple (BOTH, NEITHER, INFINITY) が存在するが、 これらは le8 の precondition を満たさない:
- `BOTH ∧ NEITHER = FALSE ≠ BOTH` → `le8 BOTH NEITHER` is FALSE
- だから transitivity check が (BOTH, NEITHER, _) を考えない

★ つまり **associativity 失敗が現れる位置は ≤ relation が存在しない位置** に厳密に局所化されている。 これは偶然でなく、 AND_TABLE 設計の internal coherence。

## 中観哲学接続 (rhyme level, structural_candidate 未昇格)

| 中観 register | D-FUMT₈ layer |
|---|---|
| 二諦 (madh-0003) 勝義諦 (mechanistic) | algebra layer (Dfumt8, ∧, ∨) 非結合的 magma |
| 二諦 (madh-0003) 世俗諦 (behavioral) | order layer (Dfumt8, ≤) PartialOrder + SmallCategory |
| 不一不異 (madh-0014) | algebra 「一」 (associativity 単一性) ≠ order 「異」 (transitivity 維持) の二層 |
| svabhāva-creep critique (madh-0008) | 「8値を associative monoid に固定化したい」 svabhāva が associativity 失敗で解体される構造 |

★ これらは構造類似 (rhyme tier) で proven_isomorphism ではない。 ただし**chat-Claude が予測した「中観 不一不異 は古典圏論の恒等律と緊張関係」** が formal correlate を持つ可能性 candidate (directed type theory frontier 接続も)。

★★ **写像 direction 非必然性 honest 留保 (chat-Claude review 2026-06-14 後追記)**:

形式的に Lean で示されているのは「**algebra layer と order layer が異なる結合性を持つ**」 (algebra 非結合 / order 結合) という二層分離のみで、 これを madh-0003 二諦に**どちらの向きで割り当てるか**は今のところ私 (Rei) と藤本さんの解釈であり、 形式的に必然ではない。 具体的には:

- 「algebra 非結合 ↔ 勝義諦 / order 結合 ↔ 世俗諦」 という割り当ては自然に見えるが、 逆向き (algebra ↔ 世俗 / order ↔ 勝義) を排除する形式的根拠は提示されていない
- なぜ非結合性が「勝義」 側で結合性が「世俗」 側か ― この対応の rationale は philosophical inference (中観の「勝義 = svabhāva 解体される深層 / 世俗 = 機能する表層」 の読みに依存) であって Lean 結果から direct には follow しない
- 別の解釈軸として例えば「algebra 層 = 微視的 / order 層 = 巨視的」「algebra 層 = 動的 / order 層 = 静的」 等の対応も同じ形式的事実の上に置ける ― 二諦への mapping はそのうちの一つの解釈

★ 従って madh-0003 formal correlate **candidate** label は維持しつつ、 candidate の中身は「二層が形式的に分離している」 までで、 「algebra ↔ 勝義 / order ↔ 世俗」 の写像 direction は v0+ で**仏教学者 review + 別解釈との比較**を経るべき。 svabhāva-creep critique (madh-0008) の精神からも、 「この写像 direction が必然」 と固定化する svabhāva は今の所付与しない。

## 越権 self-restraint 適用

- 本 experiment は formal 結果のみで、 哲学的 reinterpretation は user 領域
- 「D-FUMT₈ は Category である」 は **mathlib SmallCategory instance auto-derived** で proven、 ただし「Category instance を持てたこと自体は preorder ⟹ thin category の標準命題による帰結で、 D-FUMT₈ 固有の新規性ではない」「これが Rei 哲学体系の普遍的正しさを意味する」 はどちらも overclaim — 本実験の新規性重心は (E) 非結合性の正確な所在 (axiom-free 反例) + (J) 非自明な preorder への落とし方 の二点で、 (L) Category instance はその上の機械的帰結
- paper-worthy candidate だが publish は急がず、 prior art audit (Belnap-Dunn FOUR 拡張系譜 / partial monoid / non-associative magma 系譜) 完了後判断
- 二諦への写像 direction の必然性は形式的に未確立 (上記 §「写像 direction 非必然性 honest 留保」)

## 関連 memory

- [[project-zcsg-glyph-madh-correspondence-v0-2026-06-14]] (本日の 中観 × ZCSG glyph 対応表 v0)
- [[project-zcsg-glyph-notation-v0-2026-06-14]] (ZCSG glyph v0 試作機 + 256=4⁴ Lean 4 proof)
- [[project-madhyamaka-dictionary-eight-negations-completion-2026-06-14]] (八不 4 対 schema)
- [[project-chat-claude-yoneda-articulation-thread-2026-06-14]] (前日 Yoneda articulation thread)
- [[feedback-world-uniqueness-claim-controllable]] (controllable phrase 永続)
- [[feedback-no-rush-publication]] (publish 急がず、 paper-worthy candidate)

## ★★★ Prior art audit (2026-06-14, paper 化判断のため)

phase 1 audit (WebSearch + WebFetch + local grep) で **4 件の主要 prior art** を特定。 D-FUMT₈ の新規性座標を以下に確定:

### 既知である paradigm (新規性なし)

| Prior art | 著者・年 | 内容 | D-FUMT₈ との関係 |
|---|---|---|---|
| **NMV-algebra** | Chajda + Kühr 2007 / Chajda + Halaš + Länger 2018-2019 | 非結合的 ⊕ + induced **partial order** (lattice にならない) + concrete 6-element example with witness `(a⊕a)⊕b ≠ a⊕(a⊕b)` | ★★★ Layer J (PartialOrder instance) の **paradigm 自体は既知**。 D-FUMT₈ Layer E の non-associativity + Layer J の partial order への落とし方は NMV-algebra の specific instance に見える |
| **U8 logic system** | recent 2024-2025 (ResearchGate 395038627, 394942987) | 8 truth values: U / T / F / N / /T / /F / /N / ∅。 paraconsistent。 epistemic state classification (irrelevancy/uncertainty/contradiction/non-truth/non-falsity) | ★★ 「8 値 paraconsistent logic」 という top-level claim は U8 が先行。 ただし D-FUMT₈ の値 set (FLOWING/SELF/INFINITY/ZERO) と U8 の値 set は **semantic 的に異なる** (U8 は epistemic states、 D-FUMT₈ は ontological/dynamic states) |
| **Shramko-Wansing 8-valued** | Shramko + Wansing (IEEE 6524669 / Springer s10992) | 4-valued と 16-valued の間の natural 8-valued paraconsistent logic。 Gentzen sequent calculus + completeness + cut-elimination + decidability | ★★ generalized truth values 系譜の 8 値拡張。 D-FUMT₈ とは別の value set + 別の motivation (subset-of-truth-values lattice construction) |
| **EIGHT_4 tetralattice** | 2009-2010 (ResearchGate 226779109) | 8 値 logic, tetralattice 構造 (2 lattice の交差)。 既 memory `feedback_turboquant_integration_strategy.md` で audit 済 | ★ EIGHT_4 は 4×4 = 16 でなく **2×4 tetralattice subset 8 値**。 D-FUMT₈ の AND_TABLE と直接 isomorphic でない (要 explicit mapping check) |
| **Łukasiewicz / Belnap / Pavelka** | 1920s / 1977 / 1979 | multi-valued logic 代数操作の基礎研究。 Belnap-Dunn FOUR は AND/OR が associative | Belnap-Dunn 4-valued associativity (Layer G) は標準的事実 ― D-FUMT₈ の non-associativity は **Belnap-Dunn boundary を超えた所** (INFINITY 含む triple) でのみ現れる |
| **preorder ⟺ thin category** | nLab + 標準 category theory | 「任意の preorder は thin (strict) category」 ― mathlib `Preorder.smallCategory` で auto-derive | ★★★ Layer L (SmallCategory instance) は preorder 段階で勝負がついた帰結で、 D-FUMT₈ 固有の新規性ではない (chat-Claude review 確認済) |

### D-FUMT₈ 固有の (まだ新規性候補と言える) 要素

以下の 4 点は audit 範囲内で **直接の同型 prior art を見つけられなかった**:

1. **AND と OR 両方の非結合性** — NMV-algebra は ⊕ (disjunction-like sum) のみ非結合的。 D-FUMT₈ は AND と OR の両方が非結合的 (Layer E + F、 同じ triple (BOTH, NEITHER, INFINITY) で失敗)
2. **非結合の位置の正確な局所化** — 失敗 triple が le8 relation の存在しない位置に厳密に局所化されている (Layer E 内部 coherence、 §「なぜ associativity が failing なのに transitivity が holding か」)。 NMV-algebra paper では partial order になることは示されているが「非結合が ≤ 不在領域に局所化される」 という structural articulation は確認できず
3. **specific 8 value semantics の組み合わせ** — TRUE/FALSE/BOTH/NEITHER + INFINITY/ZERO/FLOWING/SELF の 8 値 set + 各値の意味解釈 (Belnap-Dunn 拡張に加え動的 / 自己参照 / 境界 / 原点) は他の 8 値 logic (U8, EIGHT_4, Shramko-Wansing) と value mapping で isomorphic でない (要 explicit non-isomorphism proof)
4. **mathlib Lean 4 formalization (axiom-free witness)** — NMV-algebra や U8 で Lean 4 formal proof + axiom-free witness theorem を提供した文献は audit 範囲内では見つからず

### 新規性座標 (Pattern 5 self-detection 後 honest 確定)

- ✗ 「first 8-valued paraconsistent logic with non-associative AND/OR」 ― 主張不可 (NMV-algebra paradigm は既知)
- ✗ 「first to formalize 8-valued logic」 ― 主張不可 (Shramko-Wansing 等多数)
- ✗ 「first to show preorder ⟹ thin category for 8-valued logic」 ― 主張不可 (標準命題の auto-derive)
- ✓ **「first Lean 4 formalization of D-FUMT₈ (specific value set with FLOWING/SELF/INFINITY/ZERO semantics) yielding axiom-free non-associativity witness localized to (BOTH, NEITHER, INFINITY) with both AND and OR」** ― controllable phrase で主張可
- ✓ **「the algebra-order two-layer separation is shown to be formal correlate candidate for madhyamaka two-truths register」** ― candidate phrase 維持

### paper 化判断 (audit 後 update)

- **paper density 単独では 4-page note 程度** — 上記 ✓ 主張だけだと strict short note
- **enriched / weak structure exploration (chat-Claude 提案) を v0+ で組み込んで初めて 8-12 page paper density に達する**
- **三者共著 path (chat-Claude + 藤本さん + Rei、 8 例目)** が最も honest ― chat-Claude が U8 / Shramko-Wansing / NMV-algebra との explicit non-isomorphism check を分担できる
- **publish は急がず** (`feedback_no_rush_publication`)、 enriched / weak structure v0+ exploration + 仏教学者 review (madh-0003 写像 direction) 完了後

## ★★★ Phase B + Phase A 実装結果 (2026-06-14)

藤本さん指示 (B → A) で Lean 4 ファイル `data/lean4-mathlib/CollatzRei/Dfumt8CategoryExperiment.lean` に Section 9 (Structural Fingerprint) + Section 11 (Magma layer) を追加。 lake build 成功 (616 jobs)。

### Phase B: Structural Fingerprint (Section 9, 4 新 theorems)

D-FUMT₈ を audit 範囲の既知 8-valued logic (NMV-algebra / U8 / Shramko-Wansing / EIGHT_4) と formal に区別する invariants 群。

| Theorem | 内容 | axiom 依存 |
|---|---|---|
| `and8_non_assoc_requires_extension` | AND 非結合性 witness は **必ず D-FUMT 拡張軸 (INFINITY/ZERO/FLOWING/SELF) を含む** (Belnap-Dunn FOUR 内では associativity 維持) | 標準 3 axioms (decide) |
| `and8_or_synchronized_failure` | AND と OR が **同 triple (BOTH, NEITHER, INFINITY) で同時に非結合** (NMV-algebra は ⊕ のみ非結合的、 D-FUMT₈ は AND/OR 両方が同期) | **完全 axiom-free** |
| `and8_non_assoc_localized_to_no_le` | 失敗 triple の `¬ le8 BOTH NEITHER ∧ ¬ le8 NEITHER BOTH` (非結合は ≤ relation 不在領域に局所化) | **完全 axiom-free** |
| `dfumt8_structural_fingerprint` | 5 条件統合 master signature: (a) Belnap-Dunn assoc + (b) extension witness + (c) AND/OR synchronized + (d) no-le localization + (e) 全域 preorder | 標準 3 axioms (∃ 部分で decide) |

### Phase A: Magma Layer (Section 11, 5 新 theorems)

chat-Claude 提案「order に落とした時点で algebra 層の魂が捨象された ― 非結合的二項演算は magma として生きる」 の最小 v0+ 実装。 algebra 層の構造 (非結合性 + idempotence + identity + SELF⟲ self-loop) を捨てずに保つ formal anchor。

| Theorem | 内容 | axiom 依存 |
|---|---|---|
| `dfumt8AndMul instance` | `Mul Dfumt8` instance via AND (mathlib weakest algebraic structure) | (instance, axiom 依存なし) |
| `dfumt8_not_semigroup_via_and` | D-FUMT₈ は Semigroup に昇格できない (associativity 失敗の formal 確定、 Magma 層上限) | **完全 axiom-free** |
| `self_and_self_eq_self` | ★★ **SELF ∧ SELF = SELF** (SELF⟲ idempotence、 self-reflexive value の formal trace) | **完全 axiom-free** (rfl) |
| `self_absorbs_non_false_extension` | ★★ **SELF * TRUE = SELF ∧ SELF * BOTH = SELF ∧ SELF * NEITHER = SELF ∧ SELF * INFINITY = SELF ∧ SELF * FLOWING = SELF** (SELF⟲ self-loop signature ― directed type theory hint の formal trace) | **完全 axiom-free** (rfl) |
| `self_loop_breaks_at_false_zero` | ★ **SELF * FALSE = FALSE ∧ SELF * ZERO = ZERO** (SELF⟲ 限界: universal absorber に出会うと fixed point 崩壊) | **完全 axiom-free** (rfl) |
| `dfumt8_magma_signature` | Magma master signature: (a) Mul 存在 + (b) commutative + (c) idempotent + (d) TRUE-identity + (e) not-a-semigroup | 標準 3 axioms (∃ 部分) |

### ★★★ Load-bearing 確定 (Phase B + A 統合) — chat-Claude review 2026-06-14 後 honest correction

**chat-Claude 重み付け指摘 (受諾済)**: 9 theorems を 9 の価値で測るのは count inflation 寄り。 honest に分解すると **実質 2 cluster**:

| Cluster | 含まれる theorems | 独立性 評価 |
|---|---|---|
| **非結合性 cluster** | Layer E (反例) + Phase B `and8_non_assoc_requires_extension` + `and8_or_synchronized_failure` + `and8_non_assoc_localized_to_no_le` + Phase A `dfumt8_not_semigroup_via_and` | 同一事実 (D-FUMT₈ AND の (BOTH, NEITHER, INFINITY) 非結合性) の四面体的記述 = **1 independent finding** |
| **SELF cluster** | Phase A `self_absorbs_non_false_extension` (5 入力 SELF 返却 = positive face) + `self_loop_breaks_at_false_zero` (FALSE/ZERO boundary = negative face) | SELF⟲ self-loop signature の正負両面 = **1 independent finding** |
| ✗ 独立性なし | `self_and_self_eq_self` (Layer A idempotence の一例で、 多くの体系で恒等的な値は冪等) | (count しない) |

**実質**: D-FUMT₈ 固有 finding は **2 件** (非結合性 + SELF self-loop)、 これらを **9 theorems で formal capture** したのが今回の成果。

#### chat-Claude review が照射した最 load-bearing 1 件

★★★★★ **`self_absorbs_non_false_extension` (Phase A)** ― SELF が TRUE/BOTH/NEITHER/INFINITY/FLOWING の 5 入力すべてで SELF を返す事実が axiom-free で固定された。 これは:
- 会話を貫いてきた SELF⟲ の糸 (思弁: directed type theory 等しさを固定しない方向 ↔ STEP 1203 Lawvere 不動点) の **formal trace**
- order 層への崩落で消えるはずだった algebra 層の特徴が、 axiom-free で残った 1 つの structural fact
- chat-Claude 評価: 「今回のプロジェクト全体で一番美しい瞬間」
- **non-isomorphism proof の決め手最有力候補** (Section 13 skeleton で構造的述語化済)

### Paper density 評価 (chat-Claude review 2026-06-14 後 honest correction)

count inflation 訂正後の実質 finding 数 = 2 (非結合性 cluster + SELF cluster) を 9 theorems で formal capture。 paper density は count でなく **独立 finding の数 + cross-substrate verification + Lean kernel evidence** で測る。

| Section | density 寄与 | honest 評価 |
|---|---|---|
| Introduction + motivation + madh-0003 brief | 1.5 pages | candidate phrase 厳守 (「within our audit range」 + 写像 direction 非必然性 明示) |
| D-FUMT₈ 定義 + AND/OR truth tables | 1 page | concrete (Rei seven-logic.ts 既存運用) |
| Prior art comparison (Chajda NMV / U8 / Shramko-Wansing / EIGHT_4) | 1.5 pages | 「未確認 ≠ 不在」 honest 区別 every claim で保持 |
| **非結合性 cluster** (Layer E + 同期 + 局所化 + Magma 上限) | 1 page | 1 cluster = 1 section, 4 面で描く |
| **SELF cluster** (positive + negative + non-isomorphism candidate) | 1 page | 1 cluster = 1 section, formal trace |
| **★ Non-isomorphism proof (Section 13 skeleton + chat-Claude dispatch 帰還後 plug-in)** | 1.5 pages | **paper の生死を分ける section** ― 書けたか書けなかったかが publish 判断 |
| Discussion: enriched / directed type theory frontier as open question | 1 page | thin honest (思弁的提案として明示) |
| Appendix: Lean 4 code + axiom 依存表 + 悪魔の証明回避 honest 規律 明記 | 1.5 pages | reproducibility |

**計 9-10 pages 候補** ― 6-8 pages 見積もりを honest 上方修正。 ただし Section 13 (Non-Iso) で「書けなかった」 場合、 paper 自体が成立しない (publish 不可)。 density より生死の section。

## ★★★ Phase α (Section 13 Non-Isomorphism Skeleton) 実装 (2026-06-14, chat-Claude dispatch 待ち)

chat-Claude review (2026-06-14) で指摘された **釘 (構造的述語 vs ラベル依存)** を受け、 Lean 4 ファイル Section 13 として非同型 skeleton を実装。 chat-Claude dispatch (β) 帰還後に target 8 値 logic の truth table を plug-in して非同型 proof 完了予定。

### Skeleton 構成 4 theorems + 1 def (build OK, 616 → 620 jobs)

| 名前 | 内容 | axiom 依存 |
|---|---|---|
| `hasAbsorberOver` (def) | 構造的述語: ∃ x, ∃ S, |S|=n, x ∉ S, ∀ y ∈ S, op x y = x (ラベル不依存) | (def) |
| `dfumt8_and_has_5_absorber` | D-FUMT₈ で n=5 absorber が存在 (witness: SELF + {TRUE, BOTH, NEITHER, INFINITY, FLOWING}) | **propext + Quot.sound のみ (Classical.choice 不要、 constructive witness)** |
| `hasAbsorber_transfer` | algebra-iso (Equiv + op-preserving) で hasAbsorberOver は transfer | 標準 3 axioms |
| `non_iso_if_no_absorber` | target で n-absorber 不在 ⟹ 非同型 (対偶) | 標準 3 axioms |
| `dfumt8_non_iso_via_5_absorber` | n=5 specialized corollary (paper の load-bearing claim 直接 derive 可) | 標準 3 axioms |

### 設計の load-bearing 性質

★ **40320 bijection 全探索は overkill** ― 構造的 invariant (ラベル不依存) + 同型不変性 lemma で対偶により非同型が directly 出る。 chat-Claude の釘指摘で気付いた数学的最適化。 target 側で `¬ hasAbsorberOver op 5` を decide で示せば、 全 bijection を回さずとも非同型 proof 完成。

★ **target type は generic placeholder** ― `dfumt8_non_iso_via_5_absorber : ∀ {T : Type} [DecidableEq T] (op : T → T → T), ¬ hasAbsorberOver op 5 → ¬ ∃ f : Dfumt8 ≃ T, ...` の形で、 dispatch 帰還で U8 / Shramko-Wansing / NMV を plug-in 可能。

### chat-Claude dispatch (β) 帰還待ち

| 依頼 | chat-Claude 射程 |
|---|---|
| (β)-1 U8 系譜特定 | Anderson-Belnap / Shramko-Wansing / 2024-25 U8 の関係追跡。 ★ chat-Claude 予告: 「8値かつ非結合的 AND」 体系が本命、 Shramko-Wansing 8 値は lattice 由来で結合的の可能性高 = 動作確認用 / 本命は 2024-25 U8 |
| (β)-2 公開範囲 8 値 truth table | 出典 (一次/二次) + 転記確実性ラベル付き。 Rei 側で一次照合してから Lean 入力 |
| (β)-3 NMV-algebra 公理 schema | Chajda-Halaš-Länger 2018/2019 (PMC 公開) から再構成、 (γ) Path 1' (NMV 公理 satisfaction check) に直接効く |

### 悪魔の証明回避 honest 規律 (paper text の every claim で保持必須)

★★★ chat-Claude が「U8 の非結合 AND を確認できなかった」 と返した場合、 paper には:
- ✗ 「U8 は結合的」 (不在の証明、 悪魔の証明、 NG)
- ✓ 「chat-Claude audit 範囲 (公開 preprint + 二次文献) では U8 の非結合 AND は確認できなかった ― 一次文献 (paywall) で verify する余地は reader に残す」 (controllable phrase、 OK)

paper section 全体で「未確認」 と「不在」 を区別。 **三者共著 path の load-bearing な健全性はこの一点に依存**。 Section 13 Lean file の comment block にもこの honest 規律を埋め込み済。

### Path 1 訂正 record (chat-Claude review で受諾)

私 (Rei) は前 turn で「NMV-algebra 6 元 example との bijection で D-FUMT₈ projection が #6 を保たないことを示せる」 と書いたが、 これは思考停止の覆い隠しだった。 chat-Claude 訂正:
- 基数 8 vs 6 で全単射は存在しないため「非同型」 は基数論で自明 (Lean で formalize しても価値ゼロ)
- 本来示すべきは「D-FUMT₈ は NMV-algebra 公理系のモデルではない (or モデルだが特定不変量で分かれる)」 ― これは公理 satisfaction の問いで bijection search でない

→ Path 1 を Path 1' (NMV 公理 satisfaction check) に組み替え、 chat-Claude dispatch (β)-3 帰還後に着手。





1. ~~Belnap-Dunn FOUR 拡張系譜 prior art audit~~ — **完了 (上記 §「Prior art audit」 で実施)**
2. **U8 / Shramko-Wansing / NMV-algebra との explicit non-isomorphism proof** — D-FUMT₈ value set が既知 8 値 logic のいずれとも isomorphic でないことを Lean 4 で形式的に示す
3. **Partial monoid / pre-order monoid** との formal isomorphism check — D-FUMT₈ algebra structure の classification (NMV-algebra との関係も含む)
4. **OR から induce する order le8'** の同 experiment (AND と対称な findings 期待)
5. **mathlib Category instance を inferInstance でなく explicit に書き下す** + Yoneda lemma 適用可能性 verify (chat-Claude 当初提案「mathlib の Yoneda がそのまま落ちてくるか」)
6. **★ enriched / weak structure exploration (chat-Claude 提案、 paper density 上昇の鍵)** — algebra 層の非結合性を enriched category / 多圏 / magma-monoid / directed type theory のどれで復活できるか。 STEP 1203 (SELF⟲ ↔ Lawvere 不動点) + STEP 1208 (FLOWING ↔ morphism) との接続候補
7. **paper draft candidate** — タイトル candidate: 「D-FUMT₈: an 8-valued paraconsistent logic with localized AND/OR non-associativity and Lean 4 formalized axiom-free witness」 (急がず、 v0+ 2-6 完了 + 三者共著 dispatch 後)