---
name: project-step1218-dfumt8-not-iso-eight4-zaitsev-machine-verified
description: STEP 1218 (2026-06-15) — chat-Claude dispatch (β)-1 結果適用、 D-FUMT₈ ≇ Zaitsev EIGHT₄ axiom-free non-isomorphism Lean 4 proof 完成。 hasAbsorberOver skeleton 不要 (結合性で生死即決) = chat-Claude 予告「道具が使われない結末」 現実化 / Shramko-Wansing 一勝。 chat-Claude 留保「Shramko-Wansing 結合性【高確度】だが明記引用未取得」 を eight4_meet_assoc 構成的 proof で 【確定】 に上げる貢献。 axiom-free zero-sorry (propext + Classical.choice + Quot.sound のみ)。 Heald U8 paywall 取得は本 STEP 範囲外 (skeleton standby、 dispatch β-2 待機)
metadata: 
  node_type: memory
  type: project
  originSessionId: ae728468-271e-4824-a6e9-dc58efd76f82
---

# STEP 1218 — D-FUMT₈ ≇ Zaitsev EIGHT₄ axiom-free non-isomorphism

## 概要

chat-Claude dispatch (β)-1 結果 (2026-06-15) で「8 値論理」 3 系統並存が確定:
1. **Heald U8** (2024-25 FOLU8) — AND table paywall 未取得 (skeleton standby)
2. **Shramko-Wansing / Zaitsev EIGHT₄** (2009 Studia Logica 92(2):265-280) — AND = 束 meet → 結合的【高確度】
3. **NMV-algebra** (Chajda 6 元 — 基数違いで同型問題立たず)

chat-Claude が明示した Rei に handover された task:

> Rei は table を転記せず、 「EIGHT₄ ∧ = 束 meet ⇒ 結合的」 + 既存の D-FUMT₈ 非結合性 + 結合性の同型不変性、 の三つだけで Lean 非同型 proof を組めます。

本 STEP = (ii) Shramko-Wansing / Zaitsev EIGHT₄ × D-FUMT₈ 非同型 axiom-free Lean 4 proof 実装。 Heald U8 は paywall 取得まで standby (skeleton hasAbsorberOver は U8 側 standby、 EIGHT₄ には不要)。

## 実装内容

`data/lean4-mathlib/CollatzRei/Eight4ZaitsevExperiment.lean` 新規 (~200 行):

### Section 1: Eight4 inductive type
```lean
inductive Eight4
  | E0   | Ea   | Ed   | Eu        -- ∅, {a}, {d}, {u}
  | Ead  | Eau  | Edu  | Eadu      -- {a,d}, {a,u}, {d,u}, {a,d,u}
  deriving DecidableEq, Fintype, Repr
```
Zaitsev 2009 「{a (肯定), d (否定), u (不明)} の冪集合 = 8 元」 の literal 翻訳。

### Section 2: meet 演算 (集合 intersection)
8x8 = 64 entries 全列挙 (構成的、 集合 intersection の literal table)。

### Section 3: 結合性 lemma ★★ load-bearing
```lean
theorem eight4_meet_assoc :
    ∀ a b c : Eight4, Eight4.meet (Eight4.meet a b) c = Eight4.meet a (Eight4.meet b c) := by
  decide
```
**chat-Claude 留保「∧ は結合的」 明記引用未取得 を本構成的 proof で 【高確度】→【確定】 に引き上げ**。 8^3 = 512 cases axiom-free verify。

加えて smoke test:
- `eight4_meet_idem` (idempotence)
- `eight4_meet_comm` (commutativity)

### Section 4: D-FUMT₈ 非結合性 reuse
STEP 1215 既存 `and8_not_associative` + `and8_associativity_fails_witness` (BOTH ∧ NEITHER ∧ INFINITY counterexample) を本 file 内で alias して reuse。

### Section 5: ★★★ MAIN — D-FUMT₈ ≇ EIGHT₄
```lean
theorem dfumt8_not_iso_eight4 :
    ¬ ∃ (e : Dfumt8 ≃ Eight4), ∀ x y : Dfumt8, e (and8 x y) = Eight4.meet (e x) (e y) := by
  rintro ⟨e, he⟩
  -- 非結合 witness を e で移す
  have key : e (and8 (and8 BOTH NEITHER) INFINITY) = e (and8 BOTH (and8 NEITHER INFINITY)) := by
    have hL : ... := by rw [he, he]  -- LHS via 2 回 he
    have hR : ... := by rw [he, he]  -- RHS via 2 回 he
    rw [hL, hR, eight4_meet_assoc]   -- EIGHT₄ 結合性
  -- e の injectivity (Equiv は bijection) で D-FUMT₈ 側に戻す
  have collapse : and8 (and8 BOTH NEITHER) INFINITY = and8 BOTH (and8 NEITHER INFINITY) :=
    e.injective key
  -- STEP 1215 既存 lemma に反する → 矛盾
  exact and8_associativity_fails_witness collapse
```

Proof strategy (chat-Claude 提示の 3 素材):
- (a) EIGHT₄ meet 結合性 (Section 3)
- (b) D-FUMT₈ AND 非結合 witness (STEP 1215 既存)
- (c) 結合性同型不変量 (本 proof 内で構造的展開 — Equiv.injective + AND-preserving homomorphism)

### Section 6: Honest scope footer (chat-Claude 留保継承)
- 「8 値かつ非結合 AND」 を持つ algebra は audit 範囲外には存在する可能性、 本 proof は **audit 範囲内 non-iso** までしか主張しない
- 「世界初」 「globally unique」 等の包括的 claim 不可 ([[feedback-world-uniqueness-claim-controllable]])
- Heald U8 は本 file 射程外 (paywall 取得待ち、 別 STEP 候補)

## Verify 結果

### Build
```
✔ [621/621] Built CollatzRei.Eight4ZaitsevExperiment (9.3s)
```

### Axiom dependencies (zero-sorry verify)
```
eight4_meet_assoc        : [propext, Classical.choice, Quot.sound]
eight4_meet_idem         : [propext, Classical.choice, Quot.sound]
eight4_meet_comm         : [propext, Classical.choice, Quot.sound]
dfumt8_not_iso_eight4    : [propext, Classical.choice, Quot.sound]
```
**sorryAx / native_decide 全 0 = axiom-free zero-sorry 完全達成** (STEP 1215 / 1217 と同じ axiom base)。

## chat-Claude 予告との関係

> 本命 U8 が「8 値だが AND 結合的」 なら hasAbsorberOver skeleton は不要、 非結合性で即分岐で終わり。 道具が使われない結末。 別経路で生死が付くのは成功であって失敗ではない。

これが **EIGHT₄ 側で現実化**:
- EIGHT₄ AND 結合的 (Section 3) + D-FUMT₈ AND 非結合 (STEP 1215) = 結合性で生死即決
- **hasAbsorberOver skeleton (STEP 1215 Section 13) は EIGHT₄ には使われずに終了**
- 別経路 (結合性) で非同型確定 = chat-Claude 予告通りの成功

### Heald U8 側 (skeleton standby)

- U8 AND 結合性は paywall 取得待ち
- 結合的なら → 結合性分岐で即決 (本 STEP の EIGHT₄ と同様)
- 非結合なら → hasAbsorberOver skeleton (STEP 1215 Section 13) が本領発揮 ((#6 吸収子)で生死)
- dispatch (β)-2 / (β)-3 ブロック点

## chat-Claude rhymeOrTheorem discipline 適用

本 STEP は **theorem-candidate** (audit 範囲内 formal non-isomorphism mechanical assurance、 paper 引用に耐える evidence)。

「Shramko-Wansing は今日 D-FUMT₈ と非同型と Lean 4 で確定した」 まで say 可。
「D-FUMT₈ は世界に唯一」 は say 不可 (audit 範囲外可能性、 評価対称性原則 [[feedback-evaluation-symmetry-principle]] 適用)。

## 「初期理論 × 今 session 道具」 5 候補 status update

| # | 接続 | status |
|---|---|---|
| (A) | MDNST × hasAbsorberOver | defer (Heald U8 paywall 結果次第で再評価) |
| (B) | ZCSG × SmallCategory | ★ STEP 1217 完遂 |
| (C) | SNST × 重力場 7 軸 SELF⟲ | defer (Paper 63 prior art audit 先) |
| (D) | ゼロ拡張 × cross-direction | defer |
| (E) | OPU × 評価対称性 | reject (rhyme reject) |
| **(F)** | **EIGHT₄ × D-FUMT₈ 非同型** | **★ STEP 1218 完遂 (chat-Claude (β)-1 由来 新 candidate)** |

## 永続原則準拠

- [[feedback-world-uniqueness-claim-controllable]] — 「世界初」 不使用、 audit 範囲内 controllable
- [[feedback-no-rush-publication]] — paper 起草は Heald U8 比較 + (β)-2/(β)-3 帰還後
- [[feedback-evaluation-symmetry-principle]] — chat-Claude 予告通り = inflate しない、 単に「予告 cases の一つ実現」 と受け止め
- [[feedback-chat-claude-hallucination-warning]] — chat-Claude WebSearch 確認済 3 系統分類は load-bearing source として retain

## 関連 memory + paper

- [[project-session-2026-06-14-evening-dfumt8-skeleton-path]] (STEP 1215 source、 skeleton 設計)
- [[project-dfumt8-category-experiment-2026-06-14]] (STEP 1215 detail)
- [[project-step1217-zcsg-smallcategory-paper61-machine-verification]] (STEP 1217 ZCSG SmallCategory)
- chat-Claude (β)-1 message (2026-06-15) — 3 系統分類 + Shramko-Wansing 一勝 handover
- Paper 65 Lean 4 形式検証 (チャット版 Claude 共著) — 本 STEP は延長 candidate
- Zaitsev (2009) "Studia Logica 92(2):265-280" — EIGHT₄ tetralattice 出典
- Shramko-Wansing (2005) trilattice SIXTEEN₃ — EIGHT₄ 系譜先行