# STEP 1796 — zce-shannon-upper-bound (v0.4 phase 2c)

**Timestamp**: 2026-09-06T07:17 (JST)
**Tab worktree**: main (rei-aios-4e session)
**Commit**: `<hash>` (commit 後追記)

## 一行 summary

ZCE v0.4 phase 2c = Cover-Thomas 5.4.1 upper bound (Shannon-Fano `ℓ*(x) := ⌈-log₂ p(x)⌉` の Kraft 満足 + `E[ℓ*] * log 2 ≤ entropyNats + log 2`) Lean 4 axiom-free formalize、 4 declaration 全 `[propext, Classical.choice, Quot.sound]` (Mathlib 3 標準)、 STEP 1770 lower bound と 併せて classical Shannon 1-bit overhead `H_bits(p) ≤ E[ℓ*] ≤ H_bits(p) + 1` 完結

## 主要 finding / evidence

### Lean 4 file: `data/lean4-mathlib/CollatzRei/ZceShannonUpperBound.lean`

**Definitions (1)**:
- `shannonFanoLength p x := ⌈-Real.log (p x) / Real.log 2⌉₊` = Shannon-Fano code length

**Theorems (4)** — 全 axiom-free `[propext, Classical.choice, Quot.sound]`:
1. `shannonFano_pow_le`: `2^(-↑ℓ*(x)) ≤ p x` (per-symbol Kraft bound)
2. `shannonFano_kraft`: `kraftGeneral (shannonFanoLength p)` (Kraft 満足)
3. `shannonFano_ceil_bound`: `↑ℓ*(x) < -log(p x)/log 2 + 1` (per-x ceil upper bound)
4. `shannon_sct_upper_bound`: `E[ℓ*] * log 2 ≤ entropyNats p + log 2` (**主定理**)

### Build 結果

- `lake build CollatzRei.ZceShannonUpperBound` = 2145/2145 jobs PASS (11s、 module 単独)
- `lake build CollatzRei` (root regression check) = **7955/7956 jobs PASS (24s)** = STEP 1783 baseline 7954/7955 + 1 new module (upper bound)、 root build **green 維持**
- Warning は STEP 1783 と 同一 pre-existing のみ (Paper26V3 axiom info / MasonStothersValuation lint / BrownawellMasser sorry)

### Iteration 履歴 (3 回)

- (1) 初 build fail: `Mathlib.Algebra.Order.Floor.Basic` 不在 → `Floor.Semiring` に 修正 (`Nat.le_ceil`, `Nat.ceil_lt_add_one` は Semiring.lean)
- (2) 再 build fail: `unfold_let` tactic unknown + `DecidableEq X` synth fail + `unfold_let y` scope error → `show` に 置換 + `Finset.single_le_sum` に 変更 + Nat.le_ceil 直接適用
- (3) 再 build fail: `Real.logb` unknown constant → `Mathlib.Analysis.SpecialFunctions.Log.Base` import 追加 → PASS

## Honest scope

- **主張しないこと**:
  - **Novelty ゼロ** = Cover-Thomas Ch 5 Theorem 5.4.1 (Wyner-Ziv 1976) の Lean 4 restatement のみ、 ZCE spec §5.1 「novelty 主張禁止」 継承
  - `p(x) = 0` boundary は 現 skeleton の scope 外 (strictly positive p 前提)、 phase 2d/2e defer
  - measure-theoretic bridge (Mathlib `MeasureTheory.Entropy` との bridge) は phase 2d/2e defer
- **前提**:
  - Fintype X + Nonempty X (STEP 1770 lower bound と 同一)
  - `hp_pos : ∀ x, 0 < p x` (strictly positive)
  - `hp_sum : ∑ x, p x = 1` (probability distribution)
- **確認していないこと**: 単一 Real formalize (Mathlib `Real` 実装依存) の 実 実装 の 完全 axiom footprint — Mathlib 3 標準 axiom trust に 依拠 (v0.4 arc 全体 同型)

## Combined STEP 1770 + STEP 1796 = classical Shannon SCT 完結

STEP 1770 (v0.4 phase 2b) + 本 STEP 1796 (v0.4 phase 2c) の 組合せで:
- Lower bound (STEP 1770): `entropyNats p ≤ expectedLength p ℓ * Real.log 2` for **any** Kraft-satisfying ℓ
- Upper bound (本 STEP): `expectedLength p (shannonFanoLength p) * Real.log 2 ≤ entropyNats p + Real.log 2` for Shannon-Fano ℓ*

**Combined classical result** (Cover-Thomas 5.4.1 完全形):
```
entropyNats p ≤ expectedLength p (shannonFanoLength p) * Real.log 2 ≤ entropyNats p + Real.log 2
```
= `H_nats(p) ≤ E[ℓ*] * log 2 ≤ H_nats(p) + log 2`
= (割算 log 2 > 0) `H_bits(p) ≤ E[ℓ*] ≤ H_bits(p) + 1`
= **classical Shannon 1-bit overhead result**

両 bound axiom-free = Lean 4 machine-verified assurance が classical Shannon 圧縮限界に 提供された。

## Failure mode (未来 Claude dataset)

- **What could go wrong**:
  - (a) **Mathlib import path drift**: v4.27.0 では `Log.Base`、 別 version では 別 path の 可能性、 grep 前 に `import` 迷い で time waste
  - (b) **`unfold_let` tactic 誤用**: `set ... with hy` の hy 使用 pattern と 混同、 `show` に 置換で recovery
  - (c) **`DecidableEq` typeclass 隠れ要求**: `Finset.univ.erase` 使用時 に synth fail、 `Finset.single_le_sum` 等の DecidableEq 不要 API で 回避
  - (d) **Nat.ceil vs Int.ceil 混同**: `⌈⌉₊` (Nat) vs `⌈⌉` (Int)、 前者は 負の入力で 0、 後者は well-defined、 Shannon-Fano context では 前者 (p x ≤ 1 ⇒ -log p x ≥ 0 なので 差異なし が、 hypothesis 記述 が 変わる)
- **Prevention**:
  - (a): 一次資料 grep audit 先行 (`grep -rn "def X\|theorem X"` on Mathlib) 、 build 失敗 前に import path 確認
  - (b): `set ... with hy` で 名前 導入した ら `hy` を rewrite 用 hypothesis として 使う (`unfold_let` は Lean 4 v4.x で 未提供 or 別名) → `show`/`change` で 直接 型書き換え
  - (c): `Finset` API で `[DecidableEq]` 要求 有無 を signature で 確認、 typeclass-lite alternative を 優先
  - (d): 導入時に `⌈⌉₊` (Nat) 明示、 hypothesis `0 ≤ y` を 早期証明で 用意
- **Recovery**:
  - 各 iteration は 数分 で resolve、 累計 3 iteration = 30 分以内 の 標準 debug loop、 Lean 4 build 慣習 通り

## 詳細参照

- 詳細 memory: `memory/project_step1796_zce_shannon_upper_bound_2026-09-06.md`
- 直前 STEP: STEP 1770 (`ZceShannonGeneral.lean` lower bound、 本 STEP の complement)
- 起点 memory (ZCE arc close 記録): `hooks/2026-09-05*_step1755_1768_zce_v04_arc_close_2026-09-04.md` (phase 2c candidate として 記録済)
- 関連 STEP: STEP 1768 (Gibbs phase 2a)、 STEP 1770 (Shannon SCT general phase 2b、 本 STEP の 姉妹)、 STEP 1762 (Shannon binary uniform phase 1)、 STEP 1761 (ZceLedger conservation)、 STEP 1774 (partition-conservation、 本日 4e 3 arc)、 STEP 1777/1783 (SsmQuant audit + fix、 本日 4e 3 arc)

## 追加 section: 4e 本日 arc 累計 (2026-09-06、 更新)

本 STEP 1796 で 4e session の 本日 **4 arc** 完結:
- STEP 1774 (commit `0407605d3`): ZCE partition_conservation Lean 4 (chat-Claude 圏論 (a) 実装、 axiom-free)
- STEP 1777 (commit `cbd563d24`): SsmQuant root fail audit (3 週間 silent + 7 因子 構造分析)
- STEP 1783 (commit `cec836b90`): SsmQuant import 削除 修復 (root build green 化)
- STEP 1796 (本 STEP): ZCE Shannon SCT upper bound (Cover-Thomas 5.4.1 完結、 axiom-free)

4 arc 通じて chat-Claude 4 訂正 + 藤本さん 5+ 訂正 全反映、 SAC-4 pattern 5 種 累積 dataset 化。 藤本さん `AskUserQuestion` 経由で directive 明確化 pattern (STEP 1783 + 1796)。 4e 一区切り、 次 arc は 藤本さん directive 待機。