Phantom Orbit Shadowing for the Collatz Conjecture: Verified Core, Two Barriers, and a Repositioning

Phantom Orbit Shadowing for the Collatz Conjecture: Verified Core, Two Barriers, and a Repositioning (version 4). This is a consolidation and repositioning version of an ongoing, AI-assisted personal research program on the Collatz conjecture by an independent researcher. It does not report progress toward a proof of the conjecture. Its purpose is to state precisely what is rigorously established, to identify the two distinct barriers the program runs into, to prove why the current approaches stop there, and to record the resulting decision about what to do next. This is not a proof of the Collatz conjecture, and v4 does not claim progress toward one. It is a mechanically verified core plus an honest map of an attempt and its limits. Verified core (mechanically checked in Lean 4 with Mathlib; sorry-, admit- and axiom-free): an exact congruential shadowing lemma and its no-infinite- (periodic-) shadowing corollary; finite Collatz–Wielandt spectral-radius certificates exposed to Mathlib's spectralRadius (single node, radius ≤ 97/2000; deterministic (K, b) bound < 3/4 at K0 = 16) ; a finite phantom-set taxonomy at depth K0 = 16; an elementary, formally verified bridge reducing the conjecture to a uniform strict-descent hypothesis. New in this version (v4): Two-barrier map. The conjecture splits into two genuinely distinct hard halves: no divergent orbits (barrier: distributional-to-pointwise) and no nontrivial cycles (barrier: Diophantine approximation of log23). Every part of the program is located relative to these two walls. Negative resolution of the pointwise route. Within the present phantom/2-adic formalism, the sought aperiodic rigidity on the orbit limit point is logically equivalent to the divergence conjecture itself — a non-transport lemma: the parity-vector conjugacy carries eventual periodicity to dynamical pre-periodicity, not to rationality. A paper-level argument, conditional on the standard Lagarias coding. New Lean-checked fact. No positive integer lies on an expanding cycle (post-prefix congruence form, noₚositiveₑndpointₑventuallyₚeriodicₑxpansivecongruence), generalizing the no-infinite-shadowing corollary. Planned next steps. Stop treating the weak/operator and pointwise first-barrier branches as direct routes to the conjecture: by the v4 results, further finite refinement (more T, j, cylinders, suffixes) cannot cross the divergence barrier by these routes. The weak branch may continue only as a separate, honestly labeled operator-approximation study. Redirect mathematical effort to the cycle half — the only half where partial theorems and tools genuinely bite (linear forms in logarithms, continued fractions of log23, computation; Steiner, Simons, Simons–de Weger). The realistic, finishable target is the structural layer formalized in Lean; we note the limit that a usable form of Baker's theorem is not currently in Mathlib, so the deep analytic exclusions are not cheaply formalizable. Consolidate the verified assets (this version). Continue the methodology study of AI-assisted mathematics, including the program's capacity to recognize and prove its own ceiling. Supplementary archive contents: the v4 paper (PDF and LaTeX source), the full Lean 4 + Mathlib formalization sources, the Python enumeration and diagnostic scripts, the phantom-set taxonomy data backing the certificates, and the working notes and decision logs. Methodology. The program is conducted in cross-AI collaboration (OpenAI Codex and Anthropic's Claude), with all formal claims funneled through Lean. v4 is itself a methodological data point: the cross-AI process converged on a precise negative result about its own approach, which we regard as a positive finding distinct from progress on the mathematics. The work has not been reviewed by a human mathematical expert; expert scrutiny is explicitly invited. Source code and Lean formalization: github. com/PieroBorgatta/Collatz Versions: concept DOI (always resolves to the latest) 10. 5281/zenodo. 20021537; previous versions v3, v2, v1. License: Creative Commons Attribution 4. 0 International (CC BY 4. 0).