---
name: ★ Paper 112 公開 (12 platform) + STEP 877-878 + Allouche/Korec ladder (2026-04-19)
description: Paper 112 "Nested Colored-Dot" を 12 platform 全投稿 (DOI 10.5281/zenodo.19643419). Classical Density Ladder (Terras/Allouche/Korec) と STEP 878 n=911 power-of-2 ∀n sub-family Lean 4 形式化.
type: project
originSessionId: 2026-04-19-paper112-ladder-step878
---

# Paper 112 + Ladder + STEP 878 session (2026-04-19)

## 一行要約

Paper 112 "Nested Colored-Dot" を 12 platform 全投稿 (DOI 10.5281/zenodo.19643419). 併せて Classical Density Ladder (Terras/Allouche/Korec を Krasikov-Lagarias と同フレームで axiom+corollary 化) + STEP 878 で n=911 の power-of-2 sub-family を Lean 4 ∀n 形式化.

## (1) Paper 112 — 12 platform publish 完走

| Platform | URL |
|---|---|
| Zenodo canonical DOI | https://doi.org/10.5281/zenodo.19643419 |
| Internet Archive | rei-aios-paper-112-1776524696634 |
| Harvard Dataverse | 10.7910/DVN/KC56RY |
| dev.to | nested-colored-dot-symbol-system-... |
| Hatena | 2026/04/19/073519 |
| HackMD | @zCUv2P2UQHGmAOJFPLL_-A/ryVVPt-pWl |
| Notion | Paper-112-Nested-Colored-Dot-Symbol-System |
| Scrapbox | rei-aios project |
| livedoor | archives/12843675.html |
| Software Heritage | SWHID pending |
| Nostr | njump.me/naddr1... (3/5 relay) |
| mathstodon | @Fujimoto/116428097944553460 |

Commit: `ff4b39c`

## (2) STEP 877 (今 session 前半) — Krasikov-Lagarias Lean 4

- `data/lean4-mathlib/CollatzRei/KrasikovLagarias.lean`
- 4 axioms + 10 zero-sorry theorems
- TS cross-check 14/14
- Commit: `ce33102`

## (2b) Classical Density Ladder (Terras/Allouche/Korec)

- `data/lean4-mathlib/CollatzRei/ClassicalDensityLadder.lean`
- 6 axioms + 11 zero-sorry theorems
- 数値 axioms `alpha_Korec_numerical_bounds` (log 3/log 4 ≈ 0.7924) 採用
  - Real.log numerical estimation は Mathlib で煩雑なため
- ladder 不等式: α_K < α_Allouche < 1, α_K > 0.5

### ladder 比較 (zero-sorry)
```
alpha_Korec = log 3 / log 4         (0.79 < α_K < 0.80)
alpha_Allouche = 0.869                (Tao 2019 typesetting 曖昧, numerical 採用)
terras_1976: θ = 1
korec_1994: θ > α_K
allouche_1979: θ > 0.869
density_bound_monotone: θ ≤ θ' → holds θ → holds θ'
```

### 構造的事実

- Korec 1994 strictly strengthens Terras (covers α_K < θ ≤ 1)
- Allouche 1979 is subsumed by Korec (higher threshold, fewer θ)
- Tao 2019 (log density 1 + any f→∞) は別フレーム (本 file の pow-form は natural density)

## (3) STEP 878 — n=911 power-of-2 ∀n sub-family

- `data/lean4-mathlib/CollatzRei/Step878N911Subclass.lean`
- 12 theorems zero-sorry, zero axiom
- lake build 成功 (4.4s)

### 主要定理

```lean
-- General ∀n: 2^k · n reaches n in exactly k steps
theorem collatzIter_two_pow (k n : Nat) :
    collatzIter k (2^k * n) = n

-- Specialization to n=911 (Problem 011 ∀n upgrade)
theorem two_pow_times_911_reaches_911 (k : Nat) :
    collatzIter k (2^k * 911) = 911

-- Same for n=91, n=3077, n=1 (Rei landmarks)
theorem two_pow_91_visits_91
theorem two_pow_3077_visits_3077
theorem two_pow_1_visits_1

-- Sub-family cardinality
theorem two_pow_911_family_injective :
    Function.Injective (fun k : Nat => 2^k * 911)
```

### ∀n の位置付け

- **STEP 875 (Problem 011)**: 25 specific atomic cores all visit 911 (native_decide)
- **STEP 878 (本)**: **infinite** sub-family `{2^k · n}` for any n visits n (including n=911) — pure structural proof

### 残 gap

Arithmetic predecessors (奇数 m with 3m+1 = 2^k · target) は Collatz-inverse tree 全体を構成. 本 STEP は power-of-2 branch のみをカバー. ∀n for mod-32 residue classes は empirical ~40% で **not 100%** のため成立しない.

### TS empirical 確認

`tmp/mod32-analysis.ts`:
- mod 32 residue classes 全てで visit-911 rate = 35〜45%
- 100% 成立する residue class 不在 → mod-class ベース ∀n 成立不可
- 代わりに structural (power-of-2) sub-family が ∀n を満たす

## 環境

- Mathlib v4.27.0, Lean 4 v4.29.0
- `Mathlib.Algebra.GroupPower.Basic` は v4.27.0 に存在せず → `Mathlib.Tactic.Basic` + 手動 `Nat.pow_succ, Nat.mul_comm, Nat.mul_assoc` で代替

## 今日の累積成果 (session 2026-04-18→19)

| STEP | File | Theorems | Status |
|---|---|---|---|
| 874 | LayerDNestedDot | 16+ | zero-sorry |
| 875 | Problem011N911OnRamp | 47 | zero-sorry |
| 876 | Tier2ResidualBound | 5 | zero-sorry |
| 877 | KrasikovLagarias | 10 | 4 axioms + zero-sorry |
| 877b | ClassicalDensityLadder | 11 | 6 axioms + zero-sorry |
| 878 | Step878N911Subclass | 12 | zero-sorry |
| **合計** | **6 files** | **101+** | **zero-sorry** |

Paper 112 published to 12 platforms (all-time record for Rei-AIOS paper).

## 次の候補

- Paper 112 を retroactively 他 past papers の mathstodon へ展開 (実施済: 108-111)
- OEIS 投稿 (Task 12, 藤本 action pending)
- rei-unsolved-problems v1.0.0 release (藤本 action pending)
- STEP 879: n=911 arithmetic predecessor tree の部分 ∀n 形式化
- Korec 1994 の algebraic derivation を Lean 4 に精密化 (log 3/log 4 numerical bound 厳格化)