Rei-Collatz Lean 4 Blueprint Pilot v0.1 — leanblueprint methodology adoption on Rei stack (archival preservation, ZERO new IP)

This article is a re-publication of Rei-AIOS Blueprint Pilot v0.1 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:

• Zenodo (DOI, canonical): https://doi.org/10.5281/zenodo.22051191
• GitHub source (private): https://github.com/fc0web/rei-aios Author: Nobuki Fujimoto (@fc0web) · ORCID 0009-0004-6019-9258 · License CC-BY-4.0 ---

Scope: STEP 614 + 622 + 623 + 624 THE_THEOREM chain, 48 theorems, zero sorry.
Date: 2026-08-09 pilot draft.
Origin: chat-Claude 2026-08-09 dialogue turn 7 offered content.tex骨格作成; 藤本さん Option A で 実行判断 pending → 2026-08-10 pilot 起動。
Migration plan: memory/project_blueprint_migration_candidate_2026-08-09.md

What is this?

A minimal leanblueprint-compatible blueprint for the Rei Collatz
proof-chain. The blueprint records LaTeX prose statements of 48
formalized theorems, tags each with \lean{fqname} (Lean 4
declaration name) + \leanok (fully formalized marker) + \uses{...}
(dependency DAG edges).

The point is not to prove Collatz (see honest scope in
src/content.tex Chapter 1 + Chapter 12). The point is to
demonstrate the leanblueprint methodology on a real Rei subset,
so that subsequent migration decisions can be based on operational
experience rather than concept.

Files

blueprint/
├── README.md              (this file)
└── src/
    ├── content.tex        Main body (Chapter 1-12, 48 theorems + prose + \uses DAG)
    ├── print.tex          PDF wrapper (loads amsthm etc, calls \input{content})
    ├── web.tex            HTML wrapper (for leanblueprint serve)
    └── macros/
        └── common.tex     \lean, \leanok, \uses, \notready fallback definitions

To run locally (future)

Prerequisites: Python 3.10+, TeX Live 2023+, node.js (for leanblueprint serve).

pip install leanblueprint
cd data/lean4-transfer/blueprint
leanblueprint pdf         # generates blueprint.pdf
leanblueprint serve       # local server at http://localhost:8080 with dependency graph
leanblueprint checkdecls  # verifies each \lean{name} resolves to a real Lean decl (requires proper lakefile.lean)

Caveat: checkdecls requires the underlying Lean project to be
lake build-clean with the STEP 614-624 files imported. Currently
data/lean4-transfer/ is a flat directory of standalone experimental
scripts without a lakefile.lean --- so checkdecls will not work
until stage (iii) of the migration plan (wire the STEP files into
data/lean4-mathlib/CollatzRei/ or create a dedicated
data/lean4-transfer/lakefile.lean project).

The \lean{name} tags in content.tex use bare declaration names
(matching the top-level theorem name in each STEP file). If the
migration moves declarations under a namespace CollatzRei prefix,
the \lean tags will need to be updated to the fully-qualified names
(e.g. CollatzRei.THE_THEOREM).

Honest scope (see src/content.tex Chapter 1 for full version)

• Zero sorry: 48 theorems, no acknowledged gaps at Carneiro's layer (3) (证明检查).
• native_decide caveat: 12 theorems (batch_10000 + b1-b11) use native_decide, which expands the TCB to the entire Lean compiler. This is explicitly flagged in Chapter 10 ("Batch Verification and Base Cases") and cross-references feedback_zero_sorry_floor_not_ceiling.md 2026-08-09 refine.
• Not a Collatz proof: the genuine mathematical gap (trailing 1-bits >= 4 wall for n%32 in {15, 31}) is documented verbatim in Chapter 12 ("Honest Assessment: The Genuine Mathematical Gap").
• 2026-07-28 kernel bug context: This pilot was authored days after Lean 4 issue #14576. The STEP 614-624 chain uses only bare inductive types and is not directly affected. See Chapter 1 Remark 1.4 for details.

What this pilot demonstrates (Chapter 12 Remark 12.1 verbatim)

• (i) leanblueprint methodology applied to a real Rei stack subset.
• (ii) A working \uses DAG that would allow color-coded formalization progress tracking if imported into a proper Lake project.
• (iii) Explicit 4-layer TCB annotation per 2026-08-09 feedback_zero_sorry_floor_not_ceiling.md refine.

What this pilot does NOT demonstrate

• (a) A Collatz proof (see Chapter 12 gap).
• (b) Novel mathematical content beyond STEP 614-624 (produced 2026-04 to 2026-05, see CLAUDE.md).
• (c) leanblueprint checkdecls success (see "To run locally" caveat).

Next steps (藤本さん judgment)

• Stage (i) DONE (2026-08-10 pilot): content.tex 骨格 generated.
• Stage (ii) DONE (2026-08-10 pilot): ~40 \uses edges captured.
• Stage (iii) PARTIAL (2026-08-10 Option D): lakefile.toml + lean-toolchain + CollatzChain.lean scaffolding created at data/lean4-transfer/, but architectural constraint discovered (see below).
• Stage (iv) PENDING: leanblueprint serve deploy to public/tools/rei-collatz-blueprint/ per 2026-08-06 藤本さん永久 protocol.

Stage (iii) Option D — Architectural constraint findings (2026-08-10)

Created:

• data/lean4-transfer/lakefile.toml (mathlib v4.27.0 依存、 pilot scope)
• data/lean4-transfer/lean-toolchain (leanprover/lean4:v4.27.0)
• data/lean4-transfer/CollatzChain.lean (namespace-wrapped 6 declarations: cs, ci, reaches1, exhaustive, exhaustive_parity, exhaustive_odd — pattern demonstration)
• data/lean4-transfer/.gitignore (Lake artifacts)
• leanblueprint (v0.0.20) + rich_click 依存 installed globally.

Architectural constraint discovered:

leanblueprint (v0.0.20, client.py:238) uses git.Repo(...).working_dir to locate the lakefile:

lakefile_lean_path = Path(repo.working_dir)/"lakefile.lean"
lakefile_toml_path = Path(repo.working_dir)/"lakefile.toml"

This means leanblueprint expects the lakefile at the git repository root, not in a subdirectory.
For Rei-AIOS (single git repo with Lean projects in data/lean4-transfer/ + data/lean4-mathlib/ subdirs),
neither existing lakefile is at git root, so leanblueprint commands fail with:

Error: Could not find lakefile.lean or lakefile.toml in C:\Users\user\rei-aios

Verified: setting GIT_WORK_TREE / GIT_DIR env vars does not override this (GitPython calls git rev-parse --show-toplevel).

Stage (iii) full completion options (藤本さん judgment 領域):

Option	Approach	Pros	Cons
(a) Move lakefile to git root	Add lakefile.toml at C:\Users\user\rei-aios\	Direct fix	Breaks existing convention (data/lean4-mathlib/ is the canonical Lean project); risks name collision
(b) Git submodule	Make data/lean4-transfer/ its own git repo, add as submodule	Isolates Lean project	Invasive restructuring; complicates rei-aios repo management
(c) Upstream leanblueprint PR	Fork PatrickMassot/leanblueprint to accept --project-root CLI option	Cleanest long-term	Requires upstream review + release cycle
(d) Document limitation	Accept that stage (iii) checkdecls is not directly usable in current repo layout	Zero further work	Blueprint DAG can still be built with leanblueprint pdf / serve, but declaration existence checking must be manual
(e) Wire into data/lean4-mathlib/	Add step614-624 modules under data/lean4-mathlib/CollatzRei/Chain/ namespace	Reuses existing Lake project	Still hits constraint (mathlib dir is also subdirectory); requires (a) first

Recommendation (Rei-side reading, 藤本さん judgment 領域): Option (c) or (d) depending on priority. Option (a) has the highest structural risk (existing convention breakage per CLAUDE.md).

2026-08-10 追加 (Option D 完全化): 藤本さん Option (d) 「制約 accept + 手動 checkdecls」 選択 (Option (c) upstream PR は feedback-external-community-outreach-premature tension で 別 STEP)。

Rei-side 手動 checkdecls script 実装: scripts/check-lean-decls.ts (198 行 TypeScript)。

Usage:

cd C:/Users/user/rei-aios
npx tsx data/lean4-transfer/blueprint/scripts/check-lean-decls.ts
# Exit 0 if all decls found, 1 if any missing (CI-friendly)

2026-08-10 実行結果:

• Total \lean{...} tags parsed: 67 (fqname placeholder comment 除外後)
• Found in Lean files: 67 (100%)
• Missing: 0
• Duplicates (expected): 53 (STEP 614/622/623/624 standalone scripts で cs/ci/reaches1 等 重複定義、 standalone script 性質による intentional)
• Overall status: PASS

Honest scope:

• grep-based lookup、 Lean 4 kernel formal verification ではない
• Type signature 一致は verify しない (name 存在のみ)
• Duplicates expected: STEP 622/623/624 standalone scripts で cs/ci/reaches1 等 重複定義 (script 性質)
• Kernel-level verification が必要な場合: Option (c) leanblueprint upstream PR or Option (e) data/lean4-mathlib/CollatzRei/ 統合 が別途必要

この実装で achieved:

• ✅ Blueprint content.tex \lean{...} tag 全 (67/67) が Lean file に 実在 verify
• ✅ Rei-side 独自 checkdecls (grep-based approximation) が Option (d) 選択の operational instance
• ✅ CI-friendly exit code (0/1) で 将来 pre-commit hook / cron 統合 可能

Stage (iii) status 更新:

• (a) content.tex format = DONE
• (b) \uses DAG = DONE (~40 edges)
• (c) leanblueprint CLI 統合 = PARTIAL (leanblueprint upstream 制約 + Rei-side 手動 checkdecls script 代替実装で PASS)
• Overall stage (iii) = OPERATIONAL (Blueprint pilot の 「命題忠実性 = 人間責任」 layer が Rei-side script で automatable)

What Option D pilot demonstrated

• ✅ leanblueprint (v0.0.20) available in Rei environment
• ✅ Lake project scaffolding pattern (lakefile.toml + lean-toolchain + namespace-wrapped module)
• ✅ CollatzChain.lean = 6 core declarations from STEP 622-624 wrapped in namespace CollatzChain (pattern for full 48-theorem migration)
• ⚠ Architectural constraint: leanblueprint's git-root assumption incompatible with Rei sub-directory Lean project layout
• 📝 5-option decision matrix for stage (iii) full completion (藤本さん judgment)

What Option D pilot does NOT demonstrate

• (a) lake update execution (not run; would fetch mathlib v4.27.0 ~15-30 min, network + disk cost)
• (b) lake build CollatzChain execution (blocked by (a))
• (c) leanblueprint checkdecls execution (blocked by architectural constraint above)
• (d) Full 48-theorem namespace migration (only 6 core declarations wrapped as demonstration)

Related memory

• feedback_no_rush_publication.md 2026-08-09 addition (external technical追認 by chat-Claude)
• feedback_zero_sorry_floor_not_ceiling.md 2026-08-09 refine (4-layer TCB gauge)
• project_session_2026-08-09_chat_claude_math_universe_arc.md (7 turn dialogue archival)
• project_blueprint_migration_candidate_2026-08-09.md (3-stage migration plan)
• CLAUDE.md STEP 614-624 (source proof-chain)