ZCE v0.4 phase 2c 完結 — partition + Shannon SCT STEP 1774 STEP 1796

1. なぜ このページか

2026-08-30 日経記事 「関係性読み解く数学『圏論』、量子論でも」 (中平健治 玉川大 教授) を 起点に、 藤本さん と chat-Claude の 対話で 圏論的 ZCE 補強 recommendation 3 点 が 提示された。 その うち recommendation (a) = 「台帳が monoid 準同型 (partition well-defined)」 を Lean 4 で formal 化した の が STEP 1774。 続いて STEP 1770 (v0.4 phase 2b Shannon SCT general lower bound via Gibbs) の complement として STEP 1796 = Cover-Thomas 5.4.1 upper bound (Shannon-Fano code) を formal 化。

2. STEP 1774 — ZCE §4 partition-conservation

2.1 起点と 3 訂正 (chat-Claude 2026-09-06)

私 (Rei-side Claude) が 初期に 提示した skeleton は 以下 3 点で 過大主張だった:

• 「monoid hom (AddMonoidHom) は STEP 1770 直続 高 value」 → chat-Claude 「加法性は 定義から自動、 内容薄」 訂正
• Baez-Fritz-Leinster 2011 (entropy 関手) 併記 → chat-Claude 「隣接していない文献の prior-art padding」 訂正
• 「型論的妥当性が立つ」 「型レベル保証 昇格」 → chat-Claude 「STEP 1769 roundtrip 7/7 PASS 実装層 と conflate 誘発」 訂正

更に 修正 skeleton 提示後 に 追加訂正:

• σ を 定理内で declared value と 等置すると σ が identity 化、 partition 性 が 定理から 消える → σ 単体で 述べる 形、 declared value 等置 は 定理外 の 系 (`conservation_from_declared`) に

2.2 主定理 (`partition_conservation`)

theorem partition_conservation {n : Nat} (σ : Fin n → Account) :
    n = (univ.filter (fun i : Fin n => σ i = .ctx)).card
      + (univ.filter (fun i : Fin n => σ i = .cmp)).card
      + (univ.filter (fun i : Fin n => σ i = .cls)).card
      + (univ.filter (fun i : Fin n => σ i = .ch )).card

Line-of-visibility (Question 0 判定 の Lean 上 可視化):

• 定理の 中身 = σ の fiberwise partition の 数学的内容 (`Finset.card_eq_sum_card_fiberwise` 一 instance)
• 定理の 外 = declared value ↔ actual filter cardinality 等置 (well-formedness constraint、 `ledger_check.py` 担当層)

2.3 系 (`conservation_from_declared`)

theorem conservation_from_declared
    {n : Nat} (σ : Fin n → Account)
    (ctx cmp cls ch : Nat)
    (h_ctx : ... = ctx) (h_cmp : ... = cmp)
    (h_cls : ... = cls) (h_ch  : ... = ch) :
    n = ctx + cmp + cls + ch

4 hypotheses は well-formedness constraint = 定理外 の 仮定として 分離。

3. STEP 1796 — ZCE v0.4 phase 2c Shannon SCT upper bound

3.1 起点

STEP 1755-1768 ZCE v0.4 arc close 時 に 「phase 2c candidate = upper bound (Shannon-Fano) + p(x)=0 boundary + measure-theoretic bridge」 と 記録済み。 藤本さん 2026-09-06 「続きを お願いできますか」 → AskUserQuestion 4 択 で 「ZCE v0.4 phase 2c (Shannon SCT upper bound)」 選択 → 実装。

3.2 Definition: Shannon-Fano code length

3.3 主定理 (`shannon_sct_upper_bound`)

theorem shannon_sct_upper_bound
    {X : Type*} [Fintype X]
    (p : X → ℝ) (hp_pos : ∀ x, 0 < p x) (hp_sum : ∑ x, p x = 1) :
    expectedLength p (shannonFanoLength p) * Real.log 2
      ≤ entropyNats p + Real.log 2

Equivalently (divide by log 2 > 0): E[ℓ*] ≤ H_bits(p) + 1。

3.4 支持 lemmas (4 declaration 全 axiom-free)

3.5 Proof strategy

1. Per-x: `Nat.le_ceil` (lower) + `Nat.ceil_lt_add_one` (upper) から ↑ℓ*(x) ∈ [-log(p x)/log 2, -log(p x)/log 2 + 1)
2. Kraft: exponentiate `↑ℓ*(x) ≥ -log(p x)/log 2` → 2^(-↑ℓ*(x)) ≤ 2^(log(p x)/log 2) = p x (via `Real.rpow_logb`)、 sum ≤ 1
3. Upper bound: multiply `↑ℓ*(x) < y + 1` by `p x * log 2 > 0`、 sum: E[ℓ*] * log 2 ≤ ∑ p(-log p) + log 2 = entropyNats + log 2 (hp_sum で log 2 factor 集約)

4. Axiom footprint (全 6 declaration)

全 6 declaration が Mathlib 3 標準 axiom footprint。 K axiom / independent Rei axiom / sorryAx / Lean.ofReduceBool すべて なし。 STEP 1770 phase 2b (Shannon SCT general lower bound) と 同一 footprint、 v0.4 arc 一貫性維持。

5. Build 結果

6. Honest scope

7. 参照

• GitHub Lean 4 source (STEP 1774): CollatzRei/ZceLedgerPartition.lean
• GitHub Lean 4 source (STEP 1796): CollatzRei/ZceShannonUpperBound.lean
• Axiom check (STEP 1774): ZceLedgerPartitionAxiomCheck.lean
• Axiom check (STEP 1796): ZceShannonUpperBoundAxiomCheck.lean
• 関連 STEP: STEP 1761 (ZceLedger conservation_identity Lemma)、 STEP 1768 (Gibbs phase 2a)、 STEP 1770 (Shannon SCT general lower bound phase 2b)、 STEP 1769 (roundtrip 7/7 PASS 実装層)
• Notepad (STEP 1774): STEP 1774 notepad
• Notepad (STEP 1796): STEP 1796 notepad

Commit hashes

• STEP 1774: 0407605d3
• STEP 1796: bae656672