---
name: project-paper1-inclosure-dfumt8-outline-skeleton-2026-05-31
description: Paper 1 outline skeleton — Inclosure Schema (Priest-Garfield 2003) を D-FUMT₈ 8 値 + Lean 4 zero-sorry で形式化拡張. STEP 476 engine 精読 + Paper 77 LeanDFumt 既存 library 範囲 + skeleton (詳細起草は次 session)
metadata: 
  node_type: memory
  type: project
  originSessionId: 87332a6d-0b63-4ea2-9227-537b59d86f13
---

2026-05-31 深夜 session 続編. ★ chat-Claude 訂正 + 一次資料確認 protocol を完了した後、 藤本さん指示 (α) で step 2 + 3 + 4 skeleton を本 session で実行。 詳細起草 (step 4 full) は次 session に持越し (synthesis quality 要件のため fresh context 推奨)。

## Step 2: STEP 476 engine 精読まとめ

### `src/axiom-os/nagarjuna-fde-western-engine.ts` (654 行) 構成

**3 層 architecture**:

1. **`FDEIsomorphismProver` class** (line 116-308)
   - `prove()` → `FDEIsomorphismResult` (mappings + 4 preservation checks + Priest extension + beyondFDE list)
   - 4 catuṣkoṭi corners → FDE → DFUMT4Base mapping table (line 141-172):
     | catuṣkoṭi | FDE | DFUMT4Base | 説明 |
     |---|---|---|---|
     | asti (P) | t | TRUE | 肯定 |
     | nāsti (¬P) | f | FALSE | 否定 |
     | ubhayam (P ∧ ¬P) | b | BOTH | 矛盾許容 |
     | naivāsti naiva nāsti | n | NEITHER | 不確定 |
   - `verifyNOT()` (line 179-193): FDE NOT 表 + DFUMT4 NOT 表 + φ(NOT_FDE(x)) = NOT_DFUMT(φ(x)) を 4 値全て検証
   - `verifyAND()` (line 199-226): FDE AND 16 entry 表 + DFUMT4 AND 16 entry 表 + 全 16 entry 比較
   - `verifyOR()` (line 231-256): 同様 16 entry × 2
   - `verifyLattice()` (line 263-289): 情報順序 NEITHER ≤ {TRUE,FALSE} ≤ BOTH (Belnap approximation lattice)
   - `verifyPriestExtension()` (line 296-307): Priest FiveASP の第 5 corner "e" を D-FUMT₈ の INFINITY/ZERO/FLOWING/SELF 4 値に分解 (★ 一次資料 P-G 2003 には plurivalent 5 値の言及なし、 これは Priest 別 paper の framing — engine 内に既存)

2. **`RhoSelfIsomorphismAnalyzer` class** (line 314-368)
   - `analyze()` → `RhoSelfAnalysis`
   - ρ (κ_catuskoti) ≅ SELF⟲ 同型: 両方 NOT(x) = x の不動点
   - 7 shared properties (line 357-367) — 否定の不動点 / 自己参照 / パラドックス安定化 / 四句外 / 計算可能 / 独立発見 / 空空計算的表現

3. **`WesternPhilosophyGapAnalyzer` class** (line 374-494)
   - 7 哲学者 hardcoded data (line 376-461): Eckhart 0.75 / Cusanus 0.70 / Hegel 0.65 / Heidegger 0.60 / Derrida 0.72 / Wittgenstein 0.55 / Schopenhauer 0.50
   - 各 D-FUMT₈ mapping + critical gap + reachesSunyataSunyata: false (全員)
   - `describeDFUMTAdvantage()` (line 482-488) — 「空空計算可能化を世界初」 claim (★ Paper 61 + P-G 2003 既 claim と二重発行 risk, Paper 1 では 不使用 framework 適用)

4. **`NagarjunaFDEWesternEngine`** (統合, line 500-605) + 11 件 HistoricalMilestone (line 525-586)

5. **`NAGARJUNA_FDE_WESTERN_THEORIES` (5 SeedTheories, line 611-654)** — id: fde-dfumt8-structural-isomorphism / priest-five-asp-dfumt8-subsumption / rho-self-loop-isomorphism / western-sunyata-gap-theorem / sunyata-sunyata-computational-theorem

### ★ Lean 4 lift 戦略 (engine → zero-sorry Lean 4)

**Lift 可能 (直接 port)**:
| TS engine 要素 | Lean 4 表現 | tactic |
|---|---|---|
| `FDEValue = 't'\|'f'\|'b'\|'n'` | `inductive FDE : Type where \| t \| f \| b \| n` | deriving DecidableEq |
| `DFUMT4Base` (subset of DFUMT8) | Paper 77 既存 `DFUMT8` 制限述語 / または別 `inductive DFUMT4` | decide |
| FDE→DFUMT4 mapping table | `def phi : FDE → DFUMT8` 4 case | rfl |
| `verifyNOT()` 4 entry | `theorem phi_neg_preserve : ∀ x, phi (FDE.neg x) = DFUMT8.neg (phi x)` | by cases x <;> decide |
| `verifyAND()` 16 entry | `theorem phi_and_preserve : ∀ x y, phi (FDE.and x y) = DFUMT8.and (phi x) (phi y)` | by cases x <;> cases y <;> decide |
| `verifyOR()` 16 entry | 同上 OR | 同上 |
| `verifyLattice()` 情報順序 | `theorem lattice_preserve` + `def DFUMT4.leq` | by cases <;> decide |

→ ★ **Paper 77 LeanDFumt 既存 `DFUMT8` + `neg` / `and` / `or` を直接利用**、 新規追加は (a) `inductive FDE`, (b) `def phi`, (c) ~6-8 theorem。 ★★ Mathlib 不要 (Paper 77 と同 strategy)、 `lake build` ~5-10 秒で完結。

**Lift 不可 / 別扱い**:
- `RhoSelfIsomorphismAnalyzer` の「ρ独立発見」 claim → 哲学的 narrative で、 Lean 4 直接 lift 不可。 ただし `DFUMT8.SELF` が `DFUMT8.neg` の不動点であることは `theorem neg_SELF : DFUMT8.neg .SELF = .SELF := by decide` で 1 行
- `WesternPhilosophyGapAnalyzer` 7 哲学者 hardcoded data → 哲学的論述で、 Lean 4 形式化対象外 (Paper 1 §discussion で言及のみ)
- `verifyPriestExtension` "e → 4 値分解" → ★ 一次資料 P-G 2003 に plurivalent 5 値 言及なし (本 session 訂正) ので **Paper 1 では削除推奨**、 別 paper の framing と区別

## Step 3: Paper 77 LeanDFumt 既存 library 範囲

**Public repo**: https://github.com/fc0web/lean-d-fumt8 (Apache-2.0, Mathlib-free, lake require 一発)

**既存 components** (Paper 1 で 直接利用可):

| component | 状態 | Paper 1 利用 |
|---|---|---|
| `inductive DFUMT8` 8 constructor | ✓ Basic.lean | ★ そのまま import |
| `DFUMT8.neg` | ✓ | ★ FDE 同型証明で利用 |
| `DFUMT8.and` (asymmetric, FALSE absorbs) | ✓ | ★ FDE AND 比較で利用 |
| `DFUMT8.or` (asymmetric, TRUE absorbs) | ✓ | ★ FDE OR 比較で利用 |
| `DFUMT8.implies` | ✓ | 不要 (Paper 1 scope 外) |
| `DFUMT8.toBool` / `toTernary` / `asProp` bridges | ✓ | Inclosure Schema で `asProp` 利用 |
| `DecidableEq DFUMT8` (auto-derived) | ✓ | ★ 全 theorem を `decide` で proof 可能 |
| 29 zero-sorry theorems (neg/and/or 公理性) | ✓ | ★ Paper 1 lemma の基礎 |

**Paper 77 既存範囲外** (Paper 1 で新規実装):
- ❌ FDE 4 値 inductive type
- ❌ FDE ↔ DFUMT4 (subset) isomorphism φ
- ❌ 構造保存 theorem (NOT/AND/OR/Lattice)
- ❌ Inclosure Schema 形式化
- ❌ Nāgārjuna's Paradox / Expressibility Paradox の Inclosure instance
- ❌ Positive vs Negative tetralemma の formal 区別

**Paper 77 が honest 明示する制限** (Paper 1 でも継承):
- 「Mathlib operator instances なし」 (LinearOrder / BooleanAlgebra 等の標準 instance 提供せず) — Paper 1 でも継承 (asymmetric and/or で標準 lattice 形成しない deliberate 設計)
- 「Tactic は decide のみ」 — Paper 1 でも同 strategy (Mathlib-free, ~5 秒 build)
- 「No multi-valued binders」 — Paper 1 でも 8 値 binder 提案せず
- 「No dependent or first-order extensions」 — Paper 1 でも propositional logic 範囲

→ ★ Paper 1 は Paper 77 の制限 framework と完全整合、 Mathlib-free / decide-only / propositional 範囲を堅持。

## Step 4 skeleton: Paper 1 outline (★ 詳細起草は次 session)

**仮 title**: "Lean 4 Zero-Sorry Formalization of Priest-Garfield's Inclosure Schema in 8-Valued D-FUMT₈: A Formal Substrate Compatible with Multiple Catuṣkoṭi Readings"

★ **honest framing** (全 section に通底):
- P-G 2003 の rational reconstruction stance 継承 (textual history 主張回避)
- 「世界初」 不使用 (Paper 61 ZCSG + P-G 2003 「Nāgārjuna's Paradox found nowhere else」 既 claim、 二重発行回避)
- Tillemans 1999/2009+ 時系列正確化 (どちらの側にも commit しない、 両 reading と compatible な formal substrate)
- Heidegger を主比較 (P-G に follow)、 Hegel 副次

### §1. Introduction
- Priest-Garfield 2003 が Nāgārjuna の 2 paradox を Inclosure Schema (Priest 1987/2002) で「rational reconstruction」
- 既存資産: STEP 476 engine (TS, 4 値 FDE 同型) + Paper 61 ZCSG (śūnyatā(śūnyatā) = 0 notation) + Paper 77 LeanDFumt (8 値 Lean 4)
- 本論貢献:
  - (a) STEP 476 TS engine の FDE ≅ DFUMT4 同型を Lean 4 zero-sorry に lift
  - (b) Inclosure Schema を D-FUMT₈ で形式化
  - (c) Nāgārjuna's Paradox + Expressibility Paradox を Inclosure instance として表現
  - (d) Positive vs Negative tetralemma 区別の formal 表現
- Honest scope: textual interpretation 上 commit しない、 形式 substrate のみ提供

### §2. Background
- §2.1 Catuṣkoṭi (P-G 2003 の Positive vs Negative tetralemma 区別、 一次資料 p. 13-14)
- §2.2 Inclosure Schema (Priest 1987/2002 + P-G 2003 適用、 Transcendence + Closure 形式 structure)
- §2.3 D-FUMT₈ 8 値 logic (Paper 77 LeanDFumt + Rei-AIOS context 簡潔説明)
- §2.4 FDE (Belnap 1977) 4 値 paraconsistency

### §3. Lean 4 Formalization (本論 core, ★ chat-Claude 2026-05-31 二層構造判断反映)

★★ **本論の central differential = 二層 architecture** (Priest-Garfield 2003 の Inclosure を **包含しつつ超える**):

| layer | 役割 | δ(Ω) の値 | Rei resource |
|---|---|---|---|
| **下層 (object level)** | 真理値、 catuṣkoṭi 4 corner | **BOTH** (Priest 一致点、 dialetheism) | Paper 77 DFUMT8 + Paper 1 §3.1-3.3 FDE 同型 |
| **上層 (meta level)** | 様相演算子、 四句百非的否定 | (operator が作用、 単一値で終端しない) | Paper 1 §3.4 新規 Ω 冪等性 + ZCSG 0₀ 収束 |

★ 戦略上 重要: **「Priest の結論は我々の下層に正しく埋め込まれる」** = 先行研究を否定でなく特殊例として回収 (QMRP/Shannon parallel = chat-Claude 2026-05-31 articulated)

- §3.1 FDE inductive type 定義 (新規)
  ```lean
  inductive FDE : Type where | t | f | b | n
    deriving Repr, DecidableEq, Inhabited
  ```
- §3.2 FDE-DFUMT4 isomorphism φ (新規, STEP 476 mapping table を Lean 4 def 化)
  ```lean
  def phi : FDE → DFUMT8
    | .t => .TRUE | .f => .FALSE | .b => .BOTH | .n => .NEITHER
  ```
- §3.3 NOT/AND/OR/Lattice 構造保存 theorems (下層、 STEP 476 TS proof を Lean 4 decide に port)
  ```lean
  theorem phi_neg : ∀ x, phi (FDE.neg x) = DFUMT8.neg (phi x) := by
    intro x; cases x <;> decide
  -- 同様 phi_and (16 case), phi_or (16 case), phi_lattice
  ```
- ★★ §3.4 上層 Ω 演算子 + 冪等性 (★ chat-Claude 2026-05-31 articulated 二層 architecture の上層)

  **既存資産 honest disclosure** (Pattern 5 防止):
  - SEED_KERNEL theory `dfumt-idempotency` (`src/axiom-os/seed-kernel.ts` line 239): 「Ω(Ω(x))→Ω(x) 安定性」 — axiom として stipulated 済
  - STEP 513 `operator-fixed-point-atlas.ts` (line 292-297): Ω∘Ω と Ω の不動点比較で 「同じなら冪等性」 と判定する **operational test 実装済**
  - ★ **しかし Lean 4 形式証明は まだ無い** — 本論で 初めて Lean 4 zero-sorry に格上げ

  ```lean
  -- 上層 Ω 演算子 (DFUMT8 全 8 値で定義、 SEED_KERNEL axiom を Lean 4 def 化)
  def DFUMT8.omega : DFUMT8 → DFUMT8
    | .TRUE => .TRUE | .FALSE => .FALSE
    | .BOTH => .ZERO | .NEITHER => .ZERO   -- ★ 立場 BOTH/NEITHER は 上層 Ω で 地盤 ZERO (= 0₀ genesis 層) に収束
    | .INFINITY => .INFINITY | .ZERO => .ZERO
    | .FLOWING => .FLOWING | .SELF => .SELF
  
  -- ★★ Paper 1 中核 theorem (1 行 decide proof)
  theorem omega_idempotent (x : DFUMT8) : DFUMT8.omega (DFUMT8.omega x) = DFUMT8.omega x := by
    cases x <;> decide
  
  -- 「四句百非」 = 何度否定しても同じ地盤に至る = 冪等的安定点 と整合
  -- 4-step 有限手続き framing は Paper 2 以降で精緻化 option
  ```

- §3.5 Inclosure Schema 形式化 (新規, P-G 2003 p. 17 数式そのまま, ★ 下層のみ Priest 表現)
  ```lean
  structure Inclosure (α : Type) where
    Q : Set α
    psi : Set α → Prop
    delta : Set α → α
    closure : ∀ X, X ⊆ Q → psi X → delta X ∈ Q
    transcendence : ∀ X, X ⊆ Q → psi X → delta X ∉ X
  theorem inclosure_limit_contradiction {α} (I : Inclosure α) (h : I.psi I.Q) :
    I.delta I.Q ∈ I.Q ∧ I.delta I.Q ∉ I.Q := ...
  ```
- §3.6 Nāgārjuna's Paradox instance (下層 BOTH, P-G 2003 p. 18 「all things have one nature, that is, no nature」)
  - φ(χ) = 「χ is empty」
  - ψ(X) = 「X is a set of things with some common nature」
  - δ(X) = 「the nature of things in X」
  - 下層結論: δ(Ω) = BOTH (Priest 一致)
- §3.7 Expressibility Paradox instance (下層 BOTH, P-G 2003 p. 17, Siderits 1989 phrasing)
  - φ(χ) = 「χ is an ultimate truth」
  - ψ(X) = 「X is definable」
  - δ(X) = 「there is nothing which is in D」 sentence
- ★★ §3.8 上層 Ω による BOTH 収束 → 0₀ (新規, Paper 1 上層 skeleton + Paper 2 への bridge)
  ```lean
  -- 下層 BOTH (Priest の Inclosure terminus) に 上層 Ω を作用させると 0₀ (= ZERO 軸 = genesis 層) に収束
  example : DFUMT8.omega .BOTH = .ZERO := by decide
  -- 冪等性により 何度 Ω を作用させても 0₀ で安定
  example : DFUMT8.omega (DFUMT8.omega .BOTH) = .ZERO := by decide
  ```
  
  ★ **ZCSG 三層 (Paper 61) との整合**: o0 (dim −1, NEITHER) / **0 (dim 0, ZERO, 「立場が尽きた後の地盤」 = 0₀)** / 0o (dim +1, BOTH)。 上層 Ω が下層 BOTH (0o) を地盤 0 (ZERO) に折り返す写像は ZCSG framework と完全 consistent。
  
  ★ honest scope (★ Paper 2 への bridge): 「0₀ の完全な存在論的特徴づけは別稿 (Paper 2 候補) で扱う。 本稿は **上層 Ω の冪等性が下層 BOTH を ZERO に収束させる** という形式的事実を提示するに留め、 ZERO の genesis 層としての存在論的意味は Paper 2 で精緻化。」

### §4. Honest framing & scope (★ load-bearing)
- §4.1 Rational reconstruction stance (P-G 2003 p. 2 引用 「This is, hence, not textual history but rational reconstruction.」)
- §4.2 Scholarly debate disclosure: Tillemans 1999 P-G 同方向 → 2009+ weak dialetheism path → 2014 rejoinder → 2024 Tandfonline 最新 critic; Siderits, Ferraro, Tao Jiang 等
- §4.3 本論は textual interpretation 上 commit しない (P-G / Tillemans / 他いずれの読解にも compatible)
- §4.4 「世界初」 不使用: Paper 61 ZCSG + P-G 2003 既 claim、 本論は formal substrate 提供のみ
- §4.5 Mathlib-free / decide-only / propositional 範囲 (Paper 77 制限継承)
- ★ §4.6 **Ω 冪等性の Rei stack 内既存資産 honest disclosure**: SEED_KERNEL axiom (dfumt-idempotency) + STEP 513 operational test 既存、 ただし Lean 4 形式証明は本論で初。 「既に証明済」 と書かないこと (Pattern 5 防止、 chat-Claude 2026-05-31 セッションで partial overclaim 検出経験)。 正確 framing: 「Rei stack has stipulated Ω idempotency as axiom + operational test; this paper PROMOTES it to machine-verified theorem」
- ★ §4.7 **二層 architecture の honest 限界**: 上層 Ω は SEED_KERNEL axiom 由来で、 本論ではその冪等性 (Ω∘Ω = Ω) を 1 行 decide proof で形式化、 上層作用の完全な意味論的特徴づけ (BOTH 収束 → 0₀ genesis 層の存在論) は Paper 2 候補に明示送付

### §5. Discussion
- §5.1 STEP 476 TS engine との関係: TS で 5 SeedTheories として 表現済の同型を Lean 4 で機械検証に格上げ
- §5.2 Heidegger 比較 (P-G p. 16 の選択継承、 ただし P-G 自身の Heidegger 限定批判「2 諦 identity まで follow しない」も継承)
- ★ §5.3 **二層 architecture vs Priest-Garfield BOTH-only terminus 差別化** (本論 main differential):
  - Priest-Garfield 2003 は δ(Ω) = BOTH (真な矛盾) で Inclosure を終端
  - 本論: 下層 BOTH (Priest 一致) + 上層 Ω 冪等性で BOTH を ZERO 軸 (= 0₀ genesis 層, ZCSG 三層中央) に収束
  - これは Priest を否定でなく **包含**: 「Priest の Inclosure 結論 (BOTH) は我々の下層に正しく埋め込まれる、 上層 Ω は その上に作用する」 (chat-Claude 2026-05-31 articulated QMRP/Shannon parallel = 先行研究を特殊例として回収する戦略)
  - 機械検証 (Lean 4 zero-sorry) も Priest 2003 が踏んでいない一歩 — 差分二重 (二層分離 + 機械検証)
- ★ §5.4 **ZCSG 三層 (Paper 61) との接続**:
  - ZCSG: o0 (dim −1, NEITHER, 「emptiness-before-emptiness, unnameable」) / 0 (dim 0, ZERO, 「śūnyatā-of-śūnyatā, pure origin」 = 0₀ genesis) / 0o (dim +1, BOTH)
  - 本論 上層 Ω: 下層 BOTH (= ZCSG 0o, dim +1) → ZERO (= ZCSG 0, dim 0, 0₀ genesis 層) への写像
  - これは ZCSG の dim +1 → dim 0 (contraction by 1) として 構造的整合
  - Paper 61 + Paper 1 の連携: notation (ZCSG) + Lean 4 形式化 (本論) で 同一 構造を両側から接近
- §5.5 何を主張しないか:
  - Nāgārjuna が dialetheist だった と断定しない (P-G 2003 自身 rational reconstruction と self-frame)
  - Mathlib 拡張を提案しない (Paper 77 制限継承)
  - 哲学的論争を解決しない (P-G vs Tillemans の 20 年論争にコミットしない)
  - 7 哲学者 gap analysis (STEP 476 西洋哲学比較) は引用のみ、 formal 主張しない
  - **西洋哲学 tier ranking を作らない** (chat-Claude 2026-05-31 訂正 2 永久教訓)
  - **「四段で尽きる有限手続き」 framing 採用しない** (冪等的安定点 Ω∘Ω = Ω に絞る、 四句百非との整合 + Lean 4 形式化負荷最小化)
  - **Ω idempotency が 「既に証明済」 と書かない** (SEED_KERNEL axiom + STEP 513 operational test は既存、 ただし Lean 4 形式証明は本論初 — Pattern 5 防止)
  - **0₀ の完全な存在論的特徴づけ** は本論 scope 外 (Paper 2 候補に明示送付)

### §6. Conclusion
- 既存 3 資産 (STEP 476 + Paper 61 + Paper 77) を つなぐ formal substrate を提供
- 哲学的論争に commit せず、 両 reading と compatible
- Lean 4 で 5-10 秒 build、 Mathlib 不要、 完全 reproducible

### References (試案)
- Garfield & Priest 2003 (本論 core 引用)
- Priest 1987 / 2002 (Inclosure Schema)
- Belnap 1977 (FDE 4 値)
- Tillemans 1999 / 2009 / 2014 (paraconsistent ultimate + scholarly debate)
- Siderits 1989 (「ultimate truth is no ultimate truth」 phrasing)
- Paper 61 ZCSG (Rei prior art)
- Paper 77 LeanDFumt (Lean 4 substrate)
- Nāgārjuna MMK (Garfield 1995 translation)
- 他 Mark Siderits / Ferraro / Tao Jiang / Hayes 等の critic 系

## ★ 次 session protocol refined

step 4 詳細起草 (本 skeleton → 完全 paper draft) を fresh context で実施:

1. 本 memory file + `reference_priest_garfield_2003_nagarjuna_limits_of_thought.md` 再 load
2. `src/axiom-os/nagarjuna-fde-western-engine.ts` を Read tool 再開 (本 file には key 部分のみ抽出済、 詳細 line 番号付きで再確認)
3. Paper 77 LeanDFumt repo (`https://github.com/fc0web/lean-d-fumt8`) を Bash で clone してローカル参照可能化 (optional, 既存知識で十分なら skip)
4. Tillemans 2009/2014/2024 PDF download (藤本さん action) → Read で triangulation 強化
5. Paper 1 outline 詳細起草 (本 skeleton → 各 §段落書き出し → 例 Lean 4 code 完成 → 査読前 draft)
6. Paper 1 draft → 藤本さん review → Lean 4 実装 (実 build + zero-sorry verify) → 査読版 → publish 判断

→ honest 見積もり: 次 session で skeleton → draft v0.1 (各 § 段落出し + Lean 4 code 提案) ~2-3 h、 実 Lean 4 build verify は さらに別 session ~1-2 h、 publish は 数 session 後。 急がない (`feedback_no_rush_publication.md` per)。

## 関連 memory cross-link

- [[reference_priest_garfield_2003_nagarjuna_limits_of_thought]] — 一次資料 honest synthesis + chat-Claude 訂正完全 confirm
- [[project_sages_axes_lens_and_priest_garfield_corrections_2026-05-31]] — STEP 1188 lens + chat-Claude 3 訂正
- [[feedback_world_uniqueness_claim_controllable]] — 「世界初」 controllable 規律 (Paper 1 §4.4 で適用)
- [[feedback_no_rush_publication]] — 急がない publish 規律
- [[feedback_chat_claude_hallucination_warning]] — Pattern 5 警戒 + 私の overreach (tier ranking / Priest 引用強度) 4 例の永久教訓

## 関連 Rei artifact

- Paper 61 ZCSG (DOI 10.5281/zenodo.15217458) — śūnyatā(śūnyatā) = 0 世界初形式化
- Paper 77 LeanDFumt (https://github.com/fc0web/lean-d-fumt8, Apache-2.0) — 8 値 Lean 4 substrate
- STEP 476 `src/axiom-os/nagarjuna-fde-western-engine.ts` (654 行) — Paper 1 の TS prior art
- STEP 513 `src/axiom-os/operator-fixed-point-atlas.ts` — 320 不動点列挙 (Inclosure schema の Rei 既存近接)
- STEP 1188 `#/sages-axes` lens — 8 sage × D-FUMT₈ 地図 (Paper 1 と並列の educational lens)
- 一次資料: `C:/Users/user/rei-aios/external-references/papers/priest-garfield-2003-nagarjuna-limits-of-thought.pdf` (gitignored, 次 session 即 Read 可)