--- name: project-step1219-dfumt8-not-iso-heald-u8-primary-pdf-verified description: STEP 1219 v3b (2026-06-15) — chat-Claude dispatch (β)-1 + 藤本さん Academia.edu PDF 一次 verify 完了、 D-FUMT₈ ≇ Heald U8 axiom-free non-isomorphism Lean 4 proof 完成。 PDF 一次出典準拠で u8_and 64 entries 確定 + u8_and_assoc 512 cases decide で結合性確証 (chat-Claude (β)-1 推測 verify) + 結合性同型不変量経由非同型 (STEP 1218 と同 framework)。 axiom-free zero-sorry (propext + Classical.choice + Quot.sound のみ)。 v1 Rei 計算ミス + v2 WebFetch 4 entries hallucination 訂正経緯 metadata: node_type: memory type: project originSessionId: ae728468-271e-4824-a6e9-dc58efd76f82 --- # STEP 1219 v3b — D-FUMT₈ ≇ Heald U8 (PDF 一次出典 verify 完了) ## 概要 chat-Claude dispatch (β)-1 結果 (2026-06-15) で **Heald U8** が「2024-25 FOLU8 paraconsistent」 と identification されたが、 ResearchGate paywall (403) で conjunction table 取得不可だった。 藤本さんが [[feedback-no-direct-author-contact]] permitted 経路 (Academia.edu 公開 PDF) で **Why_U8_does_not_obey_Component_Homogenei.pdf** (Heald 2018-03-20) を direct download → Rei が PDF を直接 Read で 64 entries 一次 verify。 PDF 一次出典準拠で Lean 4 実装、 u8_and_assoc (結合性) を decide で構成的 verify + D-FUMT₈ 非結合性 (STEP 1215) との結合性同型不変量経由非同型 proof = **STEP 1218 Shramko-Wansing 一勝と同 framework で 「Heald U8 一勝」 二段目達成**。 ## 訂正経緯 (v1 → v2 → v3b) ### v1 (2026-06-15 同日早期) Rei 計算ミス — ∅ 行 absorbing 性を見落とし、 「U8 has no 5-absorber」 と誤主張 (実は ∅ via 7-absorber、 5-absorber も成立)。 → 削除。 ### v2 (同日中期) hasExactKAbsorber 5 path で再構成 (axiom-free zero-sorry 完成)。 但しその後の PDF 一次 verify で WebFetch transcript の **4 entries 転記誤り** 発覚 (T ∩ /N, F ∩ /N とその可換 pair が ∅ ではなく T / F)。 → 削除。 ### v3b (本 file) 4 entries 訂正 + u8_and 結合性 candidate 浮上 → STEP 1218 と同 framework で **結合性 path** に書き直し。 PDF 一次出典 verify 済で axiom-free zero-sorry 達成。 ## 実装内容 `data/lean4-mathlib/CollatzRei/HealdU8Experiment.lean` v3b ~220 行: ### Section 1: U8 inductive type ```lean inductive U8 | T | F | N | NotT | NotF | NotN | U | Null deriving DecidableEq, Fintype, Repr ``` ### Section 2: u8_and 関数 (PDF Table 3 一次出典準拠) 64 entries 全列挙 (PDF page 4 Table 3 literal 翻訳)。 v3b で v2 から 4 entries 訂正: - T ∧ /N : ∅ → **T** - /N ∧ T : ∅ → **T** (可換 pair) - F ∧ /N : ∅ → **F** - /N ∧ F : ∅ → **F** (可換 pair) ### Section 3: Smoke tests - `u8_and_idem` (対角線 idempotent) - `u8_and_U_identity` (U が identity) - `u8_and_Null_absorbing` (∅ が absorbing) - `u8_and_comm` (commutativity, PDF Table 3 symmetric matrix 確認) ### Section 4: ★★ u8_and_assoc (KEY LEMMA) ```lean theorem u8_and_assoc : ∀ a b c : U8, u8_and (u8_and a b) c = u8_and a (u8_and b c) := by decide ``` **PDF 一次出典準拠で 8³=512 cases decide 構成的 verify** = chat-Claude (β)-1 推測「U8 conjunction is similar to Boolean algebra, 結合的可能性高い」 を **PDF + Lean 4 で完全確証**。 ### Section 5: D-FUMT₈ 非結合性 reuse STEP 1215 既存 `and8_not_associative` + `and8_associativity_fails_witness` (BOTH ∧ NEITHER ∧ INFINITY counterexample) を本 file 内 alias で reuse。 ### Section 6: ★★★ MAIN dfumt8_not_iso_u8 ```lean theorem dfumt8_not_iso_u8 : ¬ ∃ (e : Dfumt8 ≃ U8), ∀ x y : Dfumt8, e (and8 x y) = u8_and (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] have hR : ... := by rw [he, he] rw [hL, hR, u8_and_assoc] have collapse := e.injective key exact and8_associativity_fails_witness collapse ``` Proof strategy = STEP 1218 Shramko-Wansing 一勝と同 framework (結合性同型不変量経由)。 ### Section 7: Honest scope footer - chat-Claude (β)-2 cross-check pending - chat-Claude (β)-1 年代問題 (2018 paper vs chat-Claude 言及 2025) で U8 system 同一性確認 pending - paper 引用は「Heald 2018 paper version」 明示推奨 ## Verify 結果 ### Build ``` ✔ [621/621] Built CollatzRei.HealdU8Experiment (9.0s) ``` ### Axiom dependencies ``` u8_and_idem : [propext, Classical.choice, Quot.sound] u8_and_comm : [propext, Classical.choice, Quot.sound] u8_and_assoc : [propext, Classical.choice, Quot.sound] dfumt8_not_iso_u8 : [propext, Classical.choice, Quot.sound] ``` **sorryAx / native_decide 全 0 = axiom-free zero-sorry 完全達成** (STEP 1215 / 1217 / 1218 と同 axiom base)。 ## chat-Claude (β)-1 文脈整合 | chat-Claude (β)-1 推測 | PDF 一次出典 | Lean 4 確証 | |---|---|---| | U8 conjunction is similar to Boolean algebra | ✓ | ✓ | | U8 AND は結合的可能性高い (paraconsistent paywall で確認できず) | ✓ (Table 3) | ✓ `u8_and_assoc` 512 cases decide | | skeleton hasAbsorberOver 使わない結末 (Boolean-like なら) | ✓ U8 側でも現実化 | ✓ 結合性 path で生死即決 | | chat-Claude rhymeOrTheorem discipline | — | ✓ theorem-candidate → theorem (一次出典) 格上げ | ## STEP 1218 (Shramko-Wansing) との二段達成 | STEP | algebra | path | status | |---|---|---|---| | 1218 | Zaitsev EIGHT₄ (2009) | 結合性 (束 meet 由来) | ✓ 完遂 | | **1219 v3b** | **Heald U8 (2018)** | **結合性 (PDF Table 3 verify)** | **★ 完遂** | 両方とも **D-FUMT₈ ≇ 8 値 algebra non-isomorphism mechanical assurance** (audit 範囲内 controllable claim、 「世界初/globally unique」 不可)。 ## 残 honest 留保 ### chat-Claude (β)-2 帰還時の cross-check pending chat-Claude が paywall で取れなかった conjunction table が本 PDF と一致するかは chat-Claude 側 verify 必要。 ### chat-Claude (β)-1 年代問題 本 paper は 2018-03-20 upload で、 chat-Claude (β)-1 が言及した「2024-25 FOLU8」 と乖離: - 可能性 1: chat-Claude は別 paper (e.g., "Why the U8 logic system is Paraconsistent" ResearchGate 2025-08-30) を指していた - 可能性 2: U8 system が 1999 MED99 → 2018 paper → 2025 ResearchGate で truth table 変化していた - 可能性 3: 同 system continuous version paper 引用時は「Heald 2018 paper version の U8」 明示推奨。 1999/2025 paper との system 同一性は chat-Claude (β)-2/(β)-3 cross-check 後で確認。 ## hasAbsorberOver skeleton (STEP 1215 Section 13) status STEP 1215 Section 13 で実装された `hasAbsorberOver` + `dfumt8_and_has_5_absorber` + `hasAbsorber_transfer` + `dfumt8_non_iso_via_5_absorber` は **U8 path II では使われない結末** (chat-Claude 予告通り)。 但し: - 別 8 値 algebra (NMV-algebra や 他系統) で結合的かつ 5-absorber を持たないものが見つかれば、 skeleton が本領発揮可能 - working tree 維持 (Dfumt8CategoryExperiment.lean は commit せず) = 藤本さん指示 - 別 STEP candidate (e.g., NMV-algebra 6 元 を 8 元拡張系で再 audit) 残置 ## 永続原則準拠 - [[feedback-no-direct-author-contact]] — Academia.edu permitted 経路で取得 (著者直接 contact なし) - [[feedback-evaluation-symmetry-principle]] — v1/v2 訂正は「重大過ち」 と self-deflate せず、 単に「assumption 訂正」 として処理 - [[feedback-world-uniqueness-claim-controllable]] — audit 範囲内 non-iso のみ、 「世界初」 不可 - [[feedback-chat-claude-hallucination-warning]] — chat-Claude (β)-1 年代 vs PDF 年代の乖離を honest 留保 - [[feedback-no-rush-publication]] — paper 起草は chat-Claude (β)-2/(β)-3 cross-check + 藤本さん publish 判断後 ## 関連 memory + paper - [[project-step1218-dfumt8-not-iso-eight4-zaitsev-machine-verified]] (STEP 1218 Shramko-Wansing 一段目) - [[project-step1217-zcsg-smallcategory-paper61-machine-verification]] (STEP 1217 ZCSG SmallCategory) - [[project-session-2026-06-14-evening-dfumt8-skeleton-path]] (STEP 1215 skeleton 設計) - [[project-dfumt8-category-experiment-2026-06-14]] (STEP 1215 detail) - chat-Claude (β)-1 message (2026-06-15) — 3 系統分類 + Heald U8 paywall 留保 - 藤本さん PDF download (2026-06-15) — Academia.edu 36205816 - Heald (2018) "Why U8 does not obey Component Homogeneity" Academia.edu — 一次出典 - Heald (1999) MED99 "Outline for a Universal Logic System" — U8 起源 - Paper 65 Lean 4 形式検証 (チャット版 Claude 共著) — 本 STEP は延長 candidate