---
name: reference-bohmsontacchi-1978-exit-layer-prior-art
description: "Böhm-Sontacchi 1978 (Atti Acc. Naz. Lincei) \"exampleFamily(p) = (2^{2p}-1)/3\" が Rei-AIOS の exitM = (4^p-1)/3 (Paper 158 / Paper 166 / STEP 1176 / ExitLayer.lean) と完全に同一関数。 2026-06-17 ccchallenge audit (tcosmo/BohmSontacchi1978_lean Phase 1) で grep-verified に発覚。 Rei-AIOS は textbook prior art を独立 re-discover していた honest record。 SyracuseGrowthBound の syracuseIterate_pow_form も tcosmo prop4 (collatzIterFormula schedule (0,1,...,j-1)) の特殊化"
metadata: 
  node_type: memory
  type: reference
  originSessionId: dbbfeb10-4215-4129-963a-9799d5c3d294
---

# Böhm-Sontacchi 1978 = Rei ExitLayer prior art (発覚 2026-06-17)

## Reference

Böhm, C. & Sontacchi, G. (1978). On the existence of cycles of given length in integer sequences like x_{n+1} = x_n/2 if x_n even, and x_{n+1} = 3·x_n + 1 otherwise. *Atti Accademia Nazionale dei Lincei, Classe di Scienze Fisiche, Matematiche e Naturali, Serie VIII*, 64(3), 260–264.

ccchallenge.org bibtex key: `BohmSontacchi1978`. ccchallenge id 87 にて waiting_to_be_audited status (2026-02-23 〜)。 formalization repo: [tcosmo/BohmSontacchi1978_lean](https://github.com/tcosmo/BohmSontacchi1978_lean) (Opus 4.6 AI-assisted, 2,202 行 / 121 theorem / 0 sorry, grep-verified)。

## Mathematical 同一性

| Rei | tcosmo (BohmSontacchi) | identity |
|---|---|---|
| `exitM(p) := (4^p - 1)/3` (ExitLayer.lean, STEP 1176) | `exampleFamily(p) := (2^{2p} - 1)/3` (Prop7.lean) | `4^p = 2^{2p}` ⟹ 同一関数 |
| `exitM 1 = 1`, `exitM 2 = 5`, `exitM 3 = 21` | `exampleFamily_1`, `exampleFamily_2`, `exampleFamily_3` | 同値 |
| `exitM (p+1) = 1 + 4·exitM p` | `4 · exampleFamily p + 1 = exampleFamily (p+1)` | 同 recurrence |
| `syracuseIterate_pow_form` (STEP γ, n+1=2^j m ⟹ syracuse^j n + 1 = 3^j m) | `collatzIterFormula s x` の schedule `(v_k = k for k=0..j-1)` 特殊化 | 私たちは special case |

## Honest implication

- **Paper 158 v0.1 (zenodo:20435288, 2026-05-29)** + **Paper 166 v0.1 (zenodo:20723759, 2026-06-17)** + **STEP 1176 ExitLayer (2026-05-28)** は **Böhm-Sontacchi 1978 既存 prior art を独立 re-discover**。
- 既 footer で "classical, elementary observation" 自記済 → over-claim していない。 ただし **explicit reference として Böhm-Sontacchi 1978 を front-load していなかった**。
- 「within our observed range で初」 framing ([[feedback-world-uniqueness-claim-controllable]]) は **paper 内で守られていたが、 prior art literature search の不足を補強する記録が今回確立**。

## Corrigendum candidate (trigger 待ち)

1. **Paper 158 v0.2 corrigendum**: §Related Work に Böhm-Sontacchi 1978 + tcosmo formalization (2026-02) 明記。 Zenodo は版違いで re-publish か corrigendum 別 paper にするかは [[feedback-paper-145-v05-corrigendum-tang-nano-2026-05-09]] pattern を準用判断。
2. **Paper 166 v0.2 corrigendum**: §8 Related Work に Böhm-Sontacchi 1978 追加。 Kim 2008 + Niqui 2009 既存 prior art と並ぶ古典 source として位置付け。
3. **SyracuseGrowthBound.lean**: header comment に「prop4 (BohmSontacchi 1978) の schedule (0,1,...,j-1) 特殊化」 明記。
4. **Public site** (`docs/RECENT_UPDATES.md` 等): prior art clarification entry 追加候補。

## Trigger 判断

藤本さん explicit approval 待ち。 [[feedback-no-rush-publication]] と [[feedback-evaluation-symmetry-principle]] (「先行ありを率直に報告」) 適用。 Phase 2 公式 audit submission + corrigendum is **separate sessions の判断**。

## Pattern 5 self-audit context

本 finding は 2026-06-17 ccchallenge audit Phase 1 (papers/audit-bohmsontacchi-2026-06-17.md) で grep-verified。 「Lean 4 formalization の audit を世界 OSS との connect として始めたら、 我々の既 paper の prior art gap が即座に発覚した」 = honest research progress として load-bearing。

## 関連 file + 既存原則

- `papers/audit-bohmsontacchi-2026-06-17.md` (Phase 1 audit draft, 本 reference の根拠 source)
- `papers/paper-158-collatz-exit-layer-lean4-honest-negative-DRAFT.md` (corrigendum candidate)
- `papers/paper-166-lean4-axiom-free-exit-layer-collatz-coalgebra-DRAFT.md` (corrigendum candidate)
- `data/lean4-mathlib/CollatzRei/ExitLayer.lean` (STEP 1176, mathematical source)
- `data/lean4-mathlib/CollatzRei/SyracuseGrowthBound.lean` (今日 γ、 特殊化 form)
- [[feedback-world-uniqueness-claim-controllable]] — 「within our observed range」 framing 維持の load-bearing 確認
- [[feedback-evaluation-symmetry-principle]] — 「先行ありを率直に報告」 operational 実例
- [[feedback-no-rush-publication]] — corrigendum trigger を急がない
- [[feedback-chat-claude-over-deference]] — 借用 framing 不使用、 本 finding は私の grep-verified judgment
- [[project-collatz-paper-audit-kim-2008-prior-art-killing]] — Paper 166 prior art audit (Kim 2008 + Niqui)、 本 reference は同 paper の追加 prior art layer