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