Lean 4 プローブ下界 axiom-free formalization

Rei-AIOS STEP 1282 · chat-Claude 八値対話 arc C option 実装 · 2026-08-06
12 theorem 全完全 zero-axiom lake build 7941/7941 success novelty ゼロ (Shannon 1948 wrapper)

実装内容

File: data/lean4-mathlib/CollatzRei/ProbeLowerBound.lean (root import + AxiomCheck 付き)

定義: sufficientProbes n k := n^k ≥ n.factorial — k プローブで n 値写像 (n! 個の permutation) を identify するのに十分な条件。

証明方法: 全 theorem が by unfold sufficientProbes; decide の Nat decidable computation 型。「decide」 tactic は Lean 4 kernel 経由 evaluation、 native_decide 系規律違反なし。

12 theorem 全完全 zero-axiom (axiom profile)

'Rei.ProbeLowerBound.sufficient_1_for_2'      does not depend on any axioms
'Rei.ProbeLowerBound.not_sufficient_0_for_2'  does not depend on any axioms
'Rei.ProbeLowerBound.not_sufficient_2_for_4'  does not depend on any axioms
'Rei.ProbeLowerBound.sufficient_3_for_4'      does not depend on any axioms
'Rei.ProbeLowerBound.sufficient_6_for_8'      does not depend on any axioms  ★★★
'Rei.ProbeLowerBound.not_sufficient_5_for_8'  does not depend on any axioms  ★★★
'Rei.ProbeLowerBound.sufficient_2_for_3'      does not depend on any axioms
'Rei.ProbeLowerBound.not_sufficient_1_for_3'  does not depend on any axioms
'Rei.ProbeLowerBound.sufficient_3_for_5'      does not depend on any axioms
'Rei.ProbeLowerBound.not_sufficient_2_for_5'  does not depend on any axioms
'Rei.ProbeLowerBound.sufficient_7_for_10'     does not depend on any axioms
'Rei.ProbeLowerBound.not_sufficient_6_for_10' does not depend on any axioms

Mathlib base [propext, Classical.choice, Quot.sound] すら不要 = 最強 axiom-free state。 Nat decidable computation で decide 完結。

Concrete n × k boundary (機械 verify 済)

n	n!	下界 k	n^k	Rei theorem
2	2	1	2	`sufficient_1_for_2`
3	6	2	9	`sufficient_2_for_3`
4	24	3	64	`sufficient_3_for_4`
5	120	3	125	`sufficient_3_for_5`
8	40320	6	262144	`sufficient_6_for_8` ★
10	3628800	7	10000000	`sufficient_7_for_10`

chat-Claude 原文 (2026-08-06 turn 14)

「プローブ数は n に線形。 log₂(n!)/log₂(n) をスターリングで展開すると、 n が大きいほど n に漸近します。語彙を倍にすると握手も倍。対数ではない。これは小さいですが確定計算です。」

Rei 実装の関係: 上記 empirical 計算のうち n=8 で 6 probe 下界 を axiom-free machine-check として確定。一般 Stirling n→∞ 漸近 (実解析 heavy proof) は scope 外。

Prior art (100% pre-existing、 Rei は Lean 4 wrapper のみ)

Shannon, C. E. (1948) "A Mathematical Theory of Communication", Bell System Technical Journal 27 — 情報エントロピー H = -Σ p log p、情報チャネル容量
Kraft, L. G. (1949) MIT SM thesis — Kraft inequality: prefix-free coding の存在条件
Stirling, J. (1730) Methodus Differentialis — n! ≈ √(2πn)(n/e)^n による log(n!) ≈ n log n の漸近

Honest scope (譲れない線):

本 file が 形式化しない:

Shannon 1948 情報エントロピー定理の一般形式化 (mathlib 依存 heavy)
Kraft inequality の一般証明 (専門 Mathlib module 要)
Stirling n→∞ 漸近 (実解析 heavy)
「プローブ ≥ 下界は必要条件」の逆向き (情報論的下界の proof は複雑)

Rei-side novelty: ゼロ。本 file は 78 年前既知 (Shannon 1948) の情報論下界を具体 n について Lean 4 で machine-checked 確認したのみ。 chat-Claude 2026-08-06 turn 14 の empirical 計算 (n=8 で 6 probe) の formalization wrapper。

chat-Claude 2026-08-06 arc 全体 stance

本 STEP 1282 は藤本さん判断「A+B+C 順次実行」の C option 完遂。前 arc の全 novelty 撤回 (Geanakoplos-Polemarchakis 1982 + 書き換え系 + 対話ゲーム = 全既知) を継承し、本 file も「78 年前既知の再形式化」として honest scope 明示。これで A + B + C 完了、 8 値対話 arc 全体を藤本さん 2026-08-06 「全研究 site 反映 default」 protocol 下で完全 site 化達成。