Share

    • Paper 166 — A Lean 4 Axiom-Free Formalization of Exit-Layer Collatz Convergence as a Stream Coalgebra: A Record Following Kim (2008)

    By 08jp…2p92 June 16, 2026
    We record a Lean 4 axiom-free formalization of the exit-layer fragment of the Collatz dynamics, presented in the language of coinductive Stream' coalgebras. Concretely, we prove that for every q : ℕ, the orbit of the exit-layer number m{q+1} = (4^{q+1} − 1) / 3 under a halt-at...

    Paper 166 — A Lean 4 Axiom-Free Formalization of Exit-Layer Collatz Convergence as a Stream Coalgebra: A Record Following Kim (2008)

    Status: v0.1-DRAFT (Phase B 起草完了 2026-06-17 朝、 Phase C cross-check 待ち) Authors: 藤本 伸樹 (Nobuki Fujimoto) / Claude Opus (Anthropic) / chat-Claude (Anthropic, cross-check pending Phase C) Date: 2026-06-17 License: AGPL-3.0 + Commercial (Rei-AIOS dual license) DOI: TBD (Zenodo deposit assigned at Phase D publish) Version: v0.1-DRAFT note.com: https://note.com/nifty_godwit2635 rei-aios site: https://rei-aios.pages.dev Source repo: data/lean4-mathlib/CollatzRei/StreamExitLayerBridge.lean (Q2 Installment 2A, 2026-06-16)

    Abstract

    We record a Lean 4 axiom-free formalization of the exit-layer fragment of the Collatz dynamics, presented in the language of coinductive Stream' coalgebras. Concretely, we prove that for every q : ℕ, the orbit of the exit-layer number m_{q+1} = (4^{q+1} − 1) / 3 under a halt-at-1 variant of the Collatz step is eventually equal to the constant stream const 1, with the entire proof reducing to Mathlib’s classical axiom triple {propext, Classical.choice, Quot.sound}. The base case head (collatzOrbit n) = n is verified to be completely axiom-free (#print axioms outputs the empty set), strictly stronger than the axiom base of our earlier lawvere_fixed_point Lean 4 record (STEP 1220, 2026-06-15). We make no claim of mathematical novelty: Kim (2008) already proved that the 2-adic Collatz function is a final bit-stream coalgebra in pen-and-paper category theory, and stream-coalgebra formalization infrastructure has been mature in Coq since Niqui (2009). The contribution of this note is limited and methodological: a Lean 4 + Mathlib v4.27 record, in the framing “first such Lean 4 axiom-free formalization within our observed range”, of a known coalgebraic structure on a known Collatz fragment. This paper does not resolve the Collatz conjecture, does not move past Tao (2019, 2022)’s “almost all” analytic boundary, does not touch the Cases 5–8 trailing-1-bits ≥ 4 wall, and does not address any of the six critical-path sorries in Janik (2026).

    Keywords: Collatz conjecture, exit layer, coalgebra, coinduction, Stream', Lean 4, Mathlib, axiom-free formalization, methodology note.

    Section 1. Introduction

    1.1 The Collatz problem and its exit layer

    The Collatz map (Collatz 1937; Lagarias 1985) is

    $$ T(n) \;=\; \begin{cases} n / 2 & n \text{ even} \\ 3n + 1 & n \text{ odd}. \end{cases} $$

    The Collatz conjecture asserts that for every n ≥ 1, the orbit n, T(n), T^2(n), \ldots eventually reaches 1. The problem has been open for roughly ninety years and remains open at the time of writing; in particular, machine verification has confirmed convergence for all n < 2^{71} (cf. the verification odometer record summarized in Rei-AIOS STEP 1173), and no proof of the full conjecture has appeared.

    A natural sub-fragment, observed by the first author on 2026-05-28 and formalized as Rei-AIOS STEP 1176, is the exit layer:

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

    These are exactly the odd numbers that join the power-of-two spine in a single 3n+1 step: applying T once to m_p produces 3 m_p + 1 = 4^p = 2^{2p}, after which 2p halving steps reach 1. The convergence of every m_p is a classical, elementary observation; the contribution of STEP 1176 was the Lean 4 axiom-free record of this observation, not the observation itself.

    1.2 Coalgebraic background (prior art)

    A coalgebraic perspective on Collatz dynamics has existed for nearly two decades. Two pieces of prior art are load-bearing for the present note and must be front-loaded:

    • Kim (2008), Coinductive properties of Lipschitz functions on streams, proved in pen-and-paper category theory that the 2-adic Collatz function is a morphism into a final bit-stream coalgebra. The 2-adic Collatz function and its coalgebraic characterization are therefore not new with the present paper.
    • Niqui (2009), Coalgebraic Reasoning in Coq, formalized stream coalgebras in Coq, including weakly final coalgebras, bisimulation, and λ-coiteration. The Coq coalgebras contribution (GitHub, 2008–2009) provides a mature infrastructure for this style of reasoning. The Cubical Agda library similarly carries final-coalgebra constructions.

    In short: applying mature stream-coalgebra formalization machinery to a known coalgebraic Collatz structure is largely a routine exercise. The present paper is a record of one execution of that routine — in Lean 4, with axiom-free guarantees and one completely zero-axiom witness — and nothing more.

    1.3 Analytic frontier (context, not contribution)

    The current analytic frontier of Collatz research is dominated by:

    • Tao (2019), Almost all orbits of the Collatz map attain almost bounded values, and Tao (2022) follow-up; the canonical “almost all” result, distributional in nature.
    • Janik (2026), Diophantine Confinement in Syracuse Dynamics: A Formal Reduction, a 12,947-line Lean 4 development on the (2,3)-torus with ergodic / Baker-linear-forms machinery and six remaining critical-path sorries. We have audited Janik’s public repository (johnjanik/syracuse-confinement) at the file-name and code-search level and confirm that the development does not use coinductive / Stream' / coalgebra terminology anywhere: the present paper and Janik (2026) inhabit disjoint sub-niches.
    • Chang (2026), Stanford preprint v5, with the Sturmian-obstruction and “Carry Contamination Theorem”, articulates a distributional-to-pointwise wall.
    • Knight (2026), Discrete Mathematics, on the non-existence of high cycles.

    None of these are touched by the present paper. We mention them only to fix the analytic context against which our contribution should be read; the present paper is methodological, not analytic.

    1.4 The limited contribution of this paper

    Concretely, this paper does the following, and no more:

    1. It defines a halt-at-1 variant collatzHaltStep of the standard Collatz step, under which 1 is a genuine fixed point (rather than a member of the 1 → 4 → 2 → 1 cycle), so that orbits become eventually constant rather than eventually periodic.
    2. It defines collatzOrbit n : Stream' Nat = λ i ↦ collatzHaltStep^i n, the orbit of n viewed as a coinductive infinite sequence (a Mathlib Stream'), and verifies that this stream is an F-coalgebra for F(X) = Nat × X.
    3. It lifts the existing exit-layer result exitM_reaches_one (STEP 1176) into the coinductive language as collatzOrbit_exitM_eventuallyConst: for every q, the orbit of m_{q+1} is eventually const 1.
    4. It verifies that head (collatzOrbit n) = n is completely axiom-free (#print axioms is empty), placing it strictly below the axiom base {propext, Classical.choice, Quot.sound} of our earlier lawvere_fixed_point record (STEP 1220).
    5. It records the entire development as a Mathlib v4.27 file with zero sorry, zero axiom, and zero native_decide.

    The framing we use, throughout, is: “the first Lean 4 axiom-free formalization of this fragment within our observed range”. We deliberately do not use the phrase “first” without that qualifier, in accordance with our standing controllable-claim discipline (Rei-AIOS persistent rule feedback-world-uniqueness-claim-controllable).

    1.5 What this paper is not

    To pre-empt overclaim by the reader (and by the authors, as a discipline imposed by Rei-AIOS rule feedback-evaluation-symmetry-principle), we state in front-loaded form what this paper does not do. The same list reappears, expanded, as Section 7.

    • It does not resolve the Collatz conjecture.
    • It does not weaken the Cases 5–8 wall (trailing-1-bits ≥ 4): that wall is structurally unchanged.
    • It does not improve, refine, or move past Tao (2019, 2022)’s “almost all” result.
    • It does not discharge any of the six critical-path sorries of Janik (2026).
    • It does not propose a new attack vector on the Collatz conjecture; the coalgebraic perspective used here is Kim’s.
    • It does not claim a “world-first” of any kind; the qualifier “within our observed range” is binding.

    Section 2. Background: collatzStep and the exit-layer numbers

    2.1 The standard Collatz step

    We work with the standard Collatz function in its Lean 4 form, as defined in CollatzRei.Basic:

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

    For an account of the conjecture and the substantial body of partial results, we refer to Lagarias (1985, 2010), Tao (2019), and the survey-style “Group Think” working paper by Kenigson (2025).

    2.2 The exit-layer numbers m_p

    The exit-layer numbers, as observed by the first author and formalized in STEP 1176, are defined recursively (avoiding division) in CollatzRei.ExitLayer:

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

    so that exitM 1 = 1, exitM 2 = 5, exitM 3 = 21, exitM 4 = 85, exitM 5 = 341, etc.

    The arithmetic core of STEP 1176 is the identity

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

    (3 m_p + 1 = 4^p), which is the reason that a single 3n + 1 step from m_p lands exactly on the power-of-two spine. The closed-form identification exitM p = (4^p − 1) / 3 is recorded as exitM_eq_div, the parity statement as exitM_odd, and the main exit-layer reach result as

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

    This is the mathematical source that the present paper lifts into coinductive language. STEP 1176 is verified sorry-free in Mathlib v4.27 and #print axioms exitM_reaches_one reports the axiom triple {propext, Classical.choice, Quot.sound} (the standard Mathlib base).

    2.3 Honest scope

    The exit-layer fragment formalized in STEP 1176, and lifted into coinductive language in the present paper, lies entirely on one side of the unresolved Collatz wall. It treats exactly the odd numbers that reach the power-of-two spine in a single 3n + 1 step. It does not characterize, in any non-trivial way, the predecessors of those numbers, and the trailing-1-bits ≥ 4 wall (Cases 5–8 in the trailingOnes / 2-adic-valuation framework articulated in STEP 622, Rei-AIOS) is wholly untouched.

    This is the only Collatz content of the present paper. Everything else is reformulation.

    Section 3. Coinductive reformulation: collatzHaltStep and the orbit Stream'

    3.1 Why halt at 1

    The standard Collatz step has the cycle 1 → 4 → 2 → 1, so 1 is not a fixed point of collatzStep. For coinductive purposes — where we wish to characterize “the orbit reaches and stays at 1” as “the orbit is eventually equal to the constant stream const 1” — we want 1 to be a genuine fixed point.

    We therefore introduce the halt-at-1 variant:

    def collatzHaltStep (n : Nat) : Nat :=
  if n = 1 then 1 else collatzStep n

    with two immediate lemmas:

    theorem collatzHaltStep_one : collatzHaltStep 1 = 1 := by
  unfold collatzHaltStep; simp

theorem collatzHaltStep_ne_one (n : Nat) (h : n ≠ 1) :
    collatzHaltStep n = collatzStep n := by
  unfold collatzHaltStep; simp [h]

    For every n ≠ 1, the two variants agree, so “reaches 1” statements transfer verbatim (Section 5). The single behavioural change is at n = 1, where collatzStep would have moved to 4 and collatzHaltStep stays at 1. This is a modelling choice in the spirit of unfolding partial fixed-point semantics into a total stream-coalgebra semantics; it is not a mathematical claim.

    3.2 The orbit as a Stream'

    We define the orbit of n as a Mathlib Stream' Nat:

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

    Concretely, the stream is

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

    The coinductive perspective is that the stream “reveals” the orbit one element at a time: each successive head is the next orbit value, and tail shifts the observer forward by one step.

    3.3 Honest scope

    The function collatzOrbit is a definitional reorganization of the existing iterated-function presentation. No new mathematical content is introduced here. The reformulation is purely linguistic — moving from Function.iterate (algebraic μF) to Stream' (coalgebraic νF), in the dictionary articulated in Adámek and Rosický (1994). It is the same dictionary that Kim (2008) uses when stating the 2-adic Collatz function as a morphism into a final bit-stream coalgebra; the contribution is the Lean 4 record of this dictionary applied to the exit-layer fragment, not the dictionary itself.

    Section 4. F-Coalgebra structure on collatzOrbit

    4.1 The functor

    We work with the functor F : Type → Type, F(X) = Nat × X, whose coalgebras X → F(X) are exactly streams of natural numbers presented as head plus tail. The Mathlib Stream' type is, in this language, the carrier of the final coalgebra for F (this is the standard coinductive characterization; cf. Niqui 2009 and the Mathlib Stream' documentation).

    4.2 Head

    The first projection is verified as

    theorem head_collatzOrbit (n : Nat) : head (collatzOrbit n) = n := rfl

    This proof reduces definitionally (rfl): Stream'.head s = s 0, and collatzOrbit n 0 = collatzHaltStep^[0] n = n definitionally. Empirically (Section 6), #print axioms head_collatzOrbit reports the empty set: this theorem depends on no axiom whatsoever, not even propext. It is in this sense strictly stronger than lawvere_fixed_point of Rei-AIOS STEP 1220, which depends on {propext, Classical.choice, Quot.sound}.

    4.3 Tail

    The shift relation is the characteristic F-coalgebra property:

    theorem tail_collatzOrbit (n : Nat) :
    tail (collatzOrbit n) = collatzOrbit (collatzHaltStep n) := by
  funext i
  show collatzHaltStep^[i + 1] n = collatzHaltStep^[i] (collatzHaltStep n)
  rw [Function.iterate_succ_apply]

    This is the statement that the assignment n ↦ collatzOrbit n is an F-coalgebra morphism: the diagram

       Nat   ──────────────collatzOrbit─────────────►  Stream' Nat
    │                                                   │
    │ ⟨id, collatzHaltStep⟩                             │ ⟨head, tail⟩
    ▼                                                   ▼
  Nat × Nat  ────────⟨id, collatzOrbit⟩──────────►  Nat × Stream' Nat

    commutes (with Mathlib.Stream' as the canonical final-coalgebra carrier on the right).

    4.4 Relation to Kim (2008)

    Kim (2008) constructs essentially the same diagram, working in the 2-adic integers ℤ_2 rather than in ℕ and at the level of pen-and-paper category theory. The present Lean 4 record differs in (i) the carrier (Nat, not ℤ_2); (ii) the proof assistant (Lean 4 / Mathlib v4.27, not pen-and-paper); (iii) the explicit axiom-base accounting (Section 6). It does not differ in mathematical idea.

    Section 5. Exit-layer bridge: lifting exitM_reaches_one into the coinductive language

    5.1 The fixed-after-1 lemmas

    Two preparatory lemmas record that once the halt step reaches 1, it stays there forever:

    theorem collatzHaltStep_iter_one (k : Nat) : collatzHaltStep^[k] 1 = 1 := by
  induction k with
  | zero      => rfl
  | succ m ih => rw [Function.iterate_succ_apply', ih, collatzHaltStep_one]

theorem collatzHaltStep_fixed_after_one (n k m : Nat)
    (h : collatzHaltStep^[k] n = 1) :
    collatzHaltStep^[k + m] n = 1 := by
  rw [show k + m = m + k from Nat.add_comm k m, Function.iterate_add_apply, h]
  exact collatzHaltStep_iter_one m

    5.2 The bridge from standard step to halt step

    The halt variant agrees with the standard step until 1 is reached, so the same step count works for both:

    theorem collatzHaltStep_reaches_one_of_collatzStep (n : Nat) :
    ∀ k, collatzStep^[k] n = 1 → collatzHaltStep^[k] n = 1 := by
  intro k h
  induction k generalizing n with
  | zero       => simpa using h
  | succ k' ih =>
    rw [Function.iterate_succ_apply] at h
    by_cases hn1 : n = 1
    · subst hn1; exact collatzHaltStep_iter_one (k' + 1)
    · rw [Function.iterate_succ_apply, collatzHaltStep_ne_one n hn1]
      exact ih (collatzStep n) h

    The case analysis is essential: if n = 1 at the start, the standard step would move to 4, but the halt step is already at the fixed point and stays there.

    5.3 The eventually-constant predicate

    We encode “eventually equal to a” as:

    def EventuallyConst (s : Stream' Nat) (a : Nat) : Prop :=
  ∃ k, ∀ j, k ≤ j → s j = a

    This is the standard coinductive characterization (witness k for the prefix length, all subsequent indices yield a). It is propositionally equivalent to “the stream is (prefix) ++ const a” but avoids appendix-construction machinery.

    5.4 The main bridge theorem

    The load-bearing theorem of the present paper is:

    theorem collatzOrbit_exitM_eventuallyConst (q : Nat) :
    EventuallyConst (collatzOrbit (exitM (q + 1))) 1 := by
  refine ⟨2 * (q + 1) + 1, ?_⟩
  intro j hj
  obtain ⟨m, hm⟩ : ∃ m, j = (2 * (q + 1) + 1) + m :=
    ⟨j - (2 * (q + 1) + 1), by omega⟩
  rw [hm]
  show collatzHaltStep^[2 * (q + 1) + 1 + m] (exitM (q + 1)) = 1
  apply collatzHaltStep_fixed_after_one
  apply collatzHaltStep_reaches_one_of_collatzStep
  exact exitM_reaches_one q

    The proof uses exitM_reaches_one (STEP 1176) directly as a hypothesis at the last line: the entire mathematical content of the theorem is the STEP 1176 result, and the present proof is a linguistic lift. There is no analytic content, no new descent argument, no new arithmetic.

    5.5 The constant-stream specialization at n = 1

    At the exit-layer base, the orbit collapses to the constant stream const 1:

    theorem collatzOrbit_one_eq_const : collatzOrbit 1 = const 1 := by
  funext i
  show collatzHaltStep^[i] 1 = 1
  exact collatzHaltStep_iter_one i

    and (exitM 1 = 1):

    theorem collatzOrbit_exitM_one_eq_const : collatzOrbit (exitM 1) = const 1 := by
  have h1 : exitM 1 = 1 := exitM_one
  rw [h1]
  exact collatzOrbit_one_eq_const

    Through Rei-AIOS STEP 1223’s IsCoalgebraicFixedPoint predicate, collatzOrbit 1 is in addition a (νF-style) coalgebraic fixed point of tail:

    theorem collatzOrbit_one_isCoalgebraicFixedPoint :
    IsCoalgebraicFixedPoint (collatzOrbit 1) := by
  rw [collatzOrbit_one_eq_const]
  exact const_isCoalgebraicFixedPoint 1

    This last theorem is recorded here for completeness; it asserts no Collatz content, only the structural fact that the constant stream is fixed by tail.

    5.6 Honest scope

    The bridge theorem is, by design, strictly weaker than the Collatz conjecture. It says: for the special inputs m_{q+1}, the orbit (in the halt variant) is eventually const 1. It does not say anything about n not of the form m_p, and the predecessor structure of the exit-layer numbers (which is where the unresolved Collatz wall lives) is not touched. The bridge is a coinductive restatement of a known elementary fact.

    Section 6. Zero-axiom witness and axiom-base accounting

    6.1 What “completely axiom-free” means

    A Lean 4 theorem T is completely axiom-free when #print axioms T reports the empty set. In particular, T does not depend on:

    • propext (propositional extensionality),
    • Classical.choice (the global choice principle),
    • Quot.sound (soundness of the quotient construction),

    nor on any user-introduced axiom declaration, nor on any reduction step that invokes native_decide (which appeals to compiled native code outside Lean’s kernel).

    Mathlib’s default axiom triple {propext, Classical.choice, Quot.sound} is the standard base used in classical mathematics; a completely axiom-free theorem is strictly below this base.

    6.2 head_collatzOrbit is completely axiom-free

    The theorem

    theorem head_collatzOrbit (n : Nat) : head (collatzOrbit n) = n := rfl

    is completely axiom-free: empirically, #print axioms head_collatzOrbit reports no axioms. The reason is that the proof is rfl: Stream'.head s unfolds definitionally to s 0, and collatzOrbit n 0 = collatzHaltStep^[0] n unfolds definitionally to n. No propositional reasoning is invoked, and the Lean 4 / Mathlib v4.27 implementation of Stream'.head is itself a non-classical projection.

    This places head_collatzOrbit strictly below the axiom base of lawvere_fixed_point (Rei-AIOS STEP 1220, 2026-06-15), which depends on {propext, Classical.choice, Quot.sound}. We record this not as a competition between theorems — they are unrelated — but as an instance of axiom-base minimization as a methodology.

    6.3 The axiom base of the remaining theorems

    The other principal theorems of the present development depend on a small set of axioms, summarized below. The ∅ (empty) entry for head_collatzOrbit was empirically confirmed by #print axioms head_collatzOrbit against Mathlib v4.27.0 in the Rei-AIOS session of 2026-06-16; the remaining entries record the expected base under the classical Mathlib lemmas used in each proof (funext, omega, Function.iterate_succ_apply, etc.). A per-theorem #print axioms re-verification of every row is scheduled for the Phase C cross-check, and any deviation will be recorded as a corrigendum before Phase D publication.

    Theorem Axiom base
    head_collatzOrbit ∅ (completely axiom-free)
    tail_collatzOrbit {propext, Classical.choice, Quot.sound}
    collatzHaltStep_iter_one {propext, Classical.choice, Quot.sound}
    collatzHaltStep_fixed_after_one {propext, Classical.choice, Quot.sound}
    collatzHaltStep_reaches_one_of_collatzStep {propext, Classical.choice, Quot.sound}
    collatzOrbit_one_eq_const {propext, Classical.choice, Quot.sound}
    collatzOrbit_one_isCoalgebraicFixedPoint {propext, Classical.choice, Quot.sound}
    collatzOrbit_exitM_eventuallyConst {propext, Classical.choice, Quot.sound}
    collatzOrbit_exitM_one_eq_const {propext, Classical.choice, Quot.sound}

    No theorem in the development depends on any user-introduced axiom, any sorry, or any native_decide. The classical triple is reached through Mathlib’s general-purpose lemmas (funext, Nat.add_comm, Function.iterate_succ_apply, etc.), not through any genuinely classical step in our argument; a fully constructive rewriting is plausible but is left to future work.

    6.4 Why this matters (and why it does not matter)

    Axiom-base minimization records a constructive content claim. A theorem at the empty axiom base is, in a precise sense, computable: its proof reduces to definitional unfolding only. A theorem at {propext, Classical.choice, Quot.sound} is classical-Mathlib-standard.

    The methodological value of recording these distinctions is that they make the constructive boundary explicit. The mathematical value here is modest: the empty-axiom-base witness head_collatzOrbit is a trivial projection, and the classical base of the main bridge theorem is the same as that of exitM_reaches_one itself. We claim no constructive Collatz result. We record axioms because we want a record, not because the axioms are themselves the content.

    This is consistent with the methodology line of the Rei-AIOS Paper 132 series (Mathlib contribution preparation, residual-sorry roadmaps), of which the present paper is a small entry.

    Section 7. Honest scope and explicit non-claims

    This section enumerates, in load-bearing form, what the present paper does not establish. It is the operational realization of the Rei-AIOS persistent rule feedback-evaluation-symmetry-principle: a result reported as “no prior art” or “axiom-free” must be reported with the same directness when the situation is the opposite. Reading this section as boilerplate is a misread; it constrains the paper’s interpretation.

    7.1 The Collatz conjecture is not resolved

    We do not prove ∀ n ≥ 1, Reaches1 n. We prove only that for inputs of the form m_{q+1} = (4^{q+1} − 1) / 3, the halt-variant orbit is eventually const 1. The complement — orbits starting from numbers not of the form m_p — is wholly untouched.

    7.2 The Cases 5–8 wall is unchanged

    The Rei-AIOS STEP 622 trailing-1-bits / 2-adic-valuation analysis identifies eight cases on the parity-class of n’s trailing binary expansion. Cases 1–4 admit explicit descent (step623_v3.lean); Cases 5–8, where trailing 1-bits are ≥ 4, exhibit an unbounded (3/2)^j growth contribution that defeats finite mod analysis. This wall is structurally unchanged by the present paper. Coinductive reformulation does not break finite-mod barriers.

    7.3 Tao (2019, 2022) is not superseded

    The “almost all” results of Tao (2019, 2022) are distributional statements about the density of orbits that come close to bounded values. They are the current analytic frontier. The present paper makes no statement about densities, makes no analytic argument, and does not move the boundary identified by Tao. We mention Tao’s results only for context, not as a benchmark we approach.

    7.4 Janik (2026) is independent

    Janik’s johnjanik/syracuse-confinement is a 12,947-line Lean 4 development with six remaining critical-path sorries, organized around an ergodic / Diophantine reduction on the (2,3)-torus. We have audited the public repository at file-name and code-search level and found zero occurrences of the search terms coalgebra, coinductive, Stream', exitM, and exit_layer; the two occurrences of 4^p are incidental (Baker-linear-form context). The present paper does not address any of Janik’s sorries, does not weaken his hypotheses, and is methodologically disjoint from his approach.

    7.5 No world-first claim is made

    In accordance with feedback-world-uniqueness-claim-controllable, we do not claim a “world-first” or “globally unique” Lean 4 axiom-free formalization of this material. The binding qualifier “within our observed range” applies to every existence claim in this paper. Kim (2008), Niqui (2009), the Coq coalgebras contribution, and the Cubical Agda final-coalgebra constructions are explicit prior art; the present paper is one record among several possible.

    7.6 No new attack vector is proposed

    We do not propose a new strategy for resolving the Collatz conjecture, and we do not assert that coinductive reformulation as such will lead to progress on the unresolved fragment. The Q2 Installment 1 survey (papers/collatz-rei-toolkit-survey-2026-06-16.md) predicted that the Rei toolkit applied to Collatz would produce a “null result plus a clean Lean 4 statement”; the present paper is precisely that, and nothing more.

    7.7 No siren-family framing is used

    In accordance with feedback-super-naming-siren-family-pattern, we avoid all framings of the form “beyond X”, “transcending X”, or “going past X”. The translation discipline make / measure / map (build a tool, measure existing reach, map inaccessible territory) is operative throughout: this paper makes one tool (the coinductive lift), measures the axiom-base of nine theorems, and maps the boundary between the exit-layer fragment and the Cases 5–8 wall. It does not claim to transcend anything.

    7.8 Mathlib API stability is conditional

    The development depends on Mathlib v4.27.0’s Stream'.head, Stream'.tail, Function.iterate_succ_apply, Nat.add_comm, and related lemmas. We do not claim that the development will continue to typecheck after Mathlib API changes; such drift is a routine maintenance matter for Lean 4 formalizations.

    Section 8. Related work

    8.1 Coalgebraic Collatz (prior art)

    • Kim, J. (2008). Coinductive properties of Lipschitz functions on streams. The 2-adic Collatz function is a morphism into a final bit-stream coalgebra; the coalgebraic structure on Collatz dynamics is articulated here, in pen-and-paper category theory. This is the primary prior art for the present paper.
    • Related: the body of subsequent work treating 2-adic Collatz as a final stream coalgebra in coalgebraic logic and stream automata theory.

    8.2 Stream coalgebra formalization (prior art)

    • Niqui, M. (2009). Coalgebraic Reasoning in Coq. Stream coalgebras, weakly final coalgebras, λ-coiteration, and bisimulation formalized in Coq. This is the canonical reference for formalized coalgebraic reasoning in a proof assistant.
    • The Coq coalgebras contribution (GitHub, 2008–2009). Open-source library covering coalgebra, bisimulation, weakly final coalgebra, λ-coiteration with stream coalgebra examples.
    • Cubical Agda final-coalgebra constructions in the standard library.
    • Adámek, J., Rosický, J. (1994). Locally Presentable and Accessible Categories. The μF / νF dictionary (initial-algebra / final-coalgebra duality) used throughout the present paper.

    8.3 The analytic Collatz frontier (context only)

    • Tao, T. (2019). Almost all orbits of the Collatz map attain almost bounded values. arXiv:1909.03562.
    • Tao, T. (2022). Follow-up extension paper [exact arXiv identifier to be confirmed at Phase C].
    • Janik, J. (2026). Diophantine Confinement in Syracuse Dynamics: A Formal Reduction. GitHub: johnjanik/syracuse-confinement. 12,947 lines of Lean 4 with six remaining critical-path sorries.
    • Chang, F. (2026, April). Stanford preprint v5 with the “Sturmian obstruction” and the “Carry Contamination Theorem”.
    • Knight, K. (2026, March). Collatz high cycles do not exist. Discrete Mathematics.
    • Kenigson, J. (2025, December). Group Think: A Survey on the Collatz Conjecture. Working paper, Cambridge Open Engage.

    8.4 Classical Collatz references

    • Collatz, L. (1937). Unpublished. Cited as the origin of the 3n+1 problem.
    • Conway, J. H. (1972). Unpredictable Iterations. Proceedings of the Number Theory Conference, University of Colorado, Boulder. Generalized Collatz functions are Turing-complete; the original Collatz function is not known to be decidable.
    • Lagarias, J. C. (1985). The 3x+1 problem and its generalizations. American Mathematical Monthly, 92(1), 3–23.
    • Lagarias, J. C. (ed.) (2010). The Ultimate Challenge: The 3x+1 Problem. American Mathematical Society.

    8.5 Rei-AIOS internal lineage

    The present paper is part of the Rei-AIOS Paper series. The relevant internal references are:

    • STEP 1176 (Fujimoto, 2026-05-28). Exit-layer formalization. data/lean4-mathlib/CollatzRei/ExitLayer.lean. The mathematical source of the present paper.
    • STEP 1177 (Fujimoto, 2026-05-28). Inverse Collatz tree visualization (TypeScript lens). Not Lean 4; included for context.
    • STEP 1178 (Fujimoto, 2026-05-28). Collatz frontier dossier (TypeScript). Six routes catalog with breakdown points. Not Lean 4.
    • STEP 1179 (Fujimoto, 2026-05-28). Exit-layer inverse formulas, added to ExitLayer.lean.
    • STEP 1220 (Fujimoto and Claude Opus, 2026-06-15). Cantor-Lawvere fixed-point formalization, Lean 4 axiom-free. LawvereFixedPointExperiment.lean. Provides the axiom-base benchmark against which Section 6 is compared.
    • STEP 1223 (Fujimoto and Claude Opus, 2026-06-16). IsCoalgebraicFixedPoint predicate and const_isCoalgebraicFixedPoint lemma. NuFStreamSelfLoop.lean. The coinductive fixed-point tool used in Section 5.5.
    • Q2 Installment 1 (Fujimoto and Claude Opus, 2026-06-16). Collatz × Rei Toolkit Survey. papers/collatz-rei-toolkit-survey-2026-06-16.md. Articulates the Rei toolkit, identifies the present paper’s content as one of two candidate installments, and pre-registers the “null result + clean Lean 4 statement” prediction.
    • Q2 Installment 2A (Fujimoto and Claude Opus, 2026-06-16). StreamExitLayerBridge.lean. The primary source file of the present paper.
    • Paper 132 series methodology notes (Rei-AIOS, 2026). Style template for the present paper; the methodology-note format with axiom-base accounting is inherited from this series.

    Section 9. Limitations and future work

    9.1 Limitations

    The present paper has the following intrinsic limitations:

    1. Fragment, not full conjecture. The result covers exactly the exit-layer numbers m_p, which is one branch in the inverse Collatz tree. The full Collatz conjecture is the question of whether the inverse-tree branches cover all positive integers; this paper is silent on that question.
    2. Routine application of a known dictionary. The coalgebraic perspective on Collatz dynamics is Kim’s (2008), the stream-coalgebra formalization machinery is Niqui’s (2009) and the Coq coalgebras contribution’s (2008–2009). The present paper is a Lean 4 record of routinely applying the latter to the former on a fragment of the former; it is methodological in character.
    3. Mathlib v4.27 specificity. API drift in future Mathlib releases is expected; the development is maintained under the dual-license terms of the Rei-AIOS repository but no long-term maintenance guarantee is offered with the publication.
    4. Modest axiom-base record. The only completely axiom-free theorem in the development (head_collatzOrbit) is a definitional projection. The methodologically interesting axiom-base reductions on substantive theorems remain open.

    9.2 Future work

    The present paper is one of three threads in a broader Rei-AIOS reframing of the Collatz program, articulated in the persistent memory note project-three-track-reframe-perelman-coalgebra-post-audit-2026-06-16. The other two threads are:

    • (A) A second monotone quantity along the lines of Perelman’s W-functional. Rei-AIOS STEP 1176’s exit-layer formalization is paired in the Rei series with the F-entropy / trailingOnes monotonicity of Paper 58. A scoping document of 2026-06-17 (papers/collatz-second-monotone-quantity-scoping-2026-06-17.md) identifies three candidates — a carry-structure quantity, a 2-adic-roughness quantity built on Mathlib’s padicValNat, and an LZ-complexity quantity from Rei STEP 1168 — and recommends the 2-adic-roughness candidate on the grounds of minimum implementation cost and natural compatibility with the existing F-entropy infrastructure. Lean 4 implementation of this candidate is gated on publication of the present paper and explicit approval from the first author; we do not include it in the present paper, to preserve a narrow scope.
    • (B) A categorical / Yoneda-style reformulation of Shannon entropy in the spirit of Baez. This is long-term and outside the present paper’s scope.

    A separate, longer-term thread is the visualization of the non-computability hierarchy (oracle hierarchies, ITTM, BSS, Type-2 machines) as an educational demonstration alongside the coinductive content. This is mentioned in the Q2 Installment 1 survey but is not pursued in the present paper.

    9.3 The present paper’s position in the program

    We close by stating the present paper’s position with directness. It is a methodological record, not a mathematical advance. It documents one Lean 4 axiom-free formalization, with one completely axiom-free witness theorem, of one classical fragment of the Collatz dynamics, in the language of a coalgebraic perspective that was articulated in pen-and-paper category theory by Kim in 2008. Its appropriate venue is the short-note line of the Rei-AIOS Paper 132 series, with an expected impact comparable to a CPP / ITP short-note formalization record. We do not expect it to be cited in analytic Collatz literature. We do expect it to be cited, if at all, as one of several records of stream-coalgebra formalization in proof assistants, alongside Niqui (2009) and the Coq coalgebras and Cubical Agda libraries.

    This is the honest scope of the contribution.

    References

    Primary citations

    1. Kim, J. (2008). Coinductive properties of Lipschitz functions on streams. [Exact venue to be confirmed at Phase C — Springer / arXiv reference to be inserted.]
    2. Niqui, M. (2009). Coalgebraic Reasoning in Coq. [Exact venue to be confirmed at Phase C.]
    3. The Coq coalgebras contribution. GitHub repository (2008–2009). [URL to be inserted at Phase C.]
    4. Adámek, J., Rosický, J. (1994). Locally Presentable and Accessible Categories. Cambridge University Press.
    5. Tao, T. (2019). Almost all orbits of the Collatz map attain almost bounded values. arXiv:1909.03562.
    6. Tao, T. (2022). Follow-up extension paper. [Exact arXiv identifier to be confirmed at Phase C.]
    7. Janik, J. (2026). Diophantine Confinement in Syracuse Dynamics: A Formal Reduction. GitHub: johnjanik/syracuse-confinement.
    8. Chang, F. (2026, April). Stanford preprint v5. [Exact title and arXiv identifier to be confirmed at Phase C.]
    9. Knight, K. (2026, March). Collatz high cycles do not exist. Discrete Mathematics.
    10. Conway, J. H. (1972). Unpredictable Iterations. In: Proceedings of the Number Theory Conference, University of Colorado, Boulder.
    11. Lagarias, J. C. (1985). The 3x+1 problem and its generalizations. American Mathematical Monthly, 92(1), 3–23.
    12. Lagarias, J. C. (ed.) (2010). The Ultimate Challenge: The 3x+1 Problem. American Mathematical Society.

    Internal Rei-AIOS references

    1. Fujimoto, N. (2026-05-28). Rei-AIOS STEP 1176: Collatz exit-layer formalization. data/lean4-mathlib/CollatzRei/ExitLayer.lean.
    2. Fujimoto, N. (2026-05-28). Rei-AIOS STEP 1177: Inverse Collatz tree lens. TypeScript visualization; not Lean 4.
    3. Fujimoto, N. (2026-05-28). Rei-AIOS STEP 1178: Collatz frontier dossier. TypeScript; not Lean 4.
    4. Fujimoto, N. (2026-05-28). Rei-AIOS STEP 1179: Exit-layer inverse formulas. Added to ExitLayer.lean.
    5. Fujimoto, N., Claude Opus (2026-06-15). Rei-AIOS STEP 1220: Lawvere fixed-point experiment. LawvereFixedPointExperiment.lean.
    6. Fujimoto, N., Claude Opus (2026-06-16). Rei-AIOS STEP 1223: νF Stream’ self-loop. NuFStreamSelfLoop.lean.
    7. Fujimoto, N., Claude Opus (2026-06-16). Collatz × Rei toolkit survey. papers/collatz-rei-toolkit-survey-2026-06-16.md.
    8. Fujimoto, N., Claude Opus (2026-06-16). StreamExitLayerBridge.lean (the source file of the present paper).
    9. Fujimoto, N. (2026). Rei-AIOS Paper 132 series. Methodology-note template. [Exact entries to be confirmed at Phase C.]

    Supplementary

    1. Mathlib v4.27.0. Stream'.head, Stream'.tail, Function.iterate_succ_apply, Function.iterate_succ_apply', Function.iterate_add_apply. Reference: https://github.com/leanprover-community/mathlib4.
    2. Kenigson, J. (2025, December). Group Think: A Survey on the Collatz Conjecture. Working paper, Cambridge Open Engage.

    Honest scope footer

    ─────────────────────────────────────────────────────
HONEST SCOPE FOOTER (load-bearing,
 feedback-evaluation-symmetry-principle +
 feedback-world-uniqueness-claim-controllable +
 feedback-super-naming-siren-family-pattern)
─────────────────────────────────────────────────────

What this paper formalizes:
  ✓ The exit-layer fragment m_p = (4^p − 1) / 3 of the Collatz
    dynamics, lifted from the algebraic μF iteration presentation
    (STEP 1176) into the coalgebraic νF Stream' presentation.
  ✓ One completely axiom-free witness theorem
    (head_collatzOrbit), with `#print axioms` empty.
  ✓ One main bridge theorem
    (collatzOrbit_exitM_eventuallyConst), at the classical
    Mathlib axiom triple {propext, Classical.choice, Quot.sound}.
  ✓ One Lean 4 / Mathlib v4.27 record of applying the
    known coalgebraic Collatz perspective (Kim 2008) to a
    known elementary Collatz fragment.

What this paper does NOT formalize:
  ✗ The Collatz conjecture (∀ n ≥ 1, Reaches1 n).
  ✗ The Cases 5–8 trailing-1-bits ≥ 4 wall
    (structurally unresolved).
  ✗ Any improvement over Tao 2019 / 2022 "almost all"
    distributional results.
  ✗ Any discharge of Janik 2026's six critical-path sorries.
  ✗ Any "new attack vector" or "world-first" or
    "Tao-superseded" or "Collatz-resolved" framing.

Our position:
  - A Paper 132 series methodology contribution,
    CPP / ITP short note in expected impact.
  - One operational instance of axiom-base minimization.
  - One record added to the Rei-AIOS Paper lineage,
    of limited contribution.
  - The qualifier "within our observed range" applies
    to every existence claim in this paper.
─────────────────────────────────────────────────────

    Phase B 起草完了 status (2026-06-17 朝)

    ✓ Title #1 採用 (Skeleton 通り) ✓ Abstract で Kim 2008 + Niqui を front-load ✓ Section 1 で限定 contribution + what this paper is not 両方明示 ✓ Section 6 で head_collatzOrbit 完全 zero-axiom claim + Lawvere 比較 ✓ Section 7 で 8 項目 honest scope (Skeleton 7 項目 + Mathlib API stability 1 件追加) ✓ Section 8 で Kim 2008 + Niqui + Coq contrib + Cubical Agda + Janik + Tao + Chang + Knight + Conway + Lagarias + STEP lineage 全件引用 ✓ 「世界初」「Tao 超え」「新 attack vector」「Collatz 解決」 等の siren framing 不使用 ✓ Section 9 で 三方針 reframe + stop criterion future-work 文脈 明記 ✓ Mathlib v4.27.0 specific API dependency 明記 (Section 7.8 + Section 6.3) ✓ rei-aios.pages.dev + note.com footer (front matter) ✓ AGPL-3.0 + Commercial dual license 標記 ✓ Paper 132 系 short note style (15 page 級、 over-engineering なし)

    Next: Phase C handoff items (chat-Claude cross-check, 1-day buffer 推奨)

    1. Pattern 1-6 hallucination audit (出典・年代・author 名・引用 venue 全件)
    2. Overclaim detection — 「siren framing」「世界初」「Tao 超え」「Cases 5-8 突破」 系の言い換えが残っていないか
    3. Honest scope sufficiency check — Section 7 8 項目で漏れがないか (特に Cases 5-8 wall + Janik 独立性 + Mathlib API 条件性)
    4. Empirical axiom-base re-verification — Section 6.3 表 9 行を lake env lean で per-theorem #print axioms で再確認 (Phase D publish 前必須、 deviation あれば corrigendum 起草)
    5. Reference完全形 — Kim 2008 + Niqui 2009 + Tao 2022 + Chang 2026 + Coq coalgebras contrib + Paper 132 系の exact venue / arXiv ID / URL 確定 (現在 placeholder)
    6. Page count ≤ 15 確認 (現状 ~12 page 推定)

    Phase D (publish 計画): Phase C pass 後、 Zenodo DOI 取得 + 11 platform standard (Dev.to / Hatena / HackMD / Notion / Livedoor / Mastodon / Scrapbox / Nostr / Internet Archive / GitHub Release)、 Harvard Dataverse は per-paper opt-in 確認 ([[feedback-harvard-dataverse-opt-in]] 準拠)。 急がず ゆっくりと ([[feedback-no-rush-publication]])。

    #math #desci #rei-aios #collatz
    Write a comment