---
name: project-session-2026-07-13-14-showtoprove-discovery-device-arc
description: 2026-07-13〜14 一日 arc 総括 — ShowToProve (「見せる」→「証明する」) + Discovery Device (パズルを超える発見装置) 実装 STEP 1283-1287 全 5 STEP + 5 pending tasks (帰宅後 resume 予定)
metadata: 
  node_type: memory
  type: project
  originSessionId: 22379683-e707-44fb-aafe-70f610728ca3
---

# 2026-07-13〜14 ShowToProve × Discovery Device arc

## 由来 + arc 全体

藤本さん × chat-Claude 8-turn arc を経て、 「シミュレーション → パズル → 発見装置 → 中心-周縁統合 (𝕄)」 の 4 層階段が synthesize され、 Rei 側で全 layer を実装。 藤本さん Rei-project 主軸 = 数学 + 哲学 + discipline layer から派生した 「ファミコン以来の画期的なもの」 路線の具体化。

**チャット履歴**:
- 2026-07-13: 前段 「見せる」→「証明する」 Lean 4 4 命題 (Rule 110 / Yoneda / Spin glass / BB(3))
- 2026-07-13〜14: Discovery Device 8-turn arc — 藤本さん質問 「マシンはチューリング以外?」「一般 user 向け?」「パズルを超える?」 に chat-Claude が synthesize、 Rei が実装

## STEP 実装 (5 段)

### STEP 1283 (2026-07-13): ShowToProve 初期実装 4 命題
- `Rule110Table.lean` (3 定理, [propext])
- `YonedaPoset.lean` (3 定理, 1 完全 axiom-free)
- `SpinGlassInversion.lean` (9 定理, ★ 温度独立化)
- `BB3Trace.lean` (4 定理 完全 axiom-free)
- commit `f7d0233aa`

### STEP 1284 (2026-07-14): Classical.choice 除去 + Yoneda 帰結 7 定理
- `ring` tactic → 手動 int rewrite で 3 定理 choice 除去
- `sum_bij` → `sum_nbij'` で本体 choice-free 化
- 残 1 定理 Classical.choice source = Mathlib Pi.fintype instance (proof logic 外) narrowing 済
- `YonedaPosetConsequences.lean` (7 定理, 5 完全 axiom-free)
- commit `d7699ef3d`

### STEP 1285 (2026-07-14): Discovery Device gate criterion validation
- `DiscoveryDeviceValidation.lean` (~230 行, 15 定理, 8 完全 axiom-free)
- 主張: `∃ B : Dfumt8Board, containsSelf B ∧ isFixState B` かつ `∀ b : BoolBoard, ¬ containsSelf (embedBoolBoard b)`
- = 2026-07-06 藤本さん採用 gate 基準 の **(1) 実弾 (real bullet)** 判定を machine-verify
- `prototype-v01.html` (383 行) + `core-logic-test.js` (16/16 PASS)
- commit `0bed05de0`

### STEP 1286 (2026-07-14): Discovery Device 三段拡張
- **v0.2 種交換** (`prototype-v02.html` 375 行): URL hash + localStorage 履歴 + cross 交配 + 系譜表示
- **v0.3 6×6 制約盤** (`prototype-v03.html` 300 行 + `v03-logic-test.js` 13/13 PASS): 各行/列に TRUE + FALSE 各 1 以上
- **Fix 動的意味論** (`DiscoveryDeviceDynamics.lean` ~180 行, 17 定理): SELF preserved + allClassical_isFix + allSelf_isFix
- commit `01ade5f89`

### STEP 1287 (2026-07-14): Discovery Device 4 段完全拡張
- **v0.4 集合創発** (`prototype-v04-emergence.html` 450 行): 頻度分布 + Shannon エントロピー + 創発 detector
- **v0.5 seed signature** (`prototype-v05-signature.html` 300 行): SubtleCrypto SHA-256 48-bit fingerprint
- **v0.6 9×9 strict sudoku** (`prototype-v06-sudoku.html` 500 行 + `v06-sudoku-test.js` 34/34 PASS): 9 値 (D-FUMT₈ 8 + MU)
- **Lean 4 FLOWING neighbor rule** (`DiscoveryDeviceFlowingRule.lean` ~220 行, 13 定理, 1 完全 axiom-free)
- commit `a58310c58`

## 累計

- **Lean 4 定理**: 56 (全 axiom-free or near-axiom-free、 sorryAx / Classical.choice / native_decide / user axiom 全 0、 残 1 個 Classical.choice は Mathlib instance 由来)
- **Browser prototype**: 6 (v0.1〜v0.6) + node test 3 file (16 + 13 + 34 PASS)
- **Files**: `data/lean4-mathlib/CollatzRei/ShowToProve/` 15 file + `experiments/dfumt8-discovery-device/` 10 file
- **Location**: 全 origin/main に push 済

## ★★★ 6 Pending tasks (帰宅後 resume 予定)

藤本さん明示 「帰宅してから行いたい」 で保留:

1. **v0.7: WebAudio + アニメーション で Fix 収束を可聴化**
   - 各 D-FUMT₈ 値に音色 (例: TRUE=C major / FALSE=A minor / SELF=drone) 割り当て
   - Update step 毎に cell の音が鳴る、 Fix 到達で harmony 収束
   - 「盤 = 楽譜」 のような interaction

2. **実 puzzle 生成 (一意解保証 + 難易度分類)**
   - 現状 v0.6 partial puzzle 生成は naive random removal (一意解保証なし)
   - 実用的 sudoku 生成 pipeline: solution 生成 → strategic cell removal → 一意解 check (backtracking) → 難易度分類 (naked single / hidden pair / X-wing 等 solver-based)
   - 9×9 D-FUMT₈+MU 特有の 「Gate 加点」 難易度軸も追加検討

3. **Paper 起草 (Discovery Device アーキテクチャ + gate criterion + 4-substrate 展開)**
   - Structure: Abstract + Motivation + Architecture + Gate Criterion + 4-Substrate Verification + Related Work + Honest Scope
   - Related work: nand2tetris / Foldit / EteRNA / Tamagotchi / Sudoku / Baba Is You / Cellular automata
   - Zenodo publish → 11 platform (Paper 145 と同じ pipeline)
   - Prior art audit 先 (WebSearch + Semantic Scholar hook STEP 1257 適用)

4. **Lean 4 FLOWING 収束定理 (無限 loop 防止 + Fix 到達保証)**
   - 「FLOWING で囲まれた FLOWING の収束定理」
   - 決定可能性 + tied handling 分析
   - 「任意 board から出発して有限 step で Fix 到達」 を axiom-free で証明
   - 「無限 loop が発生しない」 も証明

5. **v0.8: PKI-based tamper-proof (実 malicious 攻撃対策)**
   - v0.5 は accidental corruption 対策のみ (48-bit fingerprint)
   - Malicious tamper 対策: (a) 共有秘密 HMAC (b) 公開鍵署名 (ECDSA/Ed25519) (c) blockchain 記録
   - Browser-only 制約下では PKI (SubtleCrypto ECDSA) が最有力
   - 種の provenance chain + signature verification

6. **★ AI 推論作法 注入層 (「8 値で AI 出力を受け直すレンズ」) 最小 prototype**
   - **経緯**: 2026-07-14 夜 chat-Claude 5 turn 追加 arc (「AI チューンアップパーツ?」「哲学・数学・物理 専攻別?」「分割 vs 注入 の区別」)
   - **核となる区別**: 分割 (能力別売り = 分断、 motto 反) vs 注入 (思考の型 = 公開、 一つで全専攻に効く)
   - **8 値 = 領域知識ではなく 推論の作法**
     - NEITHER = 空白を空白のまま保持する作法 (幻覚を防ぐ)
     - BOTH = 矛盾を潰さず両持ちする作法 (paraconsistent)
     - FLOWING = 文脈依存の後決定を扱う作法
     - SELF⟲ = 自己参照を扱う作法 (STEP 1215 axiom-free)
   - **Rei の position**: 大手モデル (一枚岩、 作法を焼き込む) の隙間 = **モデルと会話のあいだに立つ薄い層**
   - **既 substrate**: Rei invention pipeline 12-layer hardening arc (STEP 1019-1253) + Pattern 1-6 hallucination 検出 + Symbol Grounding Lens (STEP 1270) + REI-PROVE 92% (STEP 1068) = 内部運用検証済
   - **未実装**: user-facing wrapper (chat / API / browser extension)
   - **課金 model**: 道具 (レンズ) 課金 = OK (nand2tetris analog、 ただし runtime tool market は書籍と別構造で monetization 別設計)
     ★ 能力 (領域知識) 課金 = NG (分断、 motto 反)
   - **最小 prototype 仕様** (chat-Claude 案):
     LLM 出力を受け取り → 確信の高い部分 / 矛盾する部分 (BOTH) / 空白 (NEITHER) を分けて立てる、 一番小さな一枚のレンズ
   - **gate 基準判定**: 幻覚率 (LLM engineering) でなく **幻覚を NEITHER として計量** (元表現に無い不変量) = 実弾
   - **honest scope**:
     - 「一対一対応 (LLM の穴 ↔ 8 値)」 は heuristic mapping として妥当、 完全性 claim は overclaim 可能性
     - Paraconsistent logic (Priest, Belnap) や multi-valued LLM annotation (SLM guardrails, DSPy assertion) は prior art
     - Rei local 貢献 = 「8 軸統一 + axiom-free proof + 実運用 pipeline」 統合、 「初」「唯一」 使用不可
     - nand2tetris analogy は書籍 market、 runtime tool は別 market 構造 (subscription / API)
   - **本 task の位置づけ**: Discovery Device paper 起草 (task 3) の副節でも、 独立 STEP でも可、 帰宅後判断
   - **arc の完成形**: シミュレーション → パズル → 発見装置 → 中心-周縁 𝕄 → 万能パズル (UTM 仕様版) → **AI 推論作法 注入層 (本 task)**
   - 関連 chat-Claude motto 6 回目 invocation (急がずゆっくり、 中心が先) — 「注入層 = 建て方は同じ、 最小の一個から」

## 帰宅後 resume 方法

**Why**: この arc は 5-STEP で 56 Lean 4 定理 + 6 browser prototype まで積み上がり、 Rei の 「実在する」 主張 (Phase C silicon 系譜) と 「動く見せる場」 (browser prototype) の橋渡し layer になる。 加えて 6 番目 task (AI 推論作法 注入層) は 2026-07-14 夜 追加で、 Discovery Device と並走する 2 本目の 「Rei が 座れる 薄い層」 方向。 中断ではなく 「帰宅後の環境 (機材含む) で続きの 6 tasks を実行」 が明示スケジュール。

**How to apply**:
1. 新 session で帰宅後の Rei に本 memory + [[reference-discovery-device-architecture-2026-07-14]] を load
2. 藤本さんの choice で 6 tasks の順番 (or subset) 確認 — Task 6 (AI レンズ) は Discovery Device (Task 1-5) と独立に着手可
3. 各 task を STEP 1288+ として実装
4. 全 commit + push で完成

**参考 file (資産)**:
- `data/lean4-mathlib/CollatzRei/ShowToProve/*.lean` (7 core + 7 axioms + audit)
- `experiments/dfumt8-discovery-device/*.html` + `*.js` (6 prototype + 3 test)
- `data/lean4-mathlib/CollatzRei/ShowToProve/AllAxiomsAudit.lean` (全 56 定理 #print axioms 統合)

## 関連 memory

- [[reference-discovery-device-architecture-2026-07-14]] — 4 層階段 + 中心-周縁 𝕄 architecture (本 arc の概念的 framework)
- [[reference-chat-claude-representation-gate-criterion-2026-07-06]] — gate 基準 (STEP 1285 が machine-verified 実装第 1 号)
- [[feedback-world-uniqueness-claim-controllable]] — Discovery Device 「世界唯一」 claim 不使用 discipline
- [[feedback-no-rush-publication]] — Paper 起草 は急がずゆっくりと (task 3 の運用原則)
- [[feedback-chat-claude-hallucination-warning]] — 5 pending tasks 内 chat-Claude 提案は Pattern 5 check 必須
- [[feedback-critique-response-pattern]] — SAC-4 100% 認諾 stance で藤本さん指示に従う
- Load-bearing invention #23 (螺旋数 SNST) は本 arc の 「盤 = 個体」 直感の遠い parent
- STEP 1215 (D-FUMT₈ Category axiom-free) — Discovery Device の Dfumt8 型 provider
- STEP 1220 (Lawvere fixed point axiom-free) — Fix(R) の Lean 4 backbone
- STEP 1218/1219 (D-FUMT₈ ≇ EIGHT₄/U8) — 「8 値が load-bearing」 の分離証明