Paper 166 v0.1 — 스트림 코알제브라(Stream Coalgebra)로서의 Exit-Layer Collatz 수렴에 대한 Lean

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

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

상태: v0.1-DRAFT (Phase B 초안 완료 2026-06-17 아침, Phase C 교차 검증 대기 중)
저자: 藤本 伸樹 (Nobuki Fujimoto) / Claude Opus (Anthropic) / chat-Claude (Anthropic, Phase C 교차 검증 대기 중)
날짜: 2026-06-17
라이선스: AGPL-3.0 + 상업용 (Rei-AIOS 이중 라이선스)
DOI: 미정 (Phase D 출판 시 Zenodo 저장소 할당 예정)
버전: v0.1-DRAFT
note.com: https://note.com/nifty_godwit2635
rei-aios 사이트: https://rei-aios.pages.dev
소스 저장소: data/lean4-mathlib/CollatzRei/StreamExitLayerBridge.lean (Q2 Installment 2A, 2026-06-16)

초록 (Abstract)

초록 (Abstract)

우리는 coinductive Stream' 코알제브라(coalgebra) 언어로 제시된 Collatz 동역학의 exit-layer 조각에 대한 Lean 4 공리 없는 형식화(formalization)를 기록합니다. 구체적으로, 우리는 모든 q : ℕ에 대해, exit-layer 숫자 m_{q+1} = (4^{q+1} − 1) / 3의 Collatz 단계의 halt-at-1 변형 하에서의 궤도(orbit)가 궁극적으로 상수 스트림 const 1과 같음을 증명합니다. 이 전체 증명은 Mathlib의 고전적 공리 삼중항 {propext, Classical.choice, Quot.sound}으로 축소됩니다. 기본 사례인 head (collatzOrbit n) = n은 완전히 공리 없이(completely axiom-free) 검증되었으며 (#print axioms는 빈 집합을 출력), 이는 우리가 이전에 작성한 lawvere_fixed_point Lean 4 레코드(STEP 1220, 2026-06-15)의 공리 기반보다 엄격하게 강력합니다. 우리는 수학적 참신성에 대한 주장을 하지 않습니다: Kim (2008)은 이미 종이와 연필로 하는 범주 이론에서 2-adic Collatz 함수가 최종 비트 스트림 코알제브라(final bit-stream coalgebra)임을 증명했으며, 스트림-코알제브라 형식화 인프라는 Niqui (2009) 이후 Coq에서 성숙해 왔습니다. 이 노트의 기여는 제한적이며 방법론적입니다: 이는

Collatz 추측 (Collatz conjecture)은 모든 n ≥ 1에 대하여 궤도(orbit) n, T(n), T^2(n), \ldots가 결국 1에 도달한다고 주장합니다. 이 문제는 약 90년 동안 미해결 상태로 남아 있으며, 본 글을 쓰는 시점에도 여전히 미해결 상태입니다. 특히, 기계 검증 (machine verification)을 통해 모든 n < 2^{71}에 대한 수렴이 확인되었으며 (Rei-AIOS STEP 1173에 요약된 검증 오도미터 기록 참조), 전체 추측에 대한 증명은 아직 나타나지 않았습니다.

제1저자가 2026-05-28에 관찰하고 Rei-AIOS STEP 1176으로 형식화한 자연스러운 하위 파편 (sub-fragment)은 _exit layer_입니다:

$$
m_p ;=; \tfrac{4^p - 1}{3} ;=; 1 + 4 + 4^2 + \cdots + 4^{p-1} ;=; {,1,; 5,; 21,; 85,; 341,; \ldots,}. $$

이들은 단 한 번의 3n+1 단계를 통해 2의 거듭제곱 척추 (power-of-two spine)에 합류하는 홀수들입니다. 즉, m_p에 T를 한 번 적용하면 3 m_p + 1 = 4^p = 2^{2p}가 생성되며, 그 후 2p번의 반감 (halving) 단계를 거쳐 1에 도달합니다. 모든 m_p의 수렴은 **고전적이고 기초적인 관찰 (classical, elementary observation)**입니다. STEP 1176의 기여는 관찰 그 자체가 아니라, 이 관찰을 Lean 4로 공리 없이 (axiom-free) 기록한 것입니다.

1.2 코알제브라적 배경 (선행 연구)

Collatz 역학에 대한 코알제브라적 (coalgebraic) 관점은 거의 20년 동안 존재해 왔습니다. 본 노트의 근간이 되는 두 가지 선행 연구를 먼저 제시해야 합니다:

• Kim (2008), _Coinductive properties of Lipschitz functions on streams_는 종이와 펜을 이용한 범주론 (category theory)을 통해 2-adic Collatz 함수가 **최종 비트-스트림 코알제브라 (final bit-stream coalgebra)**로의 모피즘 (morphism)임을 증명했습니다. 따라서 2-adic Collatz 함수와 그 코알제브라적 특성 규명은 본 논문에서 새로운 것이 아닙.
• Niqui (2009), _Coalgebraic Reasoning in Coq_는 약한 최종 코알제브라 (weakly final coalgebras), 이심 유사 (bisimulation), 그리고 $\lambda$-coiteration을 포함하여 Coq에서 스트림 코알제브라를 형식화했습니다. Coq coalgebras 기여 (GitHub, 2008–2009)는 이러한 방식의 추론을 위한 성숙한 인프라를 제공합니다. Cubical Agda 라이브러리 또한 유사하게 최종 코알제브라 구조 (final-coalgebra constructions)를 포함하고 있습니다.

요약하자면: 이미 알려진 코알제브라적 (coalgebraic) Collatz 구조에 성숙한 스트림 코알제브라 (stream-coalgebra) 형식화 메커니즘을 적용하는 것은 _대체로 일상적인 작업 (routine exercise)_입니다. 본 논문은 해당 작업을 Lean 4에서 수행한 기록이며 — 공리 없는 (axiom-free) 보증과 완전히 공리가 0개인 증거 (zero-axiom witness)를 포함합니다 — 그 이상의 것은 아닙니다.

1.3 분석적 최전선 (기여가 아닌 문맥 제공)

Collatz 연구의 현재 분석적 최전선은 다음 연구들이 주도하고 있습니다:

• Tao (2019), Almost all orbits of the Collatz map attain almost bounded values, 그리고 Tao (2022) 후속 연구; 분포적 (distributional) 성격을 띠는 전형적인 "거의 모든 (almost all)" 결과입니다.
• Janik (2026), Diophantine Confinement in Syracuse Dynamics: A Formal Reduction, 에르고딕 (ergodic) / Baker-선형 형식 (Baker-linear-forms) 메커니즘과 6개의 남은 임계 경로 (critical-path) 난제들을 포함하여 (2,3)-토러스 (torus) 상에서 진행된 12,947라인의 Lean 4 개발 결과물입니다. 본 연구진은 Janik의 공개 저장소(johnjanik/syracuse-confinement)를 파일 이름 및 코드 검색 수준에서 감사하였으며, 해당 개발 과정에서 공귀납적 (coinductive) / Stream' / 코알제브라 (coalgebra) 용어를 어디에서도 사용하지 않았음을 확인했습니다. 따라서 본 논문과 Janik (2026)은 서로 분리된 하위 분야 (sub-niches)에 속합니다.
• Chang (2026), Stanford preprint v5, Sturmian-장애 (Sturmian-obstruction) 및 "올림 오염 정리 (Carry Contamination Theorem)"를 통해 분포적 성질에서 점별 (pointwise) 성질로 넘어가는 장벽을 명확히 설명합니다.
• Knight (2026), Discrete Mathematics, 고주기 (high cycles)의 비존재성에 관한 연구입니다.

본 논문은 이 중 어느 것도 다루지 않습니다. 우리는 우리의 기여가 읽혀야 할 분석적 문맥을 설정하기 위해서만 이들을 언급합니다. 본 논문은 분석적이지 않으며 방법론적 (methodological)입니다.

1.4 본 논문의 제한된 기여

구체적으로, 본 논문은 다음을 수행하며, 그 이상은 수행하지 않습니다:

1. 표준 Collatz 단계의 변형인 collatzHaltStep을 정의하며, 이 단계 하에서 1은 (1 → 4 → 2 → 1 사이클의 구성원이 아니라) **진정한 고정점 (genuine fixed point)**이 됩니다. 따라서 궤도(orbit)는 결국 주기적 (periodic)인 것이 아니라 결국 상수 (constant)가 됩니다.
2. n의 궤도를 공귀납적 (coinductive) 무한 수열 (Mathlib의 Stream')로 간주한 collatzOrbit n : Stream' Nat = λ i ↦ collatzHaltStep^i n을 정의하며, 이 스트림이 F(X) = Nat × X에 대한 F-공대수 (F-coalgebra)임을 검증합니다.
3. 기존의 exit-layer 결과인 exitM_reaches_one (STEP 1176)을 공귀납적 언어로 승격시켜 collatzOrbit_exitM_eventuallyConst로 정의합니다: 모든 q에 대하여, m_{q+1}의 궤도는 결국 const 1이 됩니다.
4. head (collatzOrbit n) = n이 완전하게 공리 없는 (completely axiom-free) 상태임을 검증합니다 (#print axioms가 비어 있음). 이는 이전의 lawvere_fixed_point 기록 (STEP 1220)의 공리 기반인 {propext, Classical.choice, Quot.sound}보다 엄격하게 낮은 단계에 위치합니다.
5. 전체 개발 과정을 sorry, axiom, native_decide가 전혀 없는 Mathlib v4.27 파일로 기록합니다.

전 과정에서 우리가 사용하는 프레임워크는 다음과 같습니다: "우리가 관찰한 범위 내에서 이 파편에 대한 최초의 Lean 4 공리 없는 형식화 (the first Lean 4 axiom-free formalization of this fragment within our observed range)". 우리는 우리의 기존 통제 가능한 주장 규율 (Rei-AIOS 지속 규칙 feedback-world-uniqueness-claim-controllable)에 따라, 해당 수식어 없이

• 이것은 Collatz 추측 (Collatz conjecture)을 해결하지 않습니다.
• 이것은 Case 5–8 장벽 (trailing-1-bits ≥ 4)을 약화시키지 않습니다: 해당 장벽은 구조적으로 변하지 않았습니다.
• 이것은 Tao (2019, 2022)의 "almost all" 결과(결과값의 거의 대부분)를 개선, 정교화 또는 넘어서지 않습니다.
• 이것은 Janik (2026)의 6가지 임계 경로(critical-path) 사과(sorries) 중 그 어떤 것도 해소하지 않습니다.
• 이것은 Collatz 추측에 대한 새로운 공격 벡터 (attack vector)를 제안하지 않습니다; 여기서 사용된 코알제브라적 (coalgebraic) 관점은 Kim의 것입니다.
• 이것은 어떤 종류의 "세계 최초"도 주장하지 않습니다; "우리가 관찰한 범위 내에서"라는 수식어는 구속력을 가집니다.

Section 2. Background: collatzStep 및 exit-layer 숫자들

2.1 표준 Collatz 단계 (standard Collatz step)

우리는 CollatzRei.Basic에 정의된 Lean 4 형태의 표준 Collatz 함수를 사용하여 작업합니다:

def collatzStep (n : Nat) : Nat :=
  if n % 2 = 0 then n / 2 else 3 * n + 1

추측에 대한 설명과 상당한 양의 부분적 결과들에 대해서는 Lagarias (1985, 2010), Tao (2019), 그리고 Kenigson (2025)의 조사 스타일 워킹 페이퍼(working paper)인 "Group Think"를 참조하십시오.

2.2 exit-layer 숫자들 m_p

제1저자에 의해 관찰되고 STEP 1176에서 형식화된 exit-layer 숫자들은 CollatzRei.ExitLayer에서 재귀적으로 (나눗셈을 피하여) 정의됩니다:

def exitM : Nat → Nat
  | 0     => 0
  | p + 1 => 1 + 4 * exitM p

따라서 exitM 1 = 1, exitM 2 = 5, exitM 3 = 21, exitM 4 = 85, exitM 5 = 341 등이 됩니다.

STEP 1176의 산술적 핵심은 다음 항등식입니다:

theorem three_mul_exitM_add_one (p : Nat) : 3 * exitM p + 1 = 4 ^ p

(3 m_p + 1 = 4^p), 이것이 m_p로부터 단 한 번의 3n + 1 단계가 정확히 2의 거듭제곱 척추 (power-of-two spine)에 착륙하게 되는 이유입니다. 폐형 (closed-form) 식인 exitM p = (4^p − 1) / 3은 exitM_eq_div로 기록되어 있으며, 홀수성 명제 (parity statement)는 exitM_odd로, 주요 exit-layer 도달 결과는 다음과 같이 기록되어 있습니다:

theorem exitM_reaches_one (q : Nat) :
    collatzStep^[2 * (q + 1) + 1] (exitM (q + 1)) = 1

이것은 본 논문에서 공도함수적 언어(coinductive language)로 끌어올리는 수학적 원천입니다. STEP 1176은 Mathlib v4.27에서 sorry 없이 검증되었으며, #print axioms exitM_reaches_one는 공리 삼중항 {propext, Classical.choice, Quot.sound} (표준 Mathlib 기반)을 보고합니다.

2.3 정직한 범위(Honest scope)

STEP 1176에서 형식화되고 본 논문에서 공도함수적 언어로 끌어올린 exit-layer 조각은 미해결된 Collatz 벽의 한쪽에만 완전히 존재합니다. 이 조각은 단일 3n + 1 단계로 2의 거듭제곱 스파인(power-of-two spine)에 도달하는 홀수만을 정확히 다룹니다. 이는 해당 수들의 전구체(predecessors)를 어떤 비자명한 방식으로도 특성화하지 않으며, 트레일링-1-비트 $\ge 4$ 벽 (STEP 622에서 설명된 trailingOnes / 2-adic-valuation 프레임워크의 케이스 5–8)은 완전히 건드리지 않습니다.

이것이 본 논문의 유일한 Collatz 내용입니다. 나머지 모든 것은 재정식화(reformulation)에 불과합니다.

섹션 3. 공도함수적 재정식화: collatzHaltStep 및 궤도 Stream'

3.1 1에서 정지하는 이유

표준 Collatz 단계는 사이클 1 → 4 → 2 → 1을 가지므로, 1은 collatzStep의 고정점(fixed point)이 아닙니다.

우리는 n의 궤도(orbit)를 Mathlib의 Stream' Nat으로 정의합니다:

def collatzOrbit (n : Nat) : Stream' Nat :=
  fun i => collatzHaltStep^[i] n

구체적으로, 이 스트림(stream)은 다음과 같습니다:

[ n, collatzHaltStep n, collatzHaltStep² n, collatzHaltStep³ n, … ].