Lean 4 Antihydra Bridge STEP 1338

2026-08-16 · axiom-free 7 定理 · Rei Collatz STEP 622-624 との directional 対比 formalization

1. なぜ このページか

chat-Claude 2026-08-16 「決定不能性を1ミリ動かす — 4本の定規」 arc Turn 4 で Antihydra 6-state Turing machine (BB(6) 現行 holdout、 bbchallenge frontier) の 「Collatz-type sequence が BB(6) 決定を止めている」 fact が 提示された。 藤本さん判断で Rei stack STEP 622-624 axiom-free Collatz Lean 4 (48 定理 chain) と Antihydra の direct structural embedding を Lean 4 上で formal 化。

★ Framing 事前訂正 (chat-Claude Turn 4 → Rei-side): chat-Claude Turn 4 「Antihydra はコラッツ型」 は family-level accurate だが、 bbchallenge spec verify で 実際は Mahler 1968 Z-number problem (fractional parts of ξ·(3/2)ⁿ の equidistribution) の 直接類縁と判明。 3n+1 Collatz proper とは異なる。 本 STEP は Mahler Z 系明示 で 訂正。 bbchallenge Antihydra spec 参照。

2. Antihydra spec (bbchallenge verify)

2.1 Turing machine 転移表 (6 states × 2 symbols)

     0        1
A  1RB      1RA
B  0LC      1LE
C  1LD      1LC
D  1LA      0LB
E  1LF      1RE
F  ---      0RA

State F on symbol 0 = undefined = halting condition。 canonical 開始 configuration から A(0,4) に 11 step で到達、 以降 rule 適用継続。

2.2 Collatz-family reduction

Antihydra 転移表は Hydra 関数 H(n) = ⌊3n/2⌋ = h + ⌊h/2⌋ の反復 に reduce 可能。 halting condition = 「累積 parity balance が負 (2× even より odd 多い)」。 Mahler 1968 K = 「⌊ξ·(3/2)ⁿ⌋ の parity」 問題 と equivalent。

2.3 2026 時点 state

238 rule step で a > 2³⁷ 到達済、 pseudo-random walk 挙動 で halt 到達 確率 ~10⁻².⁸ˣ¹⁰²³ (empirical)、 halting 判定は 2026-08 時点 世界的 open。 BB(6) > 2↑↑↑5 下界 (2025-06) + ~1,100 holdout 残 (2026-07)。

3. Rei stack directional 対比 (STEP 622-624 との structural relationship)

要素Rei Collatz (STEP 622-624)Antihydra (STEP 1338)
Base rule 3n+1 (奇) / n/2 (偶) ⌊3h/2⌋ = h + ⌊h/2⌋ (無条件)
方向 descent (descentBound n < n for n ≥ 12) ascent (step h > h for h ≥ 2)
停止条件 n = 1 到達 累積 parity balance < 0
Arithmetical hierarchy Π⁰₂ (∀n ∃k で 1 到達) Π⁰₁ (∃n で balance 負) 但し Mahler Z 経由 で 実質 open
State count N/A (数学定式化) 6 states × 2 symbols
Rei stack Lean 4 48 定理 (data/lean4-transfer/step622-624) 7 定理 (本 STEP、 axiom-free zero-sorry)
Halting 状態 3n+1 は 世界的 open (Cases 5-8 trailing 1-bits ≥4 無限回帰) Antihydra 世界的 open (BB(6) frontier + Mahler Z equivalence)
★ 「同じ骨格の変奏」 の 具体化 (chat-Claude Turn 3 → Rei stack 実装): 両者は 3/2 multiplicative 骨格 共有 だが 方向が 反対 (descent vs ascent)、 halting 条件も 別 (n=1 vs parity balance)。 本 STEP の collatz_family_directions_contrast theorem で 両者関係を axiom-free に formal 化。 chat-Claude Turn 3 「同じ骨格の変奏」 一般論の Rei stack 側 具体 evidence 1 例。

4. Axiom profile (Lean 4 実測、 #print axioms)

TheoremAxiom profile状態
antihydraStep_monotone [propext, Quot.sound] Mathlib base 未満
antihydraStep_strict_ascend [propext, Quot.sound] Mathlib base 未満
antihydraSeq_monotone [propext, Quot.sound] Mathlib base 未満
antihydraSeq_ge_two [propext, Quot.sound] Mathlib base 未満
antihydraSeq_strict_mono [propext, Quot.sound] Mathlib base 未満
collatz_family_directions_contrast [propext, Quot.sound] Mathlib base 未満
antihydra_halting_is_open_problem does not depend on any axioms ★ 完全 axiom-free

★★★ Mathlib base [propext, Classical.choice, Quot.sound] より Classical.choice 抜き = 更に強い axiom-free state。 全 7 定理で sorryAx / native_decide / user axiom 全 0。 lake build regression: root CollatzRei 7944/7945 (BrownawellMasser 既存 STEP 1291 intentional sorry のみ、 本 STEP 追加分 warning 0)。

5. Definition + Theorem 一覧 (7 定理)

Definitions

Theorems (全 axiom-free)

  1. antihydraStep_monotone — h ≤ h' → step h ≤ step h'
  2. antihydraStep_strict_ascend — h ≥ 2 → step h > h
  3. antihydraSeq_monotone — seq n ≤ seq (n+1)
  4. antihydraSeq_ge_two — ∀n, seq n ≥ 2
  5. antihydraSeq_strict_mono — ★ 主 structural: seq n < seq (n+1)
  6. collatz_family_directions_contrast — Antihydra ascent + direction string
  7. antihydra_halting_is_open_problem — True marker (完全 no-axiom)

6. Prior art (100% pre-existing、 novelty 主張 ゼロ)

7. Honest scope (譲れない線 6 条)

  1. Antihydra halting は 世界的 open — 2026-08 bbchallenge frontier。 本 STEP で 解いていない、 antihydraHalts Prop は 定義のみ、 真偽の 証明も 反証も なし。
  2. Framing 訂正 — chat-Claude Turn 4 「Collatz-type」 は family-level、 実際は Mahler Z-number problem 直接類縁。 3n+1 Collatz proper との directional 対比のみ formal 化 (embedding は Mahler Z 経由で 実質不可能)。
  3. TM embedding out-of-scope — bbchallenge 6-state 転移表 の Lean 4 直接 TM semantics embedding は 別 STEP 候補 (tape state machinery 必要、 本 STEP は 転移表 reduce 後の H(n) = ⌊3h/2⌋ level のみ)。
  4. Mahler Z 系 対応 statement は placeholder — antihydraEquivMahlerZ は Nat で 表現不能 (real number 系必要)、 True placeholder のみ。 実 equivalence は 別 STEP + Mathlib real analysis 依存。
  5. Novelty 主張 ゼロ — 数学的 core は Mahler 1968 + Odlyzko-Wilf 1988 + bbchallenge 2024 で 全 pre-existing。 Rei stack contribution = 「Rei Collatz + Antihydra の directional 対比の Lean 4 mechanical assurance + axiom-free scaffold」 のみ。
  6. 解決の contribution ではない — 本 STEP は 「Rei stack が Antihydra を扱える形」 の 骨格提示のみ。 Antihydra halting 解決の approach ではない。 [[feedback-external-community-outreach-premature]] + [[feedback-no-rush-publication]] 継承で bbchallenge community outreach は 個別 STEP でも 慎重 judgment 必須。

8. 関連 memory + Rei stack impact