Rei Collatz Blueprint (Pilot) — STEP 622-624 THE_THEOREM 48 定理
この Blueprint pilot は何か
Patrick Massot leanblueprint 方式 (sphere eversion + Liquid Tensor Experiment + Tao PFR project 採用) の Rei-side 最小 viable 実装。 STEP 614/622/623/624 THE_THEOREM chain 48 定理を LaTeX 散文 + \lean{name} tag + \leanok marker + \uses{...} DAG で 記述。 Collatz 予想の proof ではない (STEP 624 §7.1 「genuine mathematical gap: trailing 1-bits ≥ 4 wall for n%32 ∈ {15, 31}」 は 永続 open)。
Load-bearing 目的: (1) chat-Claude turn 7 blueprint 方式 offer の Rei-side 独立実装 pilot / (2) 「命題忠実性 = 人間責任」 (chat-Claude 3 打ち手 (iii)) の operational 実装 substrate / (3) 4 層 TCB annotation ([[feedback-zero-sorry-floor-not-ceiling]] 2026-08-09 refine) の 実 blueprint 内 embedding。
作成 file 一覧
| File | 行数 | 内容 |
|---|---|---|
data/lean4-transfer/blueprint/src/content.tex | 593 | LaTeX 散文 + 12 chapters + 48 定理 全 \lean tag + \uses DAG ~40 edges + 4 層 TCB annotation |
data/lean4-transfer/blueprint/src/print.tex | 41 | PDF wrapper (documentclass + amsthm + hyperref + macros + content) |
data/lean4-transfer/blueprint/src/web.tex | 36 | HTML wrapper (leanblueprint serve 用) |
data/lean4-transfer/blueprint/src/macros/common.tex | 23 | \lean/\leanok/\uses/\notready fallback definitions |
data/lean4-transfer/blueprint/README.md | 146 | 使用方法 + honest scope + stage 進捗 + 5-option 決定 matrix |
data/lean4-transfer/blueprint/scripts/check-lean-decls.ts | 198 | Rei-side 手動 checkdecls (grep-based, Option (d) 実装) |
data/lean4-transfer/lakefile.toml + lean-toolchain + CollatzChain.lean | ~80 | Lake project 骨格 (namespace-wrapped 6 core declarations demo) |
Content.tex 12 chapters 構造
- Introduction and Honest Scope — Rei Collatz proof-chain 概要 + zero-sorry + 4 層 gauge + 2026-07-28 Lean kernel bug #14576 context (Rei stack は bare inductive Nat のみで影響なし、 fortunate coincidence 明示)
- Core Definitions —
cs,ci,reaches1,descentBound - Foundational Lemmas (STEP 614) —
three_half,pow2_lt,half_sub,core_mod,core_neq,sum_mod_ind,sum_mod,rw_mul - THE_THEOREM: Trailing Ones Descent (STEP 614) — 中心結果 (t1 strict decrease at v=1 step)
- Exhaustive Modular Coverage (STEP 622) —
exhaustive,exhaustive_parity,exhaustive_odd,exhaustive_mod4_3,descent_all - Descent Lemmas: Cases 1--4 (STEP 623, 624) —
ddc,div2x2,div2x3,ci_add,case1_lt..case4_lt - Descent Lemmas: Cases 5, 7 Sub-classes (STEP 624) —
case5a_lt,case7a_lt..case7g_lt - Descent Lemmas: Case 6 Sub-classes (STEP 624) —
case6a_lt,case6b_lt - Individual Trailing Ones Descent (STEP 624) —
v2_descent,gk1..gk10 - Batch Verification and Base Cases (STEP 624) —
iter_reaches1,check_range,batch_10000,b1..b11,strong_ind(12 定理native_decide使用、 TCB expanded 明示) - (未使用 chapter)
- Honest Assessment: The Genuine Mathematical Gap — STEP 624 §7.1 verbatim + 4 層 TCB annotation
Rei-side 手動 checkdecls 実行結果 (2026-08-10)
Option D 「制約 accept + 手動 checkdecls」 実装 = scripts/check-lean-decls.ts で content.tex 内 全 \lean{...} tag を parse + data/lean4-transfer/step*.lean に対して grep で existence check。
Total \lean{...} tags parsed: 67 (fqname placeholder 除外後)
Found in Lean files: 67 (100%)
Missing: 0
Duplicates (expected): 53 (STEP 614/622/623/624 standalone scripts の重複定義)
Overall status: PASS
CI-friendly exit code (0/1) で 将来 pre-commit hook / cron 統合可能。 Kernel-level verification ではなく grep-based lookup — Option (c) leanblueprint upstream PR or Option (e) data/lean4-mathlib/CollatzRei/ 統合 が完全実装。
Option D architectural 制約 (2026-08-10 発見)
leanblueprint (v0.0.20, client.py:238) は git repo root に lakefile 要求 (git.Repo().working_dir 使用)。 Rei-AIOS は 単一 git repo で 全 Lean 投影を subdirectory 化 (data/lean4-transfer/ + data/lean4-mathlib/) = **直接互換なし**。 GIT_WORK_TREE/GIT_DIR env override 効かず (GitPython 内 git rev-parse --show-toplevel 呼出)。
5-option 決定 matrix
| Option | Approach | Pros | Cons | Status |
|---|---|---|---|---|
| (a) | lakefile を git root へ移動 | Direct fix | 既存 convention 破壊 risk | reject |
| (b) | Git submodule 化 | isolate | 侵襲的 | defer |
| (c) | upstream PR (--project-root option) | 綺麗 | [[feedback-external-community-outreach-premature]] tension | defer |
| (d) | 制約 accept + 手動 checkdecls script | 追加 work 少 + Rei-side control | kernel verify 自動化 断念 | SELECTED (2026-08-10) |
| (e) | data/lean4-mathlib/CollatzRei/ 統合 | 既 project 再利用 | (a) 必要 + namespace 統合大工事 | defer |
Honest scope
- Collatz 予想 proof ではない — STEP 624 §7.1 「genuine mathematical gap trailing 1-bits ≥ 4 wall for n%32 ∈ {15, 31}」 永続 open
- 48 定理は Carneiro 4 層のうち (3) 証明検査 floor のみ — 12 定理 (batch_10000 + b1..b11) は
native_decide使用 = TCB expanded to Lean compiler 全体 ([[feedback-zero-sorry-floor-not-ceiling]] 2026-08-09 refine 適用) - 2026-07-28 Lean kernel bug #14576 影響なし = Rei STEP 614-624 chain は bare inductive Nat のみ (nested inductive types 未使用)、 fortunate coincidence 明示 (designed defence でない)
- grep 49 vs self-report 48 の 1 drift honestly flag (「48」 を load-bearing 数値として採用)
- 「48 定理で Collatz 解決」 inflation + 「既知 lemma re-typing」 deflation 両方 reject、 truthful 記述 = 「machine-verified $t_1$-descent invariant + 明示的 gap annotation」
- 「新しい成果」 ではない — STEP 622-624 は 2026-04〜05 実装済成果、 本 pilot は 集約 site 反映 + blueprint 方式 methodology 適用 のみ
★★★ STEP 1311+1312 拡張 update (2026-08-10、 content-expansion merge)
初版 pilot (48 定理 + 4 層 TCB annotation + Option D 制約 accept 手動 checkdecls 67/67 PASS) から、 chat-Claude turn 8 「blueprint = 装置」 議論継承で content-expansion-2026-08-10.tex (240 行、 3 chapter) を main content.tex に \input merge。 手動 checkdecls は multi-tex file scan + multi-lean-dir scan + \notready-aware filter 拡張で 73/73 PASS with 3 \notready skipped (67 base + 6 expansion tags)。
拡張 3 chapter 追加内容
| Chapter | Origin STEP | 内容 | Lean 4 source (別 dir) |
|---|---|---|---|
| Ch 13 STEP 830 Büchi × Collatz Bridge | STEP 830 arc | Büchi automaton alphabet + Cobham 独立性 (base 2 halving + base 3 3n+1) の 2 declarations \notready marker (proposed, chat-Claude turn 4 「壁の内側から触る」 pattern) | data/lean4-mathlib/CollatzRei/Buchi25Bridge.lean (23 decls) |
| Ch 14 STEP 1215 D-FUMT₈ Category with SELF⟲ | STEP 1215 (2026-06-14) | Dfumt8 8 値 type + and8 non-associativity (BOTH ∧ NEITHER ∧ INFINITY witness) + TRUE identity 3 declarations \leanok axiom-free (Mathlib base only) — 三段目 (冪) と 同 「richness vs associativity tradeoff」 の operational instance | data/lean4-mathlib/CollatzRei/Dfumt8CategoryExperiment.lean (22 decls) |
| ★★★ Ch 15 STEP 1220 Lawvere fp + SELF⟲ Structural Incompatibility | STEP 1220 (2026-06-15) + 2026-08-10 chat-Claude turn 8 | Lawvere fixed-point 一般形 + D-FUMT₈ SELF⟲ = Fix(R) instance の 2 declarations \leanok + ★ SELF⟲ = Fix(R) blueprint 装置 structural incompatibility remark = chat-Claude turn 8 「DAG に乗らない構造 = 循環依存 + 自己言及 = 一つのノードに押し潰すしかない」 の 明示 documentation | data/lean4-mathlib/CollatzRei/LawvereFixedPointExperiment.lean (10 decls) |
★★★ SELF⟲ blueprint 装置 structural incompatibility (Ch 15 Remark)
「DAG に乗らない構造 — 循環的な依存、 自己言及、 相互再帰的な定義。 SELF⟲ = Fix(R) のような不動点は、 blueprint の記法では一つのノードとして押し潰すしかない」 (chat-Claude 2026-08-10 turn 8 verbatim)
Blueprint pilot は 2026-07-26 藤本さん承認 「D-FUMT₈ 第 3 原始概念 = 龍樹空」 (SELF⟲ = Fix(R)) の Rei stack core primitive を **技術的に captureできない** ことを、 Ch 15 で 明示 documentation。 Blueprint 装置は acyclic dependency management 用に設計されており、 意図的 循環構造 (SELF⟲) は shape で faithful に表現不可 = **Rei stack 全体を Blueprint faithful に 表現するのは不可能、 一部 view のみ** の operational 制約 明示。
Manual checkdecls script v2 拡張
- Multi-tex scan:
content.tex+content-*.texpattern で 全 tex file 走査 - Multi-lean-dir scan:
data/lean4-transfer/+data/lean4-mathlib/CollatzRei/2 dir 統合走査 - \notready-aware filter: 各
\lean{...}tag の 前後 5 行以内に\notreadyが あれば **skip** (未実装宣言として意図的除外) - Namespace bare-name lookup:
Buchi25Bridge.buchi_cobham_independence→ bare namebuchi_cobham_independenceで grep (namespace 差 tolerant)
Total \lean{...} tags parsed: 76 (fqname + 3 \notready 除外後 = 73)
Found in Lean files: 73 (100%)
Missing: 0
Duplicates (expected): 55 (STEP 614-624 standalone + CollatzRei 内 重複)
Overall status: PASS
関連 memory + 次段 items
- GitHub source (data/lean4-transfer/blueprint/)
- memory
project_session_2026-08-09_chat_claude_math_universe_arc.md(9 turn dialogue archival) - memory
project_blueprint_migration_candidate_2026-08-09.md(3-stage migration plan) feedback_no_rush_publication.md2026-08-09 追記 (blueprint = 精度側 discipline 技術定式化)feedback_zero_sorry_floor_not_ceiling.md2026-08-09 追記 (4 層 TCB refine)- CLAUDE.md STEP 614-624 (source proof-chain)
次段 candidate (藤本さん judgment 領域)
- Stage (iii) full:
data/lean4-mathlib/CollatzRei/Chain/namespace 統合 (Option (e)) - Stage (iv):
leanblueprint serveHTML deploy - Pilot 拡張: STEP 830 Büchi arc + STEP 1215 D-FUMT₈ Category + STEP 1220 Lawvere fp を blueprint 追加 (但し SELF⟲ blueprint 装置 structural incompatibility 判明済、 chat-Claude turn 8 参照)