---
name: ★★★ STEP 874 — Layer D NestedDot + QR 超え検証 + Paper 112 draft ★★★
description: 2026-04-18 Layer D (NestedDot inductive × RGB 24-bit) 完走. Lean 4 zero-sorry formalization / 22+36 TS tests pass / QR v40 L を depth-3 100×100 で 25×, depth-4 100³ で 2523× 超越確認 / Paper 112 draft 完成.
type: project
originSessionId: 2026-04-18-layer-d-step874
---

# STEP 874 — Layer D NestedDot + QR 超越 + Paper 112 draft

## 概要 (一行)

藤本無限次元ドット理論 Layer D (NestedDot inductive 型 × RGB 24-bit × 再帰構造) を Lean 4 zero-sorry で形式化し、QR code v40 L 容量を depth-3 で 25×, depth-4 で 2523× 超越することを実測 + 形式証明 + PNG round-trip 確認 → Paper 112 draft 完成.

## W-D1 〜 W-D5 全完走

### W-D1: Lean 4 Layer D 形式化 (zero-sorry)
- **File**: `data/lean4-mathlib/CollatzRei/LayerDNestedDot.lean`
- `ColoredDot` = `DFumt8 × Fin 16777216` (RGB 24-bit)
- `NestedDot` inductive (leaf / compound)
- Mutual recursive `depth`, `bitSize` (LEAF_BITS=43, COORD_BITS=16)
- 12 theorems + 4 QR 超越 theorems proved via `decide`
- **Layer B ↪ Layer D embedding** (`embedLayerB_injective`) 証明
- Build: `lake build CollatzRei.LayerDNestedDot` ✓ 24s, 703 jobs

### W-D2: 情報量 benchmark (22/22 pass)
- **File**: `test/wd2-density-vs-qr-test.ts`
- depth 1 leaf = 43 bit
- depth 2 flat (401 leaves) = 23,702 bit > QR v40 L (23,624, 1.003×)
- depth 3 (100×100) = **595,943 bit = 25.2× QR v40 L**
- depth 4 (100³) = **59,595,943 bit = 2,523× QR v40 L**
- 最小 leaf 数: QR v1=2, v10=37, v25=173, v40=400

### W-D3: PNG encoder
- **File**: `scripts/encode-nested-dot-to-png.ts`
- 4-pixel header (leaf vs compound marker で分岐)
- 均一 child slot layout (cols × rows = ⌈√k⌉ × ⌈k/cols⌉)
- slot dims を header に埋め込み decoder が再構築可能
- pngjs 依存 (package.json に追加)

### W-D4: PNG decoder + round-trip (36/36 pass)
- **File**: `scripts/decode-png-to-nested-dot.ts`, `test/wd4-roundtrip-test.ts`
- 12 sample 全て structural equality + depth + bitSize 保存:
  - depth 2 flat (10/50/200/401 leaves)
  - depth 3 (5×5, 10×10)
  - diverse color (16/64/256)
  - empty compound, single leaf root, mixed leaf+compound siblings

### W-D5: Paper 112 draft
- **File**: `papers/paper-112-nested-colored-dot-vs-qr.md`
- 10 sections + honest limitations (ECC なし / physical readability 未対応 / 45% density / QR 代替ではない positioning)
- 5-axis comparison table
- Lean 4 theorem 列挙 + TS benchmark 結果 + round-trip 結果
- Paper 83 原則遵守: "QR superseded" claim なし, complementary positioning

## 数値ハイライト

| 構成 | bits | vs QR v40 L |
|---|---|---|
| depth 1 leaf | 43 | 0.002× |
| depth 2 flat 401 | 23,702 | 1.003× |
| depth 3 (100×100) | 595,943 | **25.2×** |
| depth 4 (100³) | 59,595,943 | **2,523×** |

## 主要 Lean 4 定理 (全 zero-sorry)

```
depth_leaf / bitSize_leaf                   -- rfl
depth_positive / bitSize_geq_leaf           -- 全 NestedDot >= base
bitSizeList_flat (n) = n*(COORD+LEAF)       -- induction + ring
bitSize_flat_compound (n) = LEAF+n*(16+43)
bitSizeList_compoundListDepth2              -- depth-3 closed form
embedLayerB_injective                       -- Layer B ↪ Layer D
depth2_flat_3_exceeds_qr_v1L                -- decide
depth2_flat_37_exceeds_qr_v10L              -- decide
depth2_flat_401_exceeds_qr_v40L             -- decide
depth3_100x100_exceeds_qr_v40L_18x          -- decide
LayerD_summary                              -- 4-tuple 統合
```

## 既存文脈との関係

- **Paper 33** Layer C (Braille-DFumt8 discrete)
- **Paper 69** Schnorr × DFumt8
- **Paper 110** Layer B comparison with CLIP/BERT
- **Paper 111** Rei vs Santana (Collatz)
- **Paper 112** Layer D NestedDot vs QR (**本 track**)

Problem008FDAFIDT.lean の `InfiniteDot` = Layer B "平坦" 版が、`embedLayerB` で `NestedDot.leaf` に単射埋込される. Layer B の全定理は Layer D の leaf sub-type 上で lift 可能.

## pending (次 session 候補)

1. **Paper 112 publish** — 11 platform (Zenodo / IA / Harvard / dev.to / Hatena / HackMD / Notion / Scrapbox / livedoor / Nostr + pending Software Heritage SWHID)
2. **Reed–Solomon ECC layer** — 単純 bit flip で leaf/compound marker が壊れる問題の対策
3. **Bit-packed encoding** — 現 45% density を 90%+ に改善 (leaf を 2 pixels に)
4. **Finder pattern** — 印刷→再スキャン対応
5. **Layer E (draft idea)** — NestedDot 上に continuous embedding field (Paper 110 CLIP 比較への bridge)

## 環境

- Lean 4 v4.29.0, Mathlib v4.27.0
- Node v22.14.0, pngjs installed
- OS: Windows 11 Pro Git Bash
- 全 build + test in ~2 時間

## 重要注意点

- NestedDot は QR の "consumer replacement" 主張しない (Paper 83 原則)
- Physical readability, print/scan tolerance, ECC, 標準化は全て honest limitation として明記
- **raw bit capacity での超越は数学的に自明**, 意味論の豊かさが真の差別化ポイント