---
name: project-step1338-antihydra-bridge-2026-08-16
description: "STEP 1338 = Antihydra 6-state BB(6) frontier holdout の Rei Collatz (STEP 622-624) directional 対比 Lean 4 axiom-free 7 定理 (6 [propext, Quot.sound] + 1 no-axiom = Mathlib base より 強い)、 Mahler Z-number 系明示 で chat-Claude Turn 4 「Collatz-type」 framing 事前訂正、 chat-Claude 2026-08-16 4 turn arc trigger の 派生 STEP"
metadata: 
  node_type: memory
  type: project
  originSessionId: a9cbca08-7e38-4614-8e10-5fb8dd19bef4
  modified: 2026-08-15T16:05:06.403Z
---

# STEP 1338 Antihydra Bridge (2026-08-16)

## Trigger

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 提示 → 藤本さん 3 pending decision 中 第 1
選択 (「Antihydra 6-state ↔ Rei Collatz 48 定理 direct embedding STEP 化」) で 派生実行。

## 実装

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

**Definitions (9 個)**:
- `antihydraStep (h : Nat) : Nat := h + h / 2` = ⌊3h/2⌋
- `antihydraInit : Nat := 8` (bbchallenge canonical starting)
- `antihydraSeq : Nat → Nat` (iterated)
- `antihydraParityDelta (h : Nat) : Int` (+2 偶 / -1 奇)
- `antihydraParityBalance : Nat → Int` (累積 sum)
- `antihydraHalts : Prop` (halting predicate、 **真偽未証明**、 世界的 open のまま)
- `collatzFamilyDirection : Bool → String`
- `antihydraEquivMahlerZ : Prop` (placeholder for Mahler Z equivalence)
- `reiContributionScope : String` (explicit scope declaration)

**Theorems 7 個 (全 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)

### Axiom profile 実測 (`#print axioms`)

★★★ **6 定理: `[propext, Quot.sound]`** = Mathlib base `[propext, Classical.choice, Quot.sound]`
より Classical.choice 抜き = **更に強い axiom-free state**。

★★★ **1 定理: does not depend on any axioms** = **完全 no-axiom** (最強)。

全 7 定理で sorryAx / native_decide / user axiom 全 0。

### Build 結果

- 単独 build: `CollatzRei.AntihydraBridge` 1.4s success (2 jobs)
- 全 root build: `lake build CollatzRei` 7944/7945 (BrownawellMasser 既存 STEP 1291
  intentional sorry のみ、 本 STEP 追加分 warning 0)、 135s

## ★★★ Framing 事前訂正 (chat-Claude Turn 4 → Rei-side)

**chat-Claude Turn 4**: 「Antihydra はコラッツ型」 と表現。

**bbchallenge spec verify 結果** (WebFetch https://wiki.bbchallenge.org/wiki/Antihydra):
- Hydra 関数 `H(n) = ⌊3n/2⌋` の反復
- 停止条件 = 累積 parity balance が 負 (2× even より odd 多い)
- ★ **Mahler 1968 Z-number problem** (fractional parts of ξ·(3/2)ⁿ の equidistribution)
  の 直接類縁と判明
- 3n+1 Collatz proper とは **異なる**

**Rei-side 訂正**: 「Collatz-type」 は family-level accurate だが、 本 STEP では
**Mahler Z-number 系明示**、 3n+1 Collatz proper との directional 対比のみ formal 化。

[[feedback-one-reproduction-over-ten-unverified]] 「1 件でも説明できない差があれば 計器は
未検証」 「主張前に事実固定」 discipline 継承 = 実装前 bbchallenge 実測 verify で framing
先訂正 → corrigendum 発生防止 (STEP 1290 Mason-Stothers arc 同型 pattern)。

## Rei stack directional contrast (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 到達) | Π⁰₁ 但し Mahler Z 経由で 実質 open |
| State count | N/A (数学定式化) | 6 states × 2 symbols |
| Rei stack Lean 4 | 48 定理 | 7 定理 (全 axiom-free) |
| Halting 状態 | 3n+1 世界的 open | Antihydra 世界的 open (BB(6) frontier + Mahler Z) |

**★ 「同じ骨格の変奏」 の 具体化** (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 例**。

## 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 必須。

## Prior art (100% pre-existing)

- Mahler K. (1968) "An unsolved problem on the powers of 3/2", J. Austral. Math. Soc.
- Odlyzko A.M., Wilf H.S. (1988) "Functional iteration and the Josephus problem", Glasgow Math. J. 30
- Aaronson S. (2020) "The Busy Beaver Frontier"
- bbchallenge community (2024) — Antihydra 命名 + 6-state 転移表 spec
- BB(5) = 47,176,870 Coq 機械検証 (bbchallenge 2024-07)
- BB(6) > 2↑↑↑5 下界 (2025-06)

## Site 反映

- `public/tools/lean4-antihydra-bridge/index.html` (~11 KB、 8 section)
- dist-renderer mirror force-track md5 一致 (`24bef7b0ae6855bede00487e88ca77ff`)
- 2026-08-06 「全研究 site 反映 default」 protocol 継承

## 関連

- [[project-session-2026-08-16-chat-claude-lambda-arc-close]] (本 arc index、 4 turn + 3
  派生 = STEP 1338 + 2 artifact archival + RECENT_UPDATES)
- [[project-stash-22-close-arc-2026-08-15]] (前日 arc、 memory retroactive save pattern
  継承)
- [[feedback-chat-claude-21-turn-debate-2026-08-08]] (前 21 turn precedent、 段 5 到達
  precedent)
- [[feedback-collatz-not-shannon-kolmogorov-analog-2026-08-11]] (Collatz analog framing
  訂正 pattern 直接継承)
- [[feedback-zero-sorry-floor-not-ceiling]] (「0 sorry = floor」 適用、 7 定理 全 axiom-free)
- [[feedback-world-uniqueness-claim-controllable]] (novelty 主張 ゼロ 遵守)
- [[feedback-external-community-outreach-premature]] (bbchallenge outreach 慎重 judgment)
- [[feedback-no-rush-publication]] (「急がずゆっくりと」、 骨格のみ)
- Rei Collatz STEP 622-624 48 定理 chain (直接 upstream)
- STEP 1297 Rei-Solver v0.4 万能 TM 外 3/3 全経路 operational (chat-Claude Turn 4
  「オラクル + アイデア」 議論 alignment)