Paper 158 v0.2 — Collatz Exit Layer: m_p = (4^p − 1)/3의 Zero-Sorry Lean 4 형식화 및

이 기사는 dev.to 커뮤니티를 위해 Rei-AIOS Paper 158을 재출판한 것입니다.
전체 참조 목록이 포함된 정식 버전은 아래의 영구 아카이브에 있습니다:

• GitHub 소스 (비공개): https://github.com/fc0web/rei-aios 저자: Nobuki Fujimoto (@fc0web) · ORCID 0009-0004-6019-9258 · 라이선스 CC-BY-4.0 ---

m_p = (4^p − 1)/3의 Zero-Sorry Lean 4 형식화 (Formalization), 그리고 그 너머의 7개 경로 벽에 대한 정직한 지도

부제 (JA): コラッツ「出口層」の Lean 4 完全形式化と、 その先の七ルートの壁の honest 地図 — 否定的成果として

상태 (Status): v0.1 (PUBLISHED — Zenodo + IA)
초안 작성일: 2026-05-29 (v0.0); 당일 v0.1로 승격 및 출판됨.
Zenodo DOI: 10.5281/zenodo.20435288 (deposit 20435288, 2026-05-29 최종 확정, 변경 불가).
Internet Archive: https://archive.org/details/rei-aios-paper-158-1780003374000
고정된 결과물 (Pinned artifacts): data/lean4-mathlib/CollatzRei/ExitLayer.lean @ Rei-AIOS 커밋 372321c1c7001680424749fc4d11043062e4f024 (STEP 1179, "exit-layer 공식의 역, Lean에서 형식화됨 (zero-sorry)"). Mathlib v4.27.0 @ 커밋 a3a10db0e9d66acbebf76c5e6a135066525ac900. Lean 툴체인 leanprover/lean4:v4.27.0.
v0.1 승인 항목 (모두 완료됨): (a) ★ ラーメン好きさん으로부터의 동의 수령 (2026-05-29 N. Fujimoto에 의해 확인됨); (b) §6 프런티어 경로 테이블 감사 완료 2026-05-28 (Janik / Tao / Baker / Conway); (c) ★ #print axioms 원문 출력 캡처 2026-05-29 및 부록 A.1에 붙여넣기 완료; (d) Rei-AIOS 커밋 해시 고정 (위 참조); (e) Mathlib 커밋 해시 고정 (위 참조); (f) Zenodo + IA 출판 완료 (옵트인 정책에 따라 Harvard는 제외됨); (g) 영문/일문 이중 언어 쌍은 v0.2로 연기됨 (선택 사항).

저자

저자

• Nobuki Fujimoto (藤本 伸樹) — 독립 연구원 (이전 FX) , 일본. ORCID: TBD. (개념화, Lean 4 형식화, 원고)
• Claude Opus 4.7 (Anthropic) — AI 협력자. (Lean 4 메커니즘 지원, 원고 초안 작성)
• 어떠한 저자도 학술적 소속을 주장하지 않습니다. 독립 연구원이라는 틀은 지지 기반이며 정직합니다 (Cardano/Thorp 型: 도박/시장 → 수학).

솔직한 비주장 사항 (지지 기반, 반드시 최상단에 위치)

본 논문은 다음을 주장하지 않습니다:

1. Collatz 추측(3x+1)의 증명.
2. $ ext{N}$에 대한 역 Collatz 트리 커버리지에 관한 새로운 수학적 정리.
3. 관찰 $ ext{m}_p = (4^p - 1)/3$ ($ ext{= } 1, 5, 21, 85, 341, ext{…}$)의 참신성. 이 수열은 Collatz 문헌에서 잘 알려져 있습니다 (Lagarias 1985 및 주변 Jacobsthal-Collatz 논문).
4. 일곱 가지 후보 경로(Janik confinement, Tao 2019, 2-adic Hensel, Baker linear forms, automata/parity, inverse-tree/Jacobsthal, undecidability)의 참신성 — 모두 기존에 존재하는 것입니다.
5. 우리가 한 계층을 형식화했다고 해서 어떤 경로가

(C2) 탈출 계층 (exit layer) 내부의 작은 역 미분 (inverse calculus) (Lean 4 zero-sorry): 역 점화식 exitM_pred : m_p = (m_{p+1} − 1)/4, 유일성 역전 exitM_of_eq : 3m + 1 = 4^p ⟹ m = m_p, 그리고 p-복구 exitM_recover_p : Nat.log 2 (3·m_p + 1) = 2p.

(C3) 7개의 후보 축소 경로에 대한 큐레이션된 프런티어 지도 (curated frontier map) (표 1). 각 경로는 무엇이 증명되었는지, 화살표가 어디서 끊기는지 (정직한 간극, honest gap), 그리고 2026-05-28에 수행된 grep 감사(audit)를 통한 Mathlib v4.27.0 커버리지 평가가 주석으로 달려 있습니다. 이 지도는 새로운 화살표가 아니라 제안자 역할을 합니다.

(C4) 정직한 부정적 결과 프레이밍 (honest negative-result framing): 탈출 계층을 완전히 형식화하는 것은 벽을 낮추는 것이 아니라, 벽을 더 잘 보이게 만듭니다. 난이도 보존 (Janik의 방식에 따른)이 핵심적인 메타 주장 (load-bearing meta-claim)입니다.

출처 및 귀속 (Provenance and attribution)

3m + 1 = 2^n의 정수해가 n이 짝수일 때만 발생하며 (왜냐하면 2^n ≡ (−1)^n mod 3 이기 때문), 그 결과로 나타나는 홀수들이 m_p = (4^p − 1)/3 = 1, 5, 21, 85, 341, … 의 가족을 형성한다는 관찰은 ラーメン好き (Ramen-suki, 필명; 프로필 자기소개: "두부 같은 멘탈로 숫자를 세고 있습니다")가 note.com 기사 https://note.com/yaminotikara를 통해 N. Fujimoto에게 전달한 내용입니다. 폐쇄형(closed form)인 (4^p − 1)/3은 고전적인 Collatz 참고 문헌(예: Lagarias 1985, AMM 92)에 암시되어 있지만, 이 논문의 경로 선택, 프레이밍, 그리고 Lean 4 형식화는 ラーメン好き의 노트 설명을 직접적으로 따르고 있으며, 그 기원을 이곳 기록에 남깁니다. ラーメン好き는 초안 작성 전에 통보를 받았으며, 해당 필명과 URL로 인용 및 감사를 받는 것에 동의했습니다.

우리는 다음을 강조합니다: m_p가 2p + 1번의 Collatz 단계 내에 1에 도달한다는 결과는 새로운 수학적 발견이 아닙니다. 이 논문이 기여하는 바는 기계 검증이 가능한 Lean 4 기록, 탈출 계층 내부의 역 미분 (inverse calculus), 그리고 정직한 프런티어 지도입니다.

1 서론 (Introduction)

콜라츠 추측 (Collatz conjecture)은 모든 양의 정수 $n$에 대하여 반복 연산 $T(n) = n/2$ ($n$이 짝수일 때), $T(n) = 3n+1$ ($n$이 홀수일 때)이 결국 1에 도달한다고 주장합니다. 80년 동안의 관심에도 불구하고 이 문제는 여전히 미해결 상태로 남아 있으며, "수학은 아직 이러한 문제를 다룰 준비가 되지 않았다"라는 에르되시(Erdős)의 언급은 여전히 유효합니다.

본 논문은 콜라츠 문제를 해결하려는 시도가 아닙니다. 이는 정직한 부정적 진전 (negative-progress)을 의도적으로 수행하는 연습입니다. 우리는 다루기 쉬운 관찰 결과인 "탈출 층 (exit layer)" $m_p = (4^p - 1)/3$ — 즉, 단 한 번의 $3x+1$ 단계를 거친 후 이진 척추 (dyadic spine) $2^{2p}$에 도달하는 홀수들 — 을 가져와서, 이 계열에 대한 궤도-1 (orbit-to-1) 명제를 Zero-Sorry 및 최소한의 공리만을 사용하여 Lean 4로 완벽하게 형식화 (formalise) 합니다. 그런 다음 우리는 의도적으로 질문합니다: 이 형식화가 콜라츠 증명을 가로막는 어떤 벽이라도 낮추는가? 우리는 경로별로 그 대답이 _아니오_임을 밝힙니다. 우리는 7개의 후보 축소 경로 (Lagarias의 주석 달린 참고 문헌을 2019~2026년의 발전 사항으로 업데이트하여 선별한 부분 집합)를 제시하며, 각 경로의 화살표가 정확히 어디에서 끊어지는지를 표시합니다. 그 결과는 벽을 통과하는 통로가 아니라, 벽에 대한 지도입니다.

우리는 이러한 종류의 논문이 쓸 가치가 있다고 믿습니다. 이는 유혹 ("멋진 폐쇄형 계열이 있으니 분명히 발판이 될 거야!")을 작고 검증 가능하며, Lean을 실행함으로써 반증 가능한 (disprovable-by-running-the-Lean) 산출물로 변환하고, 그 주변을 둘러싼 난이도 보존 (difficulty conservation)에 대한 공개적인 기록을 남기는 작업입니다.

1.1 우리가 측정한 것 (한 줄 요약)

§6에 목록화된 7개의 경로 중, 7개 모두 우리의 형식화 이후에도 붕괴 지점이 변하지 않은 채 유지되었습니다. 탈출 층 Lean 모듈은 이 중 단 하나도 축소시키지 못했습니다. 이것이 결과입니다.

1.2 로드맵 (Roadmap)

§2는 표기법 (notation)을 수정합니다. §3은 Lean 4를 사용하여 탈출 층 정리 (exit-layer theorem)를 기술하고 증명합니다 (스켈레톤 형태; 전체 소스 코드는 부록 A에 수록). §4는 탈출 층 내부의 작은 역 계산 (small inverse calculus)을 전개하며, 왜 "한 분기에서의 역 폐쇄 형식 (inverse closed form on one branch)"이 역 Collatz 축소 (inverse Collatz reduction)가 _아닌지_를 설명합니다. §5는 역 Collatz 트리 (inverse Collatz tree)의 하단 층 (STEP 1177)을 시각화하고, 이것이 왜 벽의 잘못된 쪽인지 다시 한번 설명합니다. §6은 프런티어 표 (frontier table)입니다. §7은 Mathlib 커버리지를 논의합니다. §8은 정직한 부정적 결과 프레이밍 (honest negative-result framing)입니다. §9는 감사의 글입니다. 부록에는 전체 Lean 소스, #print axioms, 역 트리 생성기 (STEP 1177), 그리고 프런티어 맵 (frontier-map) JSON (STEP 1178)이 제공됩니다.

2 표기법 (Notation)

collatzStep : ℕ → ℕ은 (CollatzRei.Basic에서) n이 짝수일 때 collatzStep n = n/2, n이 홀수일 때 collatzStep n = 3n + 1로 정의됩니다. collatzStep^[k]는 k번의 반복 (k-fold iteration)을 의미합니다. Reaches1 n은 ∃ k, collatzStep^[k] n = 1을 의미합니다. 우리는 주요 명제에서 압축된 맵 $T(n) = (3n+1)/2$를 사용하지 않는데, 그 이유는 압축되지 않은 형태에서 기초적인 1단계 도달 조건인 $3m + 1 = 4^p$가 가장 깔끔하기 때문입니다.

**탈출 층 (exit layer)**은 exitM : ℕ → ℕ이며, exitM 0 = 0, exitM (p+1) = 1 + 4 · exitM p입니다. 귀납법 (induction)에 의해, exitM p = (4^p − 1)/3 = 1 + 4 + 4² + … + 4^(p−1)입니다.

3 Lean 4에서의 탈출 층 정리 (The exit-layer theorem in Lean 4)

3.1 핵심 항등식 (Core identity)

보조정리 3.1 (three_mul_exitM_add_one). 모든 $p ∈ ℕ$에 대하여, 3 ⋅ exitM p + 1 = 4^p이다.

증명 (Lean 4 스케치). $p$에 대한 귀납법. 기저 (Base): simp [exitM]에 의해 자명함. 단계 (Step): 3 ⋅ exitM (q+1) + 1 = 4 ⋅ (3 ⋅ exitM q + 1) (대수학)로 재작성하고, 귀납 가정 (IH)과 pow_succ를 사용함. ring에 의해 종료됨.

3.2 폐쇄 형식의 일치 (Closed-form coincidence)

보조정리 3.2 (exitM_eq_div). exitM p = (4^p − 1)/3이다.

증명. 보조정리 3.1과 omega로부터 즉각 도출됨.

3.3 홀수성 및 1단계 도달 (Oddness and one-step landing)

보조정리 3.3 (exitM_odd). 모든 $q ∈ ℕ$에 대하여, exitM (q + 1) ≡ 1 (mod 2)이다.

보조정리 3.4 (collatzStep_exitM). 모든 $q ∈ ℕ$에 대하여, collatzStep (exitM (q + 1)) = 4^(q+1)이다.

증명 (Proof). 보조정리 3.3 (Lemma 3.3)에 의해, exitM (q+1)은 홀수이므로, collatzStep은 $3x+1$ 분기를 따릅니다. 그 결과는 $(q+1)$에서 평가된 보조정리 3.1 (Lemma 3.1)과 같습니다.

3.4 이진 스파인 (Dyadic spine)

보조정리 3.5 (Lemma 3.5) (pow2_reaches_one). 모든 $j ∈ ℕ$에 대하여, collatzStep^[j] (2^j) = 1이다.

증명 (Proof). collatzStep_pow2 : collatzStep (2^(j+1)) = 2^j를 사용하여 $j$에 대해 귀납법 (Induction)을 적용한다.

3.5 주요 정리 (Main theorem)

정리 3.6 (Theorem 3.6) (exitM_reaches_one). 모든 $q ∈ ℕ$에 대하여, collatzStep^[2(q+1) + 1] (exitM (q+1)) = 1이다.

증명 (Proof). 한 단계(one step)를 거치면 $4^{q+1} = 2^{2(q+1)}$에 도달하며 (보조정리 3.4 (Lemma 3.4) + four_pow_eq), 그 후 $2(q+1)$번의 추가 단계가 진행되면 1로 절반씩 줄어듭니다 (보조정리 3.5 (Lemma 3.5)).

따름정리 3.7 (Corollary 3.7) (exitM_reaches_one_of_pos). 모든 $p ≥ 1$에 대하여, Reaches1 (exitM p)이다. ∎

3.6 공리 감사 (Axiom audit)

하중을 지탱하는(load-bearing) 6개의 정리에 대해 lake env lean으로 #print axioms를 실행한 결과, 세 가지 표준 Lean 4 기초 요소인 propext, Classical.choice, Quot.sound만을 보고합니다. 역 점화식(inverse recurrence) exitM_pred (omega에 의해 증명됨)는 더욱 깔끔하며, 오직 [propext, Quot.sound]에만 의존합니다. 주요 정리 체인에는 sorryAx나 Lean.ofReduceBool (native_decide의 기초가 되는 공리)이 존재하지 않습니다. 두 가지 구체적인 수치 예시(five_reaches_one, twentyone_reaches_one)는 native_decide를 사용하지만, 이는 장식적인 요소일 뿐 하중을 지탱하는 주장(load-bearing claim)의 일부는 아닙니다. 2026-05-29에 캡처된 원문 출력 결과는 **부록 A.1 (Appendix A.1)**에 재현되어 있습니다.

전체 Lean 4 소스 코드는 **부록 A (Appendix A)**에 재현되어 있으며, Rei-AIOS 저장소의 data/lean4-mathlib/CollatzRei/ExitLayer.lean에서 추적할 수 있습니다 (커밋 해시는 v0.1 동결 시점에 고정될 예정입니다).

4 탈출 계층 내부의 역 미분법 (The inverse calculus inside the exit layer) (그리고 이것이 왜 역 Collatz 축소가 아닌가)

탈출 계층(exit-layer)은 깔끔한 순방향 점화식(forward recurrence) exitM (p+1) = 1 + 4 · exitM p를 만족하며, 따라서 깔끔한 역 점화식(inverse recurrence)을 가집니다:

보조정리 4.1 (Lemma 4.1) (exitM_pred). exitM p = (exitM (p+1) − 1)/4.

보조정리 4.2 (Lemma 4.2) (exitM_of_eq, 유일성 역전).
만약 $3m + 1 = 4^p$ 이면 $m = exitM ext{ }p$ 이다.

보조정리 4.3 (exitM_recover_p). Nat.log 2 (3 · exitM p + 1) = 2p (즉, $p = ½ · ext{log}_2(3m + 1)$).

이것들은 역트리 (inverse tree)의 한 가지 (branch)에 대한 긴밀한 대수적 이야기를 제공합니다. 즉, exit layer의 원소가 주어지면, 우리는 순방향으로 진행하고, 역방향으로 진행하며, 그 인덱스 (index)를 폐쇄형 (closed form)으로 복구할 수 있습니다. 이 중 그 어떤 것도 일반적인 Collatz 역문제 (inverse Collatz problem)를 다루지 않습니다. 왜냐하면 Collatz에 대한 전역적인 층(rung)에서 층+1로의 질문은 "역트리가 모든 $\mathbb{N}$을 커버하는가?"인 반면, 위의 역 미적분 (inverse calculus)은 단 하나의 가지인 $1 \to 5 \to 21 \to 85 \to \dots$의 척추 (spine)만을 추적하기 때문입니다. 이 가지는 정확하지만, 트리는 미해결 문제입니다.

우리가 이 점을 강조하는 이유는 "한 가지의 폐쇄형을 역전시켰다"는 것을 "Collatz를 역전시켰다"는 것과 혼동하는 것이 역트리 접근 방식의 전형적인 실패 모드이기 때문입니다 (\S6, 경로 6 참조).

5 역 Collatz 트리의 하위 층들

압축된 홀수-대-홀수 (odd-to-odd) Collatz 맵 $T_{\text{odd}}(n) = (3n + 1)/2^{v(3n+1)}$은 역함수를 가집니다. 홀수 $n$의 선행자 (predecessors)들은 패리티-가분성 조건 (parity-divisibility condition)을 만족하는 $k \ge 1$에 대해 $(n \cdot 2^k - 1)/3$ 형태의 양의 홀수들입니다. STEP 1177은 루트 1로부터 $k=1\dots5$에 대해 이 BFS (너비 우선 탐색)를 계산하며, 처음 5개 층(크기 1, 3, 6, 12, 24)에 걸쳐 46개의 노드를 가진 트리를 생성합니다.

exit-layer 패밀리 $(4^p - 1)/3$은 정확히 루트로부터의 $k = 1$ 가지입니다. 즉, 척추 $1 \to 5 \to 21 \to 85 \to 341 \to \dots$입니다. $k \ge 2$인 선행자들은 트리의 나머지 부분으로 퍼져 나갑니다 (예: $\text{pred}(5) = {3, 13, 53, 213, \dots}$). 3의 배수들은 역트리의 *진정한 리프 (true leaves)*입니다. 왜냐하면 $3n + 1 \not\equiv 0 \pmod 3$이므로, 이들은 $T_{\text{odd}}$의 상 (images)으로 나타날 수 없기 때문이며, 이는 잘 알려진 사실입니다.