DEV Community

Nobuki Fujimoto
Nobuki Fujimoto

Posted on

Paper 158 v0.2 — The Collatz Exit Layer: Zero-Sorry Lean 4 Formalization of m_p = (4^p 1)/3, and an Honest Map of the Seven-Route Wall Beyond

#math #ai #research #lean

This article is a re-publication of Rei-AIOS Paper 158 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:

A Zero-Sorry Lean 4 Formalization of m_p = (4^p − 1)/3, and an Honest Map of the Seven-Route Wall Beyond

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

Status: v0.1 (PUBLISHED — Zenodo + IA)
Date drafted: 2026-05-29 (v0.0); promoted to v0.1 and published the same day.
Zenodo DOI: 10.5281/zenodo.20435288 (deposit 20435288, finalized 2026-05-29, IMMUTABLE).
Internet Archive: https://archive.org/details/rei-aios-paper-158-1780003374000
Pinned artifacts: data/lean4-mathlib/CollatzRei/ExitLayer.lean @ Rei-AIOS commit 372321c1c7001680424749fc4d11043062e4f024 (STEP 1179, "inverse of the exit-layer formula, formalized in Lean (zero-sorry)"). Mathlib v4.27.0 @ commit a3a10db0e9d66acbebf76c5e6a135066525ac900. Lean toolchain leanprover/lean4:v4.27.0.
v0.1 acceptance items (all cleared): (a) ★ Consent from ラーメン好きさん received (confirmed 2026-05-29 by N. Fujimoto); (b) §6 frontier route table audited 2026-05-28 (Janik / Tao / Baker / Conway); (c) ★ #print axioms verbatim output captured 2026-05-29 and pasted in Appendix A.1; (d) Rei-AIOS commit hash pinned (above); (e) Mathlib commit hash pinned (above); (f) Zenodo + IA publish complete (Harvard skipped per opt-in policy); (g) bilingual EN/JA pair deferred to v0.2 (optional).

Authors

  • Nobuki Fujimoto (藤本 伸樹) — Independent researcher (formerly FX), Japan. ORCID: TBD. (Conceptualization, Lean 4 formalization, manuscript)
  • Claude Opus 4.7 (Anthropic) — AI collaborator. (Lean 4 mechanization assistance, manuscript drafting)
  • No academic affiliation is claimed for any author. The independent-researcher framing is load-bearing and honest (Cardano/Thorp 型: 賭け/市場 → 数学).

Honest non-claims (load-bearing, must remain at the very top)

This paper does NOT claim:

  1. A proof of the Collatz conjecture (3x+1).
  2. A new mathematical theorem about the inverse Collatz tree's coverage of ℕ.
  3. Novelty of the observation m_p = (4^p − 1)/3 (= 1, 5, 21, 85, 341, …). This sequence is well known in the Collatz literature (Lagarias 1985 and the surrounding Jacobsthal-Collatz papers).
  4. Novelty of the seven candidate routes (Janik confinement, Tao 2019, 2-adic Hensel, Baker linear forms, automata/parity, inverse-tree/Jacobsthal, undecidability) — all are pre-existing.
  5. That a route ever becomes "open" because we formalised one layer.

This paper DOES claim, on the record:

(C1) A clean, zero-sorry Lean 4 formalization of the exit-layer family exitM p := (4^p − 1)/3 (recursively exitM 0 = 0, exitM (p+1) = 1 + 4·exitM p), including the key identity 3·m_p + 1 = 4^p, oddness for p ≥ 1, one-step landing on a power of two, and (★) the main theorem exitM_reaches_one_of_pos: ∀ p ≥ 1, the Collatz orbit of m_p reaches 1 in exactly 2p + 1 steps. Verified by lake env lean (exit 0) with #print axioms showing only the three standard Lean foundations (propext, Classical.choice, Quot.sound) — no sorryAx and no native_decide for the main theorem chain (Appendix A).

(C2) A small inverse calculus inside the exit layer (Lean 4 zero-sorry): the inverse recurrence exitM_pred : m_p = (m_{p+1} − 1)/4, the uniqueness inversion exitM_of_eq : 3m + 1 = 4^p ⟹ m = m_p, and the p-recovery exitM_recover_p : Nat.log 2 (3·m_p + 1) = 2p.

(C3) A curated frontier map of seven candidate reduction routes (Table 1), each annotated with what is proven, where the arrow breaks (honest gap), and a Mathlib v4.27.0 coverage assessment from a grep audit performed 2026-05-28. The map is a suggester, not a new arrow.

(C4) An honest negative-result framing: completely formalising the exit layer makes the wall more visible, not lower. Difficulty conservation (à la Janik) is the load-bearing meta-claim.

Provenance and attribution

The observation that the integer solutions of 3m + 1 = 2^n occur only when n is even (because 2^n ≡ (−1)^n mod 3), and that the resulting odd integers form the family m_p = (4^p − 1)/3 = 1, 5, 21, 85, 341, …, was communicated to N. Fujimoto by ラーメン好き (Ramen-suki, pen name; profile self-description: "豆腐のようなメンタルで、数字を数えています") in a note.com article at https://note.com/yaminotikara . Although the closed form (4^p − 1)/3 is implicit in classical Collatz references (e.g., Lagarias 1985, AMM 92), this paper's choice of route, framing, and Lean 4 formalisation directly follow ラーメン好き's note exposition, and that origin is recorded here on the record. ラーメン好き has been informed prior to drafting and has consented to citation and acknowledgment under that pen name and that URL.

We emphasise: the result that m_p reaches 1 in 2p + 1 Collatz steps is not novel mathematics. What this paper contributes is the machine-checkable Lean 4 record, the inverse calculus inside the exit layer, and the honest frontier map.

1 Introduction

The Collatz conjecture asserts that the iteration T(n) = n/2 (n even), T(n) = 3n+1 (n odd) eventually reaches 1 for every positive integer n. Despite eighty years of attention it remains open, and Erdős's remark that "mathematics is not yet ready for such problems" continues to apply.

This paper is not an attempt to settle Collatz. It is a deliberate exercise in honest negative-progress: we take a tractable observation — the "exit layer" m_p = (4^p − 1)/3, the odd numbers that hit the dyadic spine 2^(2p) after a single 3x+1 step — and we completely formalise the orbit-to-1 statement for this family in Lean 4, with zero sorry and minimal axioms. We then deliberately ask: does this formalisation lower any wall that stops a proof of Collatz? We answer, route by route, no. We exhibit seven candidate reduction routes (a curated subset of Lagarias's annotated bibliography updated with 2019–2026 advances), and we mark, for each, exactly where its arrow breaks. The result is a map of the wall, not a passage through it.

We believe this kind of paper is worth writing: it converts a temptation ("a nice closed-form family — surely this gives a foothold!") into a small, verifiable, and disprovable-by-running-the-Lean artifact, plus a public record of the difficulty conservation that surrounds it.

1.1 What we measured, in one line

Of the seven routes catalogued in §6, seven retain their breakdown point unchanged after our formalisation. The exit-layer Lean module reduces zero of them. This is the result.

1.2 Roadmap

§2 fixes notation. §3 states and proves the exit-layer theorem in Lean 4 (skeleton; full source in Appendix A). §4 develops the small inverse calculus inside the exit layer and explains why "inverse closed form on one branch" is not the inverse Collatz reduction. §5 visualises the bottom layers of the inverse Collatz tree (STEP 1177) and explains, again, why this is the wrong side of the wall. §6 is the frontier table. §7 discusses Mathlib coverage. §8 is the honest negative-result framing. §9 is acknowledgments. Appendices give full Lean source, #print axioms, the inverse-tree generator (STEP 1177), and the frontier-map JSON (STEP 1178).

2 Notation

collatzStep : ℕ → ℕ is defined (in CollatzRei.Basic) by collatzStep n = n/2 when n is even and collatzStep n = 3n + 1 when n is odd. collatzStep^[k] is k-fold iteration. Reaches1 n is ∃ k, collatzStep^[k] n = 1. We do not use the compressed map T(n) = (3n+1)/2 in the main statement, because the elementary one-step landing 3m + 1 = 4^p is cleanest in the uncompressed form.

The exit layer is exitM : ℕ → ℕ, exitM 0 = 0, exitM (p+1) = 1 + 4 · exitM p. By induction, exitM p = (4^p − 1)/3 = 1 + 4 + 4² + … + 4^(p−1).

3 The exit-layer theorem in Lean 4

3.1 Core identity

Lemma 3.1 (three_mul_exitM_add_one). For every p ∈ ℕ, 3 · exitM p + 1 = 4^p.

Proof (Lean 4 sketch). Induction on p. Base: trivial by simp [exitM]. Step: rewrite 3 · exitM (q+1) + 1 = 4 · (3 · exitM q + 1) (algebra), use the IH and pow_succ. Closes by ring.

3.2 Closed-form coincidence

Lemma 3.2 (exitM_eq_div). exitM p = (4^p − 1)/3.

Proof. Immediate from Lemma 3.1 and omega.

3.3 Oddness and one-step landing

Lemma 3.3 (exitM_odd). For every q ∈ ℕ, exitM (q + 1) ≡ 1 (mod 2).

Lemma 3.4 (collatzStep_exitM). For every q ∈ ℕ, collatzStep (exitM (q + 1)) = 4^(q+1).

Proof. By Lemma 3.3, exitM (q+1) is odd, so the collatz step takes the 3x+1 branch. The result is then Lemma 3.1 evaluated at (q+1).

3.4 Dyadic spine

Lemma 3.5 (pow2_reaches_one). For every j ∈ ℕ, collatzStep^[j] (2^j) = 1.

Proof. Induction on j, using collatzStep_pow2 : collatzStep (2^(j+1)) = 2^j.

3.5 Main theorem

Theorem 3.6 (exitM_reaches_one). For every q ∈ ℕ, collatzStep^[2(q+1) + 1] (exitM (q+1)) = 1.

Proof. One step lands on 4^(q+1) = 2^(2(q+1)) (Lemma 3.4 + four_pow_eq); then 2(q+1) further steps halve to 1 (Lemma 3.5).

Corollary 3.7 (exitM_reaches_one_of_pos). For every p ≥ 1, Reaches1 (exitM p). ∎

3.6 Axiom audit

#print axioms over all six load-bearing theorems was run with lake env lean and reports only the three standard Lean 4 foundations: propext, Classical.choice, Quot.sound. The inverse recurrence exitM_pred (proved by omega) is cleaner still, depending only on [propext, Quot.sound]. There is no sorryAx and no Lean.ofReduceBool (the axiom underlying native_decide) in the main theorem chain. The two concrete numerical examples (five_reaches_one, twentyone_reaches_one) do use native_decide and are decorations, not part of the load-bearing claim. The verbatim output captured 2026-05-29 is reproduced in Appendix A.1.

The complete Lean 4 source is reproduced in Appendix A and tracked at data/lean4-mathlib/CollatzRei/ExitLayer.lean in the Rei-AIOS repository (commit hash to be pinned at v0.1 freeze).

4 The inverse calculus inside the exit layer (and why this is not the inverse Collatz reduction)

The exit-layer satisfies a clean forward recurrence exitM (p+1) = 1 + 4 · exitM p and therefore a clean inverse recurrence:

Lemma 4.1 (exitM_pred). exitM p = (exitM (p+1) − 1)/4.

Lemma 4.2 (exitM_of_eq, uniqueness inversion). If 3m + 1 = 4^p then m = exitM p.

Lemma 4.3 (exitM_recover_p). Nat.log 2 (3 · exitM p + 1) = 2p (i.e. p = ½ · log₂(3m + 1)).

These give a tight algebraic story on one branch of the inverse tree: given a member of the exit layer, we can run forward, run backward, and recover its index in closed form. None of this addresses the inverse Collatz problem in general, because the global rung-to-rung+1 question for Collatz is "does the inverse tree cover all of ℕ?", and the inverse calculus above only tracks the spine 1 → 5 → 21 → 85 → … of one branch. The branch is exact; the tree is the open question.

We labour this point because conflating "I inverted a closed form on one branch" with "I inverted Collatz" is the standard failure mode of inverse-tree approaches (see §6, route 6).

5 The bottom layers of the inverse Collatz tree

The compressed odd-to-odd Collatz map T_odd(n) = (3n + 1)/2^v(3n+1) has an inverse: the predecessors of an odd n are exactly the positive odd integers of the form (n · 2^k − 1)/3 for k ≥ 1 satisfying the parity-divisibility condition. STEP 1177 computes this BFS for k=1..5 from root 1 and produces a 46-node tree across the first five layers (sizes 1, 3, 6, 12, 24).

The exit-layer family (4^p − 1)/3 is exactly the k = 1 branch from the root, i.e. the spine 1 → 5 → 21 → 85 → 341 → …. Predecessors with k ≥ 2 fan out into the rest of the tree (e.g. pred(5) = {3, 13, 53, 213, …}). Multiples of 3 are true leaves of the inverse tree, because 3n + 1 ≢ 0 (mod 3), so they cannot appear as images of T_odd; this is well known.

We include the visualisation here only to make precise what we are not doing: we are mapping the bottom of the tree, not climbing it. The question whether BFS from 1 eventually enumerates every positive odd number is Collatz itself.

6 Frontier map: seven candidate reduction routes

We organise the candidate routes as: state the proposed arrow ("if you prove X then Collatz drops out"), state what is actually proven, state where the arrow breaks (the honest gap), and state Mathlib v4.27.0 coverage from a 2026-05-28 grep audit.

The decomposition we use throughout: Collatz ⟺ (A) no divergent orbit ∧ (B) no nontrivial cycle. Equivalently: the inverse tree covers ℕ.

Table 1 — Seven routes and their break points

# Route (theory) Strongest established ★ Where the arrow breaks (honest) Mathlib v4.27.0
1 Janik syracuse-confinement (Diophantine confinement, Lean-mechanised) Collatz reduced by machine-checked Lean (≈13 k lines) to a single Diophantine confinement condition combining three forces: Hensel/2-adic, Baker/Archimedean, Denjoy–Koksma/ergodic ★ The confinement condition itself is not proved. The reduction is real; the assumption it reduces to is still open (sorry-equivalent in the formal record). This is the state of the art as of 2026, and it is honest about the gap. Reduction structure formalised; confinement assumption open.
2 Tao 2019 (ergodic / log-density) For any f → ∞, Col_min(N) ≤ f(N) for almost all N (log density). Improves Korec's θ > log 3 / log 4 ≈ 0.792. ★ almost all ≠ all. A measure-zero exceptional set is permitted; no non-probabilistic, structural device removes it. Dynamics/Ergodic basics present; the Syracuse-random apparatus of Tao 2019 is not in Mathlib.
3 2-adic conjugacy / Hensel Collatz is conjugate on ℤ₂ to the shift; parity vectors are uniformly distributed on ℤ₂. ★ ℤ₂ measure-theoretic statements do not transfer to per-n statements on ℤ. Same a.e./all wall in 2-adic clothing. ✓ NumberTheory/Padics/{PadicNumbers,PadicIntegers,Hensel}, RingTheory/Henselian. Formalisable when the mathematics arrives.
4 Baker / linear forms in logarithms (cycle exclusion) Baker shows nontrivial cycles, if any, must be astronomically large; Simons–de Weger eliminate small m-cycles. ★ Only finitely many cycle lengths excluded. No bound applies to all cycle lengths simultaneously. ✗ Baker's theorem / linear forms in logarithms are not in Mathlib (grep hits 0; transcendence is limited to Lindemann + Liouville). Formalising Baker is a major project in its own right.
5 Automata / formal languages (parity sequences) Structural descriptions of parity vectors (Terras 1976); regular-language presentations of compressed maps. ★ No descent certificate. Structural description does not yield "decreases for every n". Partial; furthermore, there is no theorem statement currently available to formalise.
6 Inverse Collatz tree / Jacobsthal (this paper's neighbourhood) Exit layer (4^p − 1)/3 → 1 in 2p+1 steps formalised in Lean 4 (this paper). Tree structure (mod-3 leaves; k parity) known since Lagarias 1985. ★ Tree coverage of ℕ = Collatz. Iterating BFS only enumerates finitely many bottom layers; coverage cannot be bootstrapped from local structure. ✓ Exit layer formalised (this paper). The coverage statement is exactly the sorry. Large-n checks hit the native_decide computational wall.
7 Undecidability / ZFC-independence (meta, after Conway 1972) Conway 1972 (Unpredictable Iterations): generalised 3x+1-style maps are Turing-complete, hence undecidable as a class. FRACTRAN (1987). ★ Independence of the specific 3x+1 problem is itself open. Informally Collatz is Π₂; a cycle is Σ₁ (refutable); divergence is Π₂. No actual independence proof exists. — Meta-level; not expressible inside Lean as an object-level theorem about Collatz.

The leading route in 2026 is Route 1 (Janik). The strongest unconditional result is Route 2 (Tao). The exit-layer paper sits inside Route 6 and does not move the break point of any route.

6.1 Common wall

Every route ultimately fails at the same place: there is no proven invariant that decreases on every n, and no reformulation into a solved deep theory has materialised. This is what Erdős's "not ready" remark really points at.

7 Mathlib coverage and the wall's location

The grep audit (Mathlib v4.27.0 commit a3a10db0, 2026-05-28) supports a sharper statement of the wall:

The wall is not in Lean's expressive power. It is in (a) what Mathlib has currently absorbed (2-adic/Hensel ✓; Baker ✗; Tao 2019 random ✗) and (b) the underlying mathematics being absent. Lean can locate the wall precisely (write the missing lemma as a sorry); it cannot lower it. Janik's 13 k-line reduction empirically demonstrates this: it converts the wall from many small walls into one large wall, but the height is conserved.

This is the "difficulty conservation" meta-claim. We do not prove it formally; we observe it from Janik's evidence and from the seven-route table.

8 Honest negative result

We deliberately wrote a paper whose central announcement is no progress. The reasons:

  1. It is true. Inflating elementary results into "approaches to Collatz" wastes the literature's attention. We have an exact closed-form family with a complete Lean proof; we also have seven walls we did not cross. Saying both is honest.
  2. The Lean record is durable. Formal verification turns a folklore observation into an artifact that any third party can re-run. We use this artifact only to claim what it actually proves.
  3. The map of the wall has its own utility. Future workers can use the route table to avoid revisiting routes already known to be blocked at the same point. Negative knowledge is knowledge.

The paper's title contains the words zero-sorry and honest map because both are accurate and both are load-bearing.

9 Acknowledgments

We thank ラーメン好き (note URL: https://note.com/yaminotikara ) for the exposition that initiated this work. The exit-layer observation — that 3m + 1 = 2^n has integer solutions only when n is even, and that the resulting odd integers form the family m_p = (4^p − 1)/3 = 1, 5, 21, 85, 341, … — was relayed to N. Fujimoto via ラーメン好き's note article. ラーメン好き has explicitly consented (confirmed 2026-05-29) to citation and acknowledgment under the pen name "ラーメン好き" and the URL https://note.com/yaminotikara as it appears in this paper. We thank them for the generous correspondence and for permission to use their name here. Profile self-description: 「豆腐のようなメンタルで、数字を数えています」.

We emphasise — and we believe ラーメン好き would emphasise the same point — that the closed form (4^p − 1)/3 and the corresponding spine of the inverse Collatz tree are implicit in classical Collatz references (Lagarias 1985, AMM 92; Jacobsthal-Collatz literature). We make no novelty claim for the mathematics itself, and no novelty claim flows back to ラーメン好き through this paper. The contribution of this paper is the Lean 4 record and the honest seven-route frontier map, not the underlying observation.

The Lean 4 mechanisation assistance and the manuscript drafting were carried out with Claude Opus 4.7 (Anthropic) as AI collaborator; the prior-art audit (WebSearch, 2026-05-28) and Mathlib coverage assessment (grep on Mathlib v4.27.0 commit a3a10db0…) were performed jointly.

10 References

Primary mathematical literature

[1] Lagarias, J. C. (1985). The 3x+1 Problem and its Generalizations. American Mathematical Monthly 92(1), 3–23. — The canonical survey; the (4^p − 1)/3 spine of the inverse tree and the parity-divisibility structure are implicit here.

[2] Lagarias, J. C. (ed.) (2010). The Ultimate Challenge: The 3x+1 Problem. American Mathematical Society. — Edited volume; companion bibliography.

[3] Tao, T. (2019). Almost all orbits of the Collatz map attain almost bounded values. Forum of Mathematics, Pi 10, e12 (2022). arXiv:1909.03562. — The strongest unconditional almost-all result; the load-bearing "almost all ≠ all" wall referenced in §6, Route 2.

[4] Korec, I. (1994). A density estimate for the 3x+1 problem. Math. Slovaca 44(1), 85–89. — The θ > log 3 / log 4 ≈ 0.7925 result improved by Tao.

[5] Bernstein, D. J., & Lagarias, J. C. (1996). The 3x+1 conjugacy map. Canadian Journal of Mathematics 48(6), 1154–1169. — The 2-adic conjugacy reference for §6, Route 3.

[6] Conway, J. H. (1972). Unpredictable iterations. In Proc. Number Theory Conf., Boulder (pp. 49–52), Univ. Colorado. — Generalised 3x+1-style maps are Turing-complete; the meta-level reference for §6, Route 7. Followed by Conway (1987), FRACTRAN: A simple universal programming language for arithmetic.

[7] Simons, J. L., & de Weger, B. M. M. (2005). Theoretical and computational bounds for m-cycles of the 3n+1 problem. Acta Arithmetica 117(1), 51–70. — Cycle-length exclusion via linear forms in logarithms; §6, Route 4.

[8] Terras, R. (1976). A stopping time problem on the positive integers. Acta Arithmetica 30(3), 241–252. — Parity vectors / structural descriptions; §6, Route 5.

[9] Janik, J. (2026). syracuse-confinement: a Lean 4 mechanisation reducing the Collatz conjecture to a single Diophantine confinement condition. GitHub: johnjanik/syracuse-confinement (≈13,000 lines of Lean 4). — The leading 2026 reduction; §6, Route 1.

[10] Jacobsthal-type inverse Collatz tree (arXiv:2306.14635, 2023). — One of several recent expositions of the inverse-tree structure; the exit layer (k=1 branch from root 1) is a special case.

Provenance for this paper

[11] ラーメン好き. note.com profile and articles at https://note.com/yaminotikara . — The pen-name account on note.com whose article communicated the exit-layer observation to N. Fujimoto. Profile self-description: 「豆腐のようなメンタルで、数字を数えています」. Cited and acknowledged with explicit consent of the account holder (confirmed 2026-05-29). Specific article URL and date to be pinned in §9 at next revision if ラーメン好き wishes to designate one.

Rei-AIOS artifacts (machine-checkable evidence)

[12] CollatzRei.ExitLayer Lean 4 module. Rei-AIOS repository, data/lean4-mathlib/CollatzRei/ExitLayer.lean at commit 372321c1c7001680424749fc4d11043062e4f024 (Mathlib v4.27.0 at commit a3a10db0e9d66acbebf76c5e6a135066525ac900, Lean toolchain leanprover/lean4:v4.27.0). The verbatim #print axioms output is reproduced in Appendix A.1 of this paper.

[13] Inverse Collatz tree (BFS, layers 0–4) data export. Rei-AIOS, data/inverse-collatz-tree/latest.json; generator src/aios/inverse-collatz-tree/index.ts.

[14] Collatz frontier map data export. Rei-AIOS, data/collatz-frontier/latest.json; generator src/aios/collatz-frontier/index.ts.

Background frameworks (cited for context, not load-bearing)

[15] Erdős, P. — Frequently quoted in the Collatz literature for the remark that mathematics is "not yet ready" for problems of this kind.

Appendix A — Full Lean 4 source

Source mirrored verbatim from data/lean4-mathlib/CollatzRei/ExitLayer.lean at Rei-AIOS commit 372321c1c7001680424749fc4d11043062e4f024 (STEP 1179, 2026-05-28). Compiled against Mathlib v4.27.0 (commit a3a10db0e9d66acbebf76c5e6a135066525ac900) under Lean toolchain leanprover/lean4:v4.27.0.

import Mathlib
import CollatzRei.Basic

namespace CollatzRei

open Function

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

theorem three_mul_exitM_add_one (p : Nat) : 3 * exitM p + 1 = 4 ^ p := by
  induction p with
  | zero => simp [exitM]
  | succ q ih =>
    have h : 3 * exitM (q + 1) + 1 = 4 * (3 * exitM q + 1) := by
      show 3 * (1 + 4 * exitM q) + 1 = 4 * (3 * exitM q + 1)
      ring
    rw [h, ih, pow_succ]; ring

theorem exitM_eq_div (p : Nat) : exitM p = (4 ^ p - 1) / 3 := by
  have h := three_mul_exitM_add_one p; omega

theorem exitM_odd (q : Nat) : exitM (q + 1) % 2 = 1 := by
  show (1 + 4 * exitM q) % 2 = 1; omega

theorem collatzStep_exitM (q : Nat) : collatzStep (exitM (q + 1)) = 4 ^ (q + 1) := by
  unfold collatzStep
  rw [if_neg (by have := exitM_odd q; omega)]
  exact three_mul_exitM_add_one (q + 1)

theorem collatzStep_pow2 (j : Nat) : collatzStep (2 ^ (j + 1)) = 2 ^ j := by
  have heven : 2 ^ (j + 1) % 2 = 0 := by rw [pow_succ]; omega
  unfold collatzStep
  rw [if_pos heven, pow_succ]; omega

theorem pow2_reaches_one (j : Nat) : collatzStep^[j] (2 ^ j) = 1 := by
  induction j with
  | zero => simp
  | succ q ih => rw [Function.iterate_succ_apply, collatzStep_pow2]; exact ih

theorem four_pow_eq (p : Nat) : (4 : Nat) ^ p = 2 ^ (2 * p) := by
  rw [pow_mul]; norm_num

theorem exitM_reaches_one (q : Nat) :
    collatzStep^[2 * (q + 1) + 1] (exitM (q + 1)) = 1 := by
  rw [Function.iterate_succ_apply, collatzStep_exitM, four_pow_eq]
  exact pow2_reaches_one (2 * (q + 1))

theorem exitM_succ (p : Nat) : exitM (p + 1) = 1 + 4 * exitM p := rfl

theorem exitM_pred (p : Nat) : exitM p = (exitM (p + 1) - 1) / 4 := by
  rw [exitM_succ]; omega

theorem exitM_of_eq {m p : Nat} (h : 3 * m + 1 = 4 ^ p) : m = exitM p := by
  have := three_mul_exitM_add_one p; omega

theorem exitM_recover_p (p : Nat) : Nat.log 2 (3 * exitM p + 1) = 2 * p := by
  rw [three_mul_exitM_add_one, four_pow_eq]
  exact Nat.log_pow (b := 2) (by norm_num) (2 * p)

def Reaches1 (n : Nat) : Prop := ∃ k, collatzStep^[k] n = 1

theorem exitM_reaches_one_of_pos {p : Nat} (hp : 1 ≤ p) : Reaches1 (exitM p) := by
  cases p with
  | zero => exact absurd hp (by decide)
  | succ q => exact ⟨2 * (q + 1) + 1, exitM_reaches_one q⟩

end CollatzRei
Enter fullscreen mode Exit fullscreen mode

Appendix A.1 — Axiom audit output

Captured 2026-05-29 by running an auxiliary file PrintAxiomsAudit.lean containing only import CollatzRei.ExitLayer followed by #print axioms for each load-bearing theorem, then lake env lean PrintAxiomsAudit.lean (exit code 0, no other stdout). Verbatim output:

'CollatzRei.exitM_reaches_one_of_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'CollatzRei.exitM_reaches_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'CollatzRei.three_mul_exitM_add_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'CollatzRei.exitM_pred' depends on axioms: [propext, Quot.sound]
'CollatzRei.exitM_of_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'CollatzRei.exitM_recover_p' depends on axioms: [propext, Classical.choice, Quot.sound]
Enter fullscreen mode Exit fullscreen mode

Observations:

  • All six load-bearing theorems depend only on Lean 4's three standard foundations (propext, Classical.choice, Quot.sound).
  • exitM_pred (the inverse recurrence m_p = (m_{p+1} − 1)/4, proved by omega) does not require Classical.choice; its dependency list is the tighter [propext, Quot.sound].
  • No sorryAx appears in any line.
  • No Lean.ofReduceBool (the axiom underlying native_decide) appears. The chain leading to the main theorem exitM_reaches_one_of_pos is therefore not a native_decide reduction; it is a structural Lean 4 proof.
  • The two concrete examples included in ExitLayer.lean for illustration — five_reaches_one and twentyone_reaches_one — do use native_decide and are therefore deliberately excluded from this audit; they are decorations, not part of the load-bearing claim.

Mathlib version: v4.27.0 (commit a3a10db0e9d66acbebf76c5e6a135066525ac900, as recorded in the Rei-AIOS lakefile snapshot at commit 372321c1c7001680424749fc4d11043062e4f024).

Appendix B — Inverse Collatz tree bottom layers (STEP 1177)

Generator: src/aios/inverse-collatz-tree/index.ts (Rei-AIOS). Data: data/inverse-collatz-tree/latest.json.

Layer sizes (BFS from root 1 with k = 1..5): 1, 3, 6, 12, 24 (total 46 nodes). The exit-layer family appears as the k = 1 spine of the tree. Multiples of 3 are true leaves (no preimage under T_odd).

Appendix C — Frontier map data (STEP 1178)

Generator: src/aios/collatz-frontier/index.ts (Rei-AIOS). Data: data/collatz-frontier/latest.json. See Table 1 of §6 for the human-readable extract.

Version history

  • v0.0 (2026-05-29): OUTLINE drafted. #print axioms verbatim output captured 2026-05-29 and pasted into Appendix A.1 (clean: standard 3 axioms; exitM_pred even cleaner [propext, Quot.sound]; no sorryAx; no native_decide in load-bearing chain).
  • v0.1 (2026-05-29): Promoted from OUTLINE → pre-publish review → PUBLISHED the same day. ラーメン好きさんからの 明示的同意 を受領 (confirmed 2026-05-29 by N. Fujimoto); §9 Acknowledgments を consent-received 文言に更新. Rei-AIOS commit 372321c1c7001680424749fc4d11043062e4f024 を pin (Mathlib commit a3a10db0… も同時 pin). §10 references を 15 entry に拡張 (Lagarias 1985 / Tao 2019 / Korec 1994 / Bernstein–Lagarias 1996 / Conway 1972 / Simons–de Weger 2005 / Terras 1976 / Janik 2026 等). Published 2 platforms (lightweight per user choice, no-rush principle): Zenodo DOI 10.5281/zenodo.20435288 (deposit 20435288, finalized 2026-05-29) + Internet Archive rei-aios-paper-158-1780003374000. Harvard skipped per opt-in policy.

This paper is a deliberate negative-progress record. It does not advance the proof of the Collatz conjecture. It formalises one well-known elementary observation completely, and it makes precise where every candidate reduction route still breaks.

Top comments (0)