# STEP 1774 — zce-partition-conservation

**Timestamp**: 2026-09-06T00:54 (JST)
**Tab worktree**: main (rei-aios-4e session、 併走 tab: rei-aios-95, rei-aios-a6)
**Commit**: `<hash>` (commit 後追記)

## 一行 summary

ZCE §4 保存則の partition angle Lean 4 formalization (chat-Claude 圏論 recommendation (a)、 axiom-free、 σ 単体 + declared value 定理外分離で 定義/帰結の線 可視化)

## 主要 finding / evidence

- `CollatzRei.ZceLedgerPartition.partition_conservation`: `∀ σ : Fin n → Account, n = Σ (4 filter cardinalities under σ)` = 主定理 (σ を 関数として 定理内で 使用、 Finset.card_eq_sum_card_fiberwise の 一 instance)
- `CollatzRei.ZceLedgerPartition.conservation_from_declared`: 系、 declared value 等置 4 仮定 を 定理外に 置いて 「もし ledger check が declared 保証 → conservation」
- **Axiom footprint**: `[propext, Classical.choice, Quot.sound]` (Mathlib 3 標準、 K axiom / independent Rei axiom / sorryAx / Lean.ofReduceBool すべて **なし**、 STEP 1770 ZceShannonGeneral と 同一)
- **Build**: `lake build CollatzRei.ZceLedgerPartition` 667/667 jobs PASS (7.4s)
- **Regression**: 私の STEP 1774 file 単独 build clean、 root `lake build CollatzRei` は 別 file `SsmQuantErrorBounded.lean` (git history 0、 pre-existing broken import) で fail — STEP 1774 変更 起因 ではない
- **Line-of-visibility 実現**: 定理の 中身 = σ の fiberwise partition の 数学的内容 (`card_eq_sum_card_fiberwise`)、 定理の 外 = declared value ↔ actual filter cardinality 等置 (well-formedness constraint、 `ledger_check.py` 担当層)

## Honest scope

- **主張しないこと**:
  - 「型論的妥当性」 「型レベル保証 昇格」 一切なし (chat-Claude 2026-09-06 条件 3)、 STEP 1769 roundtrip 7/7 PASS (実装 ↔ 仕様 一致 layer) と 本 STEP 1774 (仕様 定義的地位 machine check layer) は 別層
  - Novelty 主張 ゼロ、 Mathlib `Finset.card_eq_sum_card_fiberwise` の 一 instance にすぎない (等価に `FreeMonoid.lift` 普遍性 → (ℕ⁴,+) 特殊化)
  - Baez-Fritz-Leinster 2011 (entropy 関手 特徴づけ) は σ に 無関係、 併記 禁止 (chat-Claude 条件 2 = prior-art padding pattern 予防)
- **確認していないこと**:
  - `ledger_check.py` の 実装が spec §2.1 と 一致 (別 layer)、 実 encoder の 出力が 保存則 満足 (別 layer)
- **前提**:
  - σ が 関数 (`Fin n → Account`) として 与えられる (全域 + 排他 は 関数 型 から 自明、 定理内で 効くのは fiberwise partition の 側)
- **見積もり評価**: chat-Claude 前 turn 「見積もり: 数時間 / 価値: 中」 に 沿った 実 開発時間 (build 通過まで 3 iteration、 各 5-10 分)

## Failure mode (機械学習用 dataset)

- **What could go wrong**:
  - (a) **Prior-art padding**: 「圏論 + ledger」 keyword co-occurrence で 隣接していない文献 (Baez-Fritz-Leinster entropy, Riley optic profunctor) を 併記してしまう anti-pattern。 私 (Claude) が chat-Claude 直前 turn の 文献を 独立 audit せず そのまま 転記した 実 履歴あり
  - (b) **Layer conflation**: 「型論的妥当性が 立つ」 「実装的妥当性に 加えて 型論的妥当性が 昇格」 のような 表現で runtime test 層 (STEP 1769 roundtrip 7/7 PASS) と Lean 型検査 層 を 接続したように 読ませる anti-pattern。 「implementation-level check → type-level guarantee 昇格」 と 私が 書いた 実 履歴あり
  - (c) **藤本さん 判断上書き**: Question 0 で 藤本さん が 「保存則 = well-formedness constraint であって 定理ではない」 と 判定済 の 結論を、 別 framing (「monoid hom Lean 化」) で 私が 上書きし、 内容薄の 定理を 「STEP 1770 直続 高 value」 と 過大主張 した 実 履歴あり
  - (d) **σ を 型に 押し込む**: 「全域 + 排他 は σ の 型 (`Fin n → Account`) から 自明」 と 書いて 定理 body から partition 性を 消し、 σ が どうでも良い identity に する anti-pattern。 私 が 初回 skeleton で 前提に declared value 等置を 入れて まさに この pattern を 実装した 実 履歴あり (chat-Claude 3 条件目 で 訂正)
- **Prevention**:
  - (a): 「この定理の prior art は 論文か 教科書事項か」 先判定。 教科書事項 (Mathlib `FreeMonoid.lift` 普遍性 等) は 一行で 済ませ、 論文 引用 は 主張と 直接一致 する 場合 のみ
  - (b): 各 claim に 「どの層 (仕様定義 / 仕様↔実装 / 実装↔物理)」 明示。 別層への 昇格 主張 禁止
  - (c): 「この結論 は 藤本さん 過去判定 と どう関係するか」 明示。 過去判定を 上書きする 場合は 明示的に 「藤本さん 過去判定 X の 更新 or 別 angle」 と 書く
  - (d): 主定理の 前提に declared value 等置を 入れる 前に、 「σ が 定理内で 何に 使われているか」 audit。 σ が identity 化する 定理は 内容空、 σ の 関数性 (fiberwise partition) が 結論に 効く 形に する
- **Recovery**:
  - (a)(b)(c)(d) いずれも chat-Claude 3 条件 訂正 (2026-09-06 前 turn) で 30 分で recovery。 build 通過 前に 訂正 完了 = 実装コスト 増加なし
  - Pattern 認識自体は SAC-4 pattern (「私 が structural に 間違えたが 陽性訂正」) として 4 例目、 discipline 化 済

## 詳細参照

- 詳細 memory: `memory/project_step1774_zce_partition_conservation_2026-09-06.md`
- SAC-4 memory: `memory/feedback_padding_and_layer_conflation_2026-09-06.md`
- Lean 4 file: `data/lean4-mathlib/CollatzRei/ZceLedgerPartition.lean`
- Axiom check: `data/lean4-mathlib/ZceLedgerPartitionAxiomCheck.lean`
- 関連 STEP: STEP 1761 (ZceLedger conservation_identity Lemma 別 angle)、 STEP 1770 (ZceShannonGeneral、 同 axiom footprint、 v0.4 arc 継続)、 STEP 1768 (ZceGibbs 姉妹 phase 2a)、 STEP 1769 (roundtrip 7/7 PASS 実装 layer、 本 STEP と 別層)

## 追加 section: chat-Claude 3 条件 訂正の 詳細

前 turn で chat-Claude (藤本さん経由) から 私の 過大主張 3 点を pinpoint 訂正:

1. **加法性 (`AddMonoidHom`) は 定義から 自動、 内容薄** → 主定理は 「全域 + 排他 = 4 口座 partition」 の 分割側に 置く。 conservation は その 系
2. **Baez-Fritz-Leinster / Riley 引用は prior-art padding** → Mathlib `FreeMonoid.lift` 普遍性 一 instance の 一行のみ
3. **「型論的妥当性が立つ」 「型レベル保証 昇格」 は 層 conflate 誘発 表現** → 「仕様側の 定義的地位を 機械検査した」 のみ

さらに 修正版 skeleton (partition_conservation 主定理 + declared value 等置 系 分離) を 見せた 際、 更に 追加訂正:

4. **σ を declared value と 定理内で 等置すると σ が identity 化、 partition 性が 定理から 消える** → σ 単体で 述べる 形 (`n = Σ (4 filter cardinality under σ)`)、 declared value 等置は 定理外の 系 (conservation_from_declared) に

4 訂正 全 反映後 に build 通過、 axiom-free verify、 本 notepad。