---
name: project-step1217-zcsg-smallcategory-paper61-machine-verification
description: "STEP 1217 (2026-06-15) — Paper 61 ZCSG 三層 (o0 / 0 / 0o, dim -1 / 0 / +1) を Lean 4 で Preorder + mathlib SmallCategory instance auto-derive。 axiom-free zero-sorry 達成 (propext + Classical.choice + Quot.sound のみ)。 藤本さん初期理論 × STEP 1215 mathlib Category 道具の最初の structural addition 接続 (5 候補中 (B))。 functor `Dfumt8 → Zcsg3` candidate は将来 STEP 範囲外 honest scope 明示"
metadata: 
  node_type: memory
  type: project
  originSessionId: ae728468-271e-4824-a6e9-dc58efd76f82
---

# STEP 1217 — ZCSG × mathlib SmallCategory instance (Paper 61 機械検証)

## 概要

藤本さん指示「初期理論 × 今 session 道具」 5 候補 (A-E) のうち、 Rei 推奨 (B) を即着手 implementation。

**目的**: Paper 61 ZCSG (Zero-Centered Symbol Grammar, チャット版 Claude 共著) の三層構造 (o0 / 0 / 0o, dim -1 / 0 / +1) を Lean 4 で **inductive type + dimension 関数 + Int 経由 Preorder instance** として実装し、 mathlib `Preorder.smallCategory` 経由で SmallCategory instance を **auto-derive**。

これは STEP 1215 (Dfumt8CategoryExperiment) で D-FUMT₈ 8 値が `instCategoryDfumt8 : SmallCategory Dfumt8` を Preorder.smallCategory 経由で持つことを confirm した方法論を、 **ZCSG 三層 (より coarse な layer)** に axiom-free で適用するもの。

## 実装内容

`data/lean4-mathlib/CollatzRei/ZcsgCategoryExperiment.lean` 新規 (~170 行):

### Section 1: inductive type
```lean
inductive Zcsg3
  | O0     -- o0  収束 dim -1
  | O      -- 0   原点 dim  0
  | OO     -- 0o  展開 dim +1
  deriving DecidableEq, Fintype, Repr
```

### Section 2: dimension 関数 (Paper 61 literal mapping)
```lean
def Zcsg3.dim : Zcsg3 → Int
  | O0 => -1
  | O  => 0
  | OO => 1
```

### Section 3: Preorder instance (dim pullback)
```lean
instance instPreorderZcsg3 : Preorder Zcsg3 where
  le a b := Zcsg3.dim a ≤ Zcsg3.dim b
  le_refl _ := le_refl _
  le_trans _ _ _ hab hbc := le_trans hab hbc
```

### Section 4: SmallCategory auto-derive
```lean
instance instSmallCategoryZcsg3 : CategoryTheory.SmallCategory Zcsg3 :=
  Preorder.smallCategory Zcsg3
```

### Section 5-6: smoke test theorems
- `zcsg_linear_order` (O0 ≤ O ∧ O ≤ OO ∧ O0 ≤ OO)
- `zcsg_not_descending` (¬ OO ≤ O0)
- `zcsg_self_le_self` (reflexivity)
- `zcsg_transitive_o0_to_oo` (transitivity 経由)
- `zcsg_card_three` (constructive: ∀ x, x = O0 ∨ x = O ∨ x = OO)
- `zcsg_id_exists` (Category 内恒等射の存在)

### Section 7: D-FUMT₈ ↔ ZCSG functor candidate (将来 STEP 範囲外 honest scope)

D-FUMT₈ (STEP 1215) と ZCSG 三層を繋ぐ functor `Dfumt8 → Zcsg3` (8 軸 → 3 層 coarse projection) は両者の dim 関数 compatibility 経由で**候補**になるが、 functor laws (id 保存 + 合成保存) の axiom-free proof は本 STEP の範囲外で、 将来 STEP 候補。

例 mapping (Paper 61 + 62 から literal 正当化可能だが未証明):
```
TRUE / FALSE / BOTH         ↦ OO (展開 dim +1)
ZERO / SELF                 ↦ O  (原点 dim 0)
NEITHER / INFINITY / FLOWING ↦ O0 (収束 dim -1)
```

functor 成立すれば STEP 1215 Dfumt8 Category と本 Zcsg3 Category が mathlib CategoryTheory.Functor で繋がり、 D-FUMT₈ 8 軸 detailed lens と ZCSG 3 層 coarse lens の formal projection が確立する = Paper 61 + 62 + 65 三者統合の Lean 4 evidence candidate。

但し、 hasAbsorberOver (STEP 1215 構造的不変量) が functor を通して保たれるかは別問題で、 D-FUMT₈ 5 吸収子 (SELF) が ZCSG O (原点) で何に対応するかは藤本さん哲学的判断を要する。

## Verify 結果

### Build
```
✔ [620/620] Built CollatzRei.ZcsgCategoryExperiment (6.9s)
Build completed successfully (620 jobs).
```

### Axiom dependencies (zero-sorry verify)
```
zcsg_linear_order          : [propext, Classical.choice, Quot.sound]
zcsg_not_descending        : [propext, Classical.choice, Quot.sound]
zcsg_transitive_o0_to_oo   : [propext, Classical.choice, Quot.sound]
zcsg_card_three            : [propext]                              ← constructive
instSmallCategoryZcsg3     : [propext, Classical.choice, Quot.sound]
```

**sorryAx / native_decide 全 0** = axiom-free zero-sorry 完全達成。 STEP 1215 と同じ axiom base (mathlib 標準)。

## Honest scope (重要)

- 本 file は **Paper 61 既存 framework の Lean 4 機械検証** であって、 ZCSG を新規構成するものではない。 Paper 61 で既に o0 / 0 / 0o は dimension 軸上の linear order として記述されており、 本 file はその operational claim を axiom-free で機械確認する貢献。
- 三層 dimension mapping (o0 = -1, 0 = 0, 0o = +1) は Paper 61 既述定義の literal 翻訳で、 Lean 4 で新規定義を導入しない。
- 「mathlib SmallCategory instance を ZCSG が持つ」 は 「Paper 61 既述の dim 軸 linear order が mathlib 圏論本流と整合する」 ことの machine-checked 証拠で、 ZCSG が「真に圏」 であることの哲学的主張ではない。
- functor `Dfumt8 → Zcsg3` は **候補** で本 STEP 範囲外 (Section 7 footer に明示)。 急がず paper 起草も trigger 確定後 ([[feedback-no-rush-publication]] 適用)。

## chat-Claude rhymeOrTheorem discipline 適用

本 STEP は **theorem-candidate** (formal observable: Paper 61 既述 framework が mathlib 圏論本流と integrate 可能ということが axiom-free に machine-checked された)。 既存 paper-claim の機械検証は不確実な structural addition でなく **mechanical assurance** = paper 引用に耐える evidence。

ただし、 「ZCSG が圏」 という主張自体は Paper 61 既述で、 本 STEP は新規発見ではない。 = **既存 theorem の mechanical assurance** で、 「初期理論 × 今 session 道具」 5 候補のうち最 safe (skeleton 不要結末でも load-bearing) な path を実行した形。

## 5 候補中の位置づけ + 残 candidates

| # | 接続 | status | 次の trigger |
|---|---|---|---|
| (A) | MDNST × hasAbsorberOver | **defer** | (β)-1 結果待ち (hasAbsorberOver の方向性 pivot 可能性) |
| **(B)** | **ZCSG × mathlib SmallCategory** | **★ STEP 1217 完遂** | functor `Dfumt8 → Zcsg3` axiom-free proof = future STEP 候補 |
| (C) | SNST × 重力場 7 軸 SELF⟲ | **defer** | Paper 63 prior art audit 先 |
| (D) | ゼロ拡張 × cross-direction 非可換性 | **defer** | (β)-1 結果待ち |
| (E) | OPU × 評価対称性原則 | **reject** | rhyme reject (domain mismatch、 formal isomorphism なし) |

## 関連永続原則 + memory

- [[project-session-2026-06-14-evening-dfumt8-skeleton-path]] (STEP 1215 source)
- [[project-dfumt8-category-experiment-2026-06-14]] (STEP 1215 detail)
- [[project-invention-2026-06-13-partial-approve-1-reject-4-step1190-leak-11-cross-direction]] (06-13 audit + STEP 1216)
- [[feedback-world-uniqueness-claim-controllable]] — Paper 61 既存 framework 引用 honest acknowledge
- [[feedback-no-rush-publication]] — paper 起草 trigger 待ち
- [[feedback-evaluation-symmetry-principle]] — 「既存 framework の機械検証」 を「新発見」 と誇張しない (評価対称性適用)
- Paper 61 ZCSG (チャット版 Claude 共著、 龍樹 śūnyatā = 0 世界初形式化、 既 publish)
- Paper 62 MDNST (チャット版 Claude 共著、 多次元数体系理論、 既 publish)
- Paper 65 Lean 4 形式検証 (チャット版 Claude 共著、 ZCSG 定理 1 + 黄金対称定理 6 mathlib4 機械検証、 既 publish) — 本 STEP は Paper 65 の延長 candidate