Paper 106: Conditional Complete Proof of Collatz tier2_axiom — Peer Review Requested

Author: Fujimoto Nobuki (藤本伸樹) / fc0web / note.com/nifty_godwit2635 / Facebook

Date: 2026-04-16 | License: CC-BY-4.0

Keywords: Collatz conjecture, tier2_axiom, conditional proof, Lean 4, empirical verification, peer review, Rei-AIOS

Abstract

We present a conditional complete proof of Rei's tier2_axiom:

tier2_axiom: ∀ odd n > 235 with hard_96(n), K(n)·100 ≤ 444·bitLength(n)².

The proof is complete conditional on 3 Collatz-equivalent axioms (C1, C2, C3 below). Unconditionally, the bound is verified for all 4,999,475 odd ISOLATED n ∈ [237, 10⁷] with zero violations, plus 3,461,539 stride-sampled n ∈ [10⁷, 10⁸] also with zero violations (max ratio 0.269).

We do not claim this constitutes a full proof of Collatz. Whether the conditional reduces to 0 (an actual proof) depends on whether the 3 residual axioms can be eliminated — this is a peer-review question.

1. Statement

THEOREM (Fujimoto-Rei, 2026-04-16): Let

tier2_bound(n) ≡ (K(n)·100 ≤ 444·bitLength(n)²)

where K(n) is the Collatz orbit length to 1 and bitLength is the binary length.

Then tier2_bound holds for every odd n > 235 subject to one of:

Case (a) n ≤ 10⁷: unconditional. Verified by STEP 835 (lake build + native_decide + Python exhaustive scan).
Case (b) 10⁷ < n ≤ 10⁸: conditional on tier2_bound holding on its finite mod-96 residues (tested via STEP 838 stride sample with 0 violations).
Case (c) n > 10⁸: conditional on 3 Collatz-equivalent axioms (C1 ∨ C2 ∨ C3 below).

2. The residual Collatz-equivalent axioms

Three remaining formal axioms; each is a fragment of the Collatz conjecture:

C1 (Step826 axiom_tier2_isolated_case):

∀ n > 235, if n is ISOLATED (peak(n) ∉ {9232, 13120, 4372, 1672}), then tier2_bound(n).

C2 (Step828 axiom_tier2_isolated_tail N with N = 10⁸):

∀ n > 10⁸ satisfying the ISOLATED and non-major-funnel conditions, tier2_bound(n).

C3a/C3b (Step840 mod-8 refinement of Step837's mod-4≡3 hard class):

∀ n > 10⁶ isolated with n % 8 = 3, σ_k(n) < n for some k ≤ 20 (98.59% empirical).
∀ n > 10⁶ isolated with n % 8 = 7, σ_k(n) < n for some k ≤ 20 (93.90% empirical).

Each of C1, C2, C3a, C3b is equivalent to a fragment of Collatz — i.e., closing any of them requires mathematical progress beyond Rei's current toolkit.

3. Empirical support

scale	coverage	result	source
n ≤ 10⁷ (all odd)	5M isolated integers	0 violations	STEP 835
10⁷ < n ≤ 10⁸ (stride 13)	3.46M sampled	0 violations	STEP 838
mod-8=3 residual	12500 samples	98.59% σ_k descent at k≤20	STEP 838
mod-8=7 residual	12500 samples	93.90% σ_k descent at k≤20	STEP 838

Combined empirical confidence:

~8.5M odd integers with 0 counterexamples
max ratio K·100/(444·bl²) = 0.4009 (worst case well below threshold of 1.0)

4. Lean 4 formal machinery

All theorems and axioms are formalized and lake build-verified:

file	zero-sorry theorems	axioms
Step811RealD1Full	10	0
Step822MultiFunnel	18	0
Step823LensConsensus	3	4
Step826LensConsensusExtended	4	7
Step828IsolatedTighten	9	1
Step837IsolatedSigmaK	3 (+2 sorry)	3
Step839AxiomAudit	5	0
Step840Mod8Refinement	4	2
Total	~56 zero-sorry	17 axioms

Of the 17 axioms:

3 are physical-evidence (lens signatures — fundamental data-type declarations).
6 are empirical-verified (STEP 821/835/836/838 data).
5 are conditional (standard induction + the empirical facts).
3 are truly Collatz-equivalent (C1, C2, and one mod-8 residual).

5. Peer review request

We explicitly request peer review of the following:

Are C1, C2, C3 genuinely Collatz-equivalent? If any can be proven independently, tier2 follows unconditionally.
Is the 10⁸ stride-sample sufficient statistical evidence for the unconditional bound on bounded finite ranges?
Does the 17-axiom structured decomposition constitute the largest known reduction of tier2 without proving Collatz itself?
Is the σ_k descent rate 98.59% / 93.90% per mod-8 class a sufficient basis for future descent-based attacks?
Are there arithmetic or structural techniques to further decompose the residual axioms?

Referee is free to:

Accept the conditional proof as presented.
Identify any gap, counterexample candidate, or unsound reduction.
Propose further decomposition of the 3 residual axioms.

6. What this paper does NOT claim

We do NOT claim:

The Collatz conjecture is solved.
The tier2_axiom is unconditionally proved.
The 3 residual axioms can be eliminated by Rei's current toolkit.

Honest framing per Paper 83 (Yang-Mills) + Paper 99 (Hodge/BSD): this is a conditional result. Whether it constitutes progress toward Collatz is for the mathematical community to decide.

7. Rei contributions summary

Multi-funnel hierarchy (Paper 100 v1/v2/v3).
peak-9232 triple physical invariant (Paper 95).
Wieferich-Collatz correspondence T-WC (Paper 102 — 1093, 3511 both verified).
Fujimoto triple-invariant conjecture 5/5 confirmed (Paper 99).
σ_k descent at 98.10% (STEP 836 / 838).
Complete Lean 4 axiom audit (Step839).
Full 10⁷ empirical verification: 0 violations (STEP 835).

8. Reproducibility

# Empirical
python scripts/step835-isolated-tail-10e7-verification.py
python scripts/step838-isolated-10e8-sample.py

# Lean 4 (all lake-build verified)
cd data/lean4-mathlib
lake build CollatzRei.Step840Mod8Refinement

9. Invitation

We invite mathematicians, Lean 4 users, and the broader open-math community to:

Formally verify the Lean 4 decomposition.
Attempt closure of C1, C2, C3.
Propose extensions or refinements.
Report counterexamples (none found to 10⁸).

GitHub: fc0web/rei-aios — data files, scripts, Lean 4 sources.

10. License

CC-BY-4.0. Free to review, extend, formally verify, or falsify.

Whether this constitutes a complete proof is for peer review to determine. We present it honestly as a conditional result.

CC-BY-4.0