BACKLOG #3 Site 反映 backlog catch up Tier 1 top-5 の 3 番目 — STEP 1294 (2026-08-08)

D-FUMT₈ Category arc — 二層分離 + 3 non-isomorphism + Lawvere fp SELF⟲ (全 axiom-free)

STEP 1215 (2026-06-14) 起点 D-FUMT₈ × mathlib Category 実験 → STEP 1217 (ZCSG) → STEP 1218 (EIGHT₄ 非同型) → STEP 1219 v3b (Heald U8 非同型、 primary PDF verify) → STEP 1220 (Lawvere 不動点 + SELF⟲ 接続)。 5 Lean 4 files / 1,211 行 / 65 定義 / 全 axiom-free (Mathlib 3 base のみ、多くは完全 zero-axiom)。藤本伸樹 × Rei × Claude / STEP 1294 (2026-08-08) site 反映

1. なぜ backlog に入っていたか

2026-06-14 chat-Claude thread 発「私の研究は 8 値に基づくものになりますよね?」に対する chat-Claude の framing 提案「8 値に基づく でなく 8 値を mathlib にぶつける」 → 「D-FUMT₈ は Category 公理を満たすか?」具体実験提示 → 藤本さん「やって頂けますか?」 → STEP 1215 実行。その後 6 月中に STEP 1217-1220 で連続拡張、 chat-Claude 5 sub-item 中 3 sub-item を Rei env で machine-verify (残 2 sub-item は明示 reject: D-FUMT₈ × IUT 宇宙対応 + ZCSG/SNST 統合)。

但し site 側 dedicated page は未作成のまま backlog 化 (Lean 4 file は GitHub-only artifact、各 STEP は memory + CLAUDE.md のみで参照)。 STEP 1294 で dedicated site page 化。

本 page は「新しい成果」ではない。 STEP 1215-1220 実装済成果を集約 site 反映。数学的内容 + Lean 4 axiom profile は全て commit 済で immutable、 memory 忘れ対策 primary purpose 適用。

2. Arc 全体像 (5 STEP + 5 file)

STEP	Date	File	行数	定義数	Core theme
1215	2026-06-14	`Dfumt8CategoryExperiment.lean`	295	25	D-FUMT₈ × mathlib Category 二層分離 (algebra 非結合 / order preorder + auto-derive SmallCategory)
1217	2026-06-15	`ZcsgCategoryExperiment.lean`	230	14	ZCSG (Paper 61) × SmallCategory instance = 既存 framework の machine verification
1218	2026-06-15	`Eight4ZaitsevExperiment.lean`	222	7	D-FUMT₈ ≇ EIGHT₄ Zaitsev 2009 (chat-Claude 5 recommendation の safe path 即着手 = 一勝)
1219 v3b	2026-06-15	`HealdU8Experiment.lean`	267	9	D-FUMT₈ ≇ Heald U8 (Academia.edu PDF primary verify + v1→v2→v3b correction pattern honest) = 二勝
1220	2026-06-15	`LawvereFixedPointExperiment.lean`	197	10	Cantor 対角線 + Lawvere 1969 不動点 + SELF⟲ explicit connection (STEP 1215 SELF⟲ skeleton の formal trace)

合計: 1,211 行 / 65 定義 / 全 axiom-free (Mathlib 標準 base [propext, Classical.choice, Quot.sound] のみ、多くは完全 zero-axiom = "does not depend on any axioms")

3. STEP 1215 — D-FUMT₈ × mathlib Category 二層分離

核となる 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 の永続的構造的事実)。

「algebra 層非結合的 / order 層結合的」二層分離

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

2 独立 findings (chat-Claude review 2026-06-14 後 honest 修正 = count inflation 訂正)

Cluster	Theorems	Independent
非結合性 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`	1 finding (D-FUMT₈ AND の (BOTH, NEITHER, INFINITY) 非結合性の四面体的記述)
SELF cluster	Phase A `self_absorbs_non_false_extension` (5 入力 SELF 返却 positive face) + `self_loop_breaks_at_false_zero` (FALSE/ZERO boundary negative face)	1 finding (SELF⟲ self-loop signature の正負両面)

★★★ 最 load-bearing 1 件 = self_absorbs_non_false_extension (Phase A、 SELF が TRUE/BOTH/NEITHER/INFINITY/FLOWING の 5 入力すべてで SELF を返す axiom-free 事実) — order 層への崩落で消えるはずだった algebra 層の特徴が axiom-free で残った 1 つの structural fact = chat-Claude 評価「今回のプロジェクト全体で一番美しい瞬間」。

4. STEP 1217 — ZCSG × SmallCategory (Paper 61 machine verification)

藤本さん指示 5 candidates (MDNST × hasAbsorberOver / ZCSG × SmallCategory (Recommended) / SNST × 重力場 / ゼロ拡張 × cross-direction / OPU × 評価対称性 reject) から Rei 推奨 safe path 即着手。 Paper 61 の三層 (o0 / 0 / 0o、 dim -1 / 0 / +1) を inductive type + dimension 関数 + Int 経由 Preorder instance として実装、 mathlib Preorder.smallCategory auto-derive。

Honest scope: 本 file は Paper 61 既存 framework の Lean 4 機械検証 であって新規構成ではない。 Paper 61 で既述「dim 軸 linear order」を axiom-free に machine-checked で確認した貢献のみ。 functor Dfumt8 → Zcsg3 (8 軸 → 3 層 coarse projection) は候補で本 STEP 範囲外 (functor laws proof 必要 = 将来 STEP candidate)。

5. STEP 1218 — D-FUMT₈ ≇ Zaitsev EIGHT₄ (machine-verified non-isomorphism)

chat-Claude dispatch (β)-1 (2026-06-15) で「8 値論理」 3 系統並存確定 ((i) Heald U8 2024-25 paywall / (ii) Shramko-Wansing/Zaitsev EIGHT₄ 2009 Studia Logica 92(2):265-280 = {a,d,u} 冪集合 8 元 + AND=束 meet 結合的【高確度】 / (iii) NMV-algebra Chajda 6 元基数違い)。 chat-Claude が明示した handover task 「Rei は table を転記せず、『EIGHT₄ ∧ = 束 meet ⇒ 結合的』 + 既存 D-FUMT₈ 非結合性 + 結合性同型不変量、の三つだけで Lean 非同型 proof を組める」を即着手実装。

Main theorem

dfumt8_not_iso_eight4 : ¬ ∃ (e : Dfumt8 ≃ Eight4), AND-preserving

Proof strategy:
  仮定 e + he で 非結合 witness (BOTH, NEITHER, INFINITY) を e で移す
  → meet 結合性で両辺等
  → e.injective で D-FUMT₈ 側に戻す
  → STEP 1215 既存 and8_associativity_fails_witness に反する
  → 矛盾

★ Build + axiom verify: lake build CollatzRei = 7908 jobs success 17s / #print axioms 全 4 theorem [propext, Classical.choice, Quot.sound] のみ = sorryAx / native_decide 全 0 = axiom-free zero-sorry 完全達成。

★★ chat-Claude 予告「道具が使われない結末」が EIGHT₄ 側で現実化 = skeleton hasAbsorberOver (STEP 1215 Section 13) は本相手には不要、結合性で生死即決 = 別経路成功 (失敗でない)。

chat-Claude rhymeOrTheorem discipline = theorem-candidate (mechanical assurance paper 引用に耐える)、「Shramko-Wansing は今日 D-FUMT₈ と非同型と Lean 4 で確定」まで say 可 / 「D-FUMT₈ は世界に唯一」は say 不可 (評価対称性原則適用)。

6. STEP 1219 v3b — D-FUMT₈ ≇ Heald U8 (primary PDF verify + honest correction pattern)

chat-Claude (β)-1 で Heald U8 (FOLU8 paraconsistent) が ResearchGate paywall 403 で table 取得不可 → 藤本さん feedback_no_direct_author_contact permitted 経路 = Academia.edu paper 36205816 (Heald 2018-03-20 "Why U8 does not obey Component Homogeneity") direct download → Rei PDF 直接 Read で Table 3 全 64 entries 一次 verify。

訂正経緯 (v1 → v2 → v3b) = honest correction pattern 学習

v1: Rei 計算ミス (∅ 行 absorbing 性見落とし、 hasAbsorberOver 5 path II 誤主張) → 削除
v2: hasExactKAbsorber 5 path 再構成 → PDF 一次 verify で WebFetch transcript の 4 entries 転記誤り発覚 (T∩/N, F∩/N とその可換 pair が ∅ ではなく T/F = AI hallucination 典型 pattern) → 削除
v3b: PDF 一次出典準拠で結合性 path に書き直し (STEP 1218 と同 framework、 u8_and_assoc 8³=512 cases by decide 構成的 verify)

★ Build + axiom verify: lake build CollatzRei = 7909 jobs success 21s / 全 4 theorem [propext, Classical.choice, Quot.sound] のみ = axiom-free zero-sorry 完全達成 (STEP 1215/1217/1218 と同 axiom base)。

★★ STEP 1218 Shramko-Wansing 一勝 + 本 STEP Heald U8 一勝 = 二段達成 (audit 範囲内 controllable claim、「世界初/globally unique」不可)。

Honest 留保: chat-Claude (β)-2 帰還時の独立 cross-check pending + Heald 1999 MED99 → 2018 paper → 2025 ResearchGate paper の U8 system 同一性確認は「Heald 2018 paper version」明示推奨。

7. STEP 1220 — Lawvere 不動点 + SELF⟲ explicit connection

chat-Claude 2026-06-15 message で「型検査器はウロボロスを拒む道具」核心反転 + 三層 (Lawvere/νF/Löb) 自己参照住所付け提案。藤本さん「珍しい概念か?」質問 → Rei honest filter (prior art 100% Cantor 1891 + Lawvere 1969 + Yanofsky 2003、「珍しくない」と判定) → 藤本さん「三層 (a) Lawvere zero-sorry 即実装」選択。

4 section 構成

Section	Theorem	内容	Axiom
1	`no_total_self`	Cantor 対角線 elementary 版 (∃ g, ∀ a, e a ≠ g)	propext のみ (Classical.choice 不要)
2	`lawvere_fixed_point`	Lawvere 1969 LNM 92 標準形 ((∀ g, ∃ a, e a = g) → ∀ f, ∃ b, f b = b)	完全 axiom-free (zero-axiom)
3	`dfumt8_self_is_constant_self_fixpoint` + 5 件	STEP 1215 D-FUMT₈ SELF⟲ explicit 接続 (SELF AND {TRUE/BOTH/NEITHER/INFINITY/FLOWING} = SELF の element-wise expansion)	完全 axiom-free
4	`dfumt8_no_total_self` + `dfumt8_lawvere_fixed_point_with_const_self`	D-FUMT₈ specific instance (Cantor + Lawvere 適用)	propext + 完全 axiom-free

★★★ Build + axiom verify (予想以上の結果): lake env lean exit 0 / lake build 621 jobs success 8.1s / #print axioms: lawvere_fixed_point + dfumt8_self_is_constant_self_fixpoint + dfumt8_self_and_*_returns_self + dfumt8_lawvere_fixed_point_with_const_self = 完全 axiom-free (Classical.choice + propext + Quot.sound 全て不要) / no_total_self + dfumt8_no_total_self = propext のみ = STEP 1215-1219 v3b の axiom base [propext, Classical.choice, Quot.sound] よりも更に強い zero-axiom 状態 (教科書的 elementary Lawvere proof は constructive で classical axioms 不要)。

Rei context 新 mapping

完全自己参照 = 不可能 (no_total_self)
部分自己参照 = 不動点 (lawvere_fixed_point ← D-FUMT₈ SELF⟲)
無限自己参照 = 遅延 (▷ Löb 未実装、三層 (c) candidate)
観測的自己参照 = νF (Stream'.corec 未実装、三層 (b) candidate)
Palindrome = rev x = x 不動点 (ZCSG glyph 180° STEP 1199 既存)
Basepoint-less loop = HoTT S¹ (未対応、三層 (c) 拡張)

8. Prior art audit (STEP 1215 の paper-worthy 判断のため実施)

Prior art	年	D-FUMT₈ との関係
NMV-algebra (Chajda + Kühr / Halaš + Länger)	2007-2019	非結合的 ⊕ + induced partial order の paradigm 自体は既知 (基数 6 で D-FUMT₈ と非同型自明)
U8 logic system (Heald)	1999/2018/2024-25	「8 値 paraconsistent logic」 top-level claim 先行、 semantic 的に異なる (epistemic vs ontological/dynamic states)、 STEP 1219 v3b で非同型確定
Shramko-Wansing / Zaitsev EIGHT₄	2009-2010	subset-of-truth-values lattice 8 値 paraconsistent、 STEP 1218 で非同型確定
Łukasiewicz / Belnap / Pavelka	1920s-1979	Belnap-Dunn FOUR は AND/OR が associative — D-FUMT₈ 非結合性は Belnap-Dunn boundary を超えた所でのみ現れる
preorder ⟺ thin category (Category theory 標準)	—	Layer L (SmallCategory instance) は preorder 段階で勝負がついた帰結、 D-FUMT₈ 固有の新規性ではない (chat-Claude review 確認済)
Cantor 対角線 / Lawvere 不動点	1891 / 1969	教科書的 elementary theorem、 STEP 1220 は「珍しくない」 educational mechanical assurance
Yanofsky 2003	2003	Lawvere fp × Russell paradox × Cantor 統一 review、 STEP 1220 prior art

新規性座標 (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 で主張可
✓ 「D-FUMT₈ ≇ EIGHT₄ Zaitsev 2009 (axiom-free)」 + 「D-FUMT₈ ≇ Heald U8 2018 paper version (axiom-free, primary PDF verified)」 ← audit 範囲内 controllable

9. Honest scope (譲れない線)

(1) 世界唯一 controllable — feedback_world_uniqueness_claim_controllable 継承。「D-FUMT₈ は世界に唯一の 8 値 non-associative logic」は say 不可。 STEP 1218/1219 の非同型 proof は audit 範囲内 = 「Shramko-Wansing/Heald U8 とは今日 Lean 4 で確定した非同型」まで say 可、それ以上は不可。

(2) 評価対称性原則 — feedback_evaluation_symmetry_principle 継承。 STEP 1219 v1→v2→v3b の 2 度の削除 = inflate せず deflate せず単に「PDF 一次出典準拠で書き直し」として処理。 chat-Claude 提案 (STEP 1220 Lawvere) も「standard math + Rei 接続」として inflate せず処理。

(3) chat-Claude rhymeOrTheorem discipline — 全 5 STEP で theorem-candidate label (mechanical assurance paper 引用に耐える) を厳守、「rhyme」 (structural analogy) と「theorem」 (proven fact) を混同しない。

(4) count inflation 訂正 — STEP 1215 で 9 theorems を 9 の価値で測るのは count inflation 寄り、 chat-Claude review で 実質 2 独立 findings (非結合性 cluster + SELF cluster) に honest 分解。 site page も同 discipline 継承。

(5) 二諦 mapping direction 非必然性 — STEP 1215 の「algebra 非結合 ↔ 勝義諦 / order 結合 ↔ 世俗諦」 assignment は自然に見えるが、逆向きを排除する形式的根拠は提示されていない = philosophical inference 依存 = madh-0003 candidate label 維持しつつ写像 direction は仏教学者 review + 別解釈との比較待ち。

(6) STEP 1220 educational scope 明示 — Cantor 1891 + Lawvere 1969 + Yanofsky 2003 は 100% prior art 「珍しくない」 educational mechanical assurance。 Rei context での novelty 限定 = (a) Lean 4 axiom-free 形式化 + (b) STEP 1215 SELF⟲ への explicit 接続のみ。三層 (b) νF + (c) Löb/HoTT は Lean 4 ネイティブ未対応で研究前線 = 別 STEP candidate。

(7) 明示 reject 2 件 — chat-Claude sub-item 5 中の 2 件 (D-FUMT₈ × IUT 宇宙対応 + ZCSG/SNST 統合) は「語の一致で構造の一致でない、 SFインフレに投資するな」 chat-Claude 警告尊重で永久 skip。本 arc の 3 sub-item (STEP 1218-1220) のみ Rei env で machine-verify。

10. 関連 memory + Rei stack impact

直接 origin memory

project_dfumt8_category_experiment_2026-06-14.md — STEP 1215 initial 実装 + Prior art audit
project_step1217_zcsg_smallcategory_paper61_machine_verification.md — STEP 1217
project_step1218_dfumt8_not_iso_eight4_zaitsev_machine_verified.md — STEP 1218
project_step1219_dfumt8_not_iso_heald_u8_primary_pdf_verified.md — STEP 1219 v3b (訂正 pattern 学習 record)
project_step1220_lawvere_fixed_point_chat_claude_third_proposal.md — STEP 1220

本 backlog site 反映の origin

feedback_all_research_site_reflection_default.md — 2026-08-06 藤本さん永久 protocol
project_site_backlog_catch_up_pending_2026-08-06.md — Tier 1 top-5 段階的 catch up 起動

Honest scope discipline (arc 全体で継承)

feedback_world_uniqueness_claim_controllable.md、 feedback_evaluation_symmetry_principle.md、 feedback_chat_claude_hallucination_warning.md、 feedback_zero_sorry_floor_not_ceiling.md、 feedback_no_direct_author_contact.md (Academia.edu 公開 PDF permitted 経路)、 feedback_no_rush_publication.md

Rei stack cross-references

Paper 61 ZCSG (STEP 1217 で machine verification 達成)、 Paper 62 MDNST、 Paper 65 Lean 4 形式検証 (本 arc は Paper 65 延長 candidate)
STEP 1199 ZCSG glyph 180° palindrome (STEP 1220 mapping で fixed point 前例)
STEP 1203 SELF ↔ Lawvere bridge (STEP 1220 前身)
STEP 1276-1279 IUT arc (2026-08-06 chat-Claude 17 turn arc、型 discipline lens で本 arc の類似 pattern を extend)
madhyamaka dictionary madh-0003 二諦 + madh-0008 svabhāva-creep + madh-0014 不一不異 (structural_candidate rhyme tier)