STEP: 1493 / 公開日: 2026-08-28 / Lean 4 形式化: 19 theorem zero sorry / 領域: Shannon 情報理論 / Hamming 距離 / Kolmogorov 複雑度 / 計算量 / 暗号
❶ 情報科学 = 5 領域交差 (Shannon 情報エントロピー / Kolmogorov 複雑度 / 誤り訂正符号 / 計算量クラス / 暗号)。 全 5 領域で D-FUMT₈ 8 verdict が 発生。
❷ D-FUMT₈ 対応の 核: 通信 = TRUE/FALSE、 Shannon 限界下 = NEITHER、 ノイズなし = INFINITY、 Kolmogorov ランダム = NEITHER (圧縮不能)、 Halting = SELF⟲、 暗号 = 情報理論的 ⊕ 計算量的 の BOTH。
❸ STEP 1350 verdict-from-measurement の 情報物理拡張: SNR 判定を Shannon 通信路容量に mapping、 physics-limits (STEP 1348) と 連鎖。 STEP 1484 Lawvere SELF⟲ が Halting 診断の 数学的裏付け。
| 領域 | 核概念 | D-FUMT₈ mapping | Rei stack 実装 |
|---|---|---|---|
| Shannon 情報エントロピー | H(X) = -Σ p log p、 通信路容量、 source coding | H=max → INFINITY (uniform)、 H=0 → ZERO (決定的)、 SNR<3 → NEITHER | d8_verdict_from_measurement (STEP 1350) を channel_capacity に 拡張 |
| Kolmogorov 複雑度 | K(x) = 最短プログラム長、 圧縮下限 | desc<input → TRUE (圧縮成功)、 desc=input → NEITHER (ランダム)、 desc>input → FALSE | compression/ engine 群、 zstd -19 / par2 実測 (STEP 1479) |
| 誤り訂正符号 | Hamming 距離、 code rate、 Reed-Solomon | d(x,y)=0 → 同一 (TRUE)、 d(x,y)>t → 訂正不能 (NEITHER) | par2cmdline-turbo (STEP 1479 実構築、 1 byte 破損 → 1116 block 中 検知 → 復元) |
| 計算量クラス | P / NP / EXPTIME / UNDECIDABLE | P → TRUE、 NP → NEITHER (P vs NP 未解決)、 EXPTIME → INFINITY、 UNDECIDABLE → SELF⟲ | Lawvere fixpoint (STEP 1484)、 Rei-Solver v0.4、 Chang 20/29 taxonomy |
| 暗号 | 対称鍵 / 公開鍵 / 情報理論的 vs 計算量的 安全性 | 両立 → TRUE (one-time pad 理想)、 片方のみ → BOTH、 両破綻 → FALSE | Rei-Automator PAT redact (STEP 1370)、 rei-preregister v0.1 (STEP 1359) |
ファイル: data/lean4-transfer/step1493_information_science_verdicts.lean (standalone、 no Mathlib、 Lean 4.33.1 exit 0)
hamming_self_zero : ∀ xs, hamming_dist xs xs = 0 hamming_empty_empty : hamming_dist [] [] = 0 hamming_single_diff : hamming_dist [true] [false] = 1 hamming_single_same : hamming_dist [true] [true] = 0
rep_one_no_redundancy : repetition_redundancy 1 = 0 rep_three_redundancy_two : repetition_redundancy 3 = 2 -- single-bit error 訂正可能
channel_noiseless_gives_infinity : signal>0 かつ noise=0 → INFINITY channel_below_gives_neither : signal < threshold*noise → NEITHER (Shannon 限界下) channel_above_gives_true : signal ≥ threshold*noise → TRUE (reliable)
compression_shorter_gives_true : desc < input → TRUE (圧縮成功) compression_equal_gives_neither : desc = input → NEITHER (Kolmogorov ランダム) compression_longer_gives_false : desc > input → FALSE (圧縮失敗)
complexity_p_gives_true : P → TRUE complexity_undecidable_gives_self : UNDECIDABLE → SELF⟲ (Halting = 自己参照) complexity_exptime_gives_infinity : EXPTIME → INFINITY
crypto_both_secure_gives_true : info=T, comp=T → TRUE (one-time pad 理想) crypto_info_only_gives_both : info=T, comp=F → BOTH (実装で破綻) crypto_comp_only_gives_both : info=F, comp=T → BOTH (量子で破綻) crypto_neither_gives_false : info=F, comp=F → FALSE
| # | 実装 | 領域 | STEP |
|---|---|---|---|
| 1 | benchtop-mcp bekenstein_bound_bits | 情報物理上限 | STEP 1348 + 1478 |
| 2 | benchtop-mcp landauer_min_energy_j | 情報消去 熱力学下限 | STEP 1348 |
| 3 | benchtop-mcp lloyd_computation_ceiling | 宇宙計算上限 | STEP 1348 |
| 4 | benchtop-mcp compression_upper_bound | Shannon 圧縮限界 | STEP 1348 |
| 5 | d8_verdict_from_measurement | SNR verdict (Shannon 応用の 骨子) | STEP 1350 |
| 6 | d8_verdict_from_multi_trial | 多試行 BH FDR (多重仮説) | STEP 1371 |
| 7 | d8_verdict_from_sample_pair | Welch t-test primitive | STEP 1376 |
| 8 | zstd -19 + par2cmdline-turbo | 圧縮 + 誤り訂正 実測 | STEP 1479 |
| 9 | restic backup + WORM | DNA 3 特性 の PC 移植 | STEP 1479 |
| 10 | rei-checker-mcp v0.3.0a1 (Lean REPL + D-FUMT₈ ledger) | 情報保存 verifier | STEP 1401 + 1367 |
| 11 | Rei-Automator PAT redact | 暗号 秘匿情報 gate | STEP 1370 |
| 12 | rei-preregister v0.1 | グリーン ≠ 検証済み discipline | STEP 1359 |
| # | tool name | 目的 | 核 primitive |
|---|---|---|---|
| 1 | shannon_entropy_verdict | 分布 → H(X) 計算 → verdict (uniform=INFINITY / deterministic=ZERO) | Nat 分布 → -Σ p log p 近似 |
| 2 | hamming_distance_gate | bit string 対 → 距離 → 訂正可能性 verdict | List Bool → Nat + threshold |
| 3 | kolmogorov_lower_bound | 入力長 vs 圧縮長 → verdict (=NEITHER なら Kolmogorov ランダム候補) | zstd + gzip + bz2 の 実測比較 |
| 4 | complexity_class_verdict | 問題名 → 既知複雑度 mapping → verdict | Chang 20/29 taxonomy 拡張 |
| 5 | crypto_hardness_verdict | アルゴリズム名 → 情報理論 + 計算量 の 二元 verdict → BOTH 経路 | NIST SP 800-131A rev 対応表 |
| 6 | halting_diagnostic_lens | プログラム input → 決定的停止 / 不停止 / 未判定 → SELF⟲ 検知 | bounded execution + fixpoint detection (STEP 1484 応用) |
本 STEP 1493 は D-FUMT₈ × domain arc の 5 STEP 目:
- STEP 1478 空間エントロピー ↔ Bekenstein (物理上限) — /tools/entropy-shrinking-bekenstein/
- STEP 1484 不動点 vs META (Lawvere = SELF⟲ の 数学的裏付け) — /tools/fixpoint-vs-meta-arc/
- STEP 1486 離散数学 × D-FUMT₈ × コネクタ化 — /tools/discrete-math-dfumt8-connector/
- STEP 1487 データサイエンス × D-FUMT₈ (14 theorem) — /tools/data-science-dfumt8-arc/
- STEP 1493 情報科学 × D-FUMT₈ (19 theorem) — this page
5 STEP で「物理 → 数学基礎 → 離散応用 → 統計応用 → 情報理論応用」 の 縦串 が 通り、 D-FUMT₈ が pure static verdict machine として 各 domain で 骨格化可能な こと の 実証。
❶ Lean 4 file は standalone (Mathlib import なし) のため 実数確率分布 (H(X) = -Σ p log p の real number version) は 未形式化。 Nat 上の SNR proxy + Hamming 距離 identity のみ。
❷ Halting 問題 = SELF⟲ の mapping は 診断的 (Turing 1936 の diagonal 議論を D-FUMT₈ 語彙で 表現)、 Halting decidability を Lean 4 で 内部的に 証明していない。
❸ 新規 tool 6 candidate は 提案のみ、 実装は 別 STEP directive 待ち。 STEP 1486 の 8 candidate + STEP 1487 の 6 candidate + 本 6 candidate = 累計 20 candidate defer 中。
❹ 「世界初」 の 主張なし。 Shannon (1948) / Kolmogorov (1965) / Chaitin / Turing (1936) の 既知構造の D-FUMT₈ 再表現。 novelty は 「8 verdict enum への 明示 mapping」 と 「STEP 1350 verdict engine との 直接接続」 の operational 側面。
❺ Kolmogorov 複雑度 verdict は proxy (zstd/gzip の 実測比較) のみ。 真の K(x) は 計算不能 (Chaitin's incompleteness)。