A Spectral Reduction of the Collatz Conjecture via Phantom Orbit Shadowing - v2

Version 2 of the preprint, superseding v1 (DOI 10.5281/zenodo.20021538) of May 2026. The mathematical core is unchanged; v2 incorporates a completed Lean 4 + Mathlib formal verification of the foundational shadowing lemma, an explicit comparison with the concurrent work of Chang (arXiv:2603.11066), an expanded related-work section, and an extended methodology section that makes the cross-AI verification protocol explicit. Mathematical content We propose a structural reformulation of the Collatz conjecture in terms of a finite-dimensional spectral problem. Starting from the empirical observation that “rebel” orbits of the Syracuse map shadow, for finite stretches, periodic rational points of the 2-adic dynamics associated to negative rational fixed points (the “phantom cycles” of Chang 2026, an object that goes back to Lagarias 1985 and the Böhm–Sontacchi criterion in the Collatz literature), we construct an episode graph on the space of phantom orbits. The strongly connected component (SCC) of this graph that supports the slowest descent is encoded as a finite weighted transfer operator on a refined phase state (ν2(t), odd(t) mod 4, h mod 4) at the critical node (k=12, c=2, b=1). We prove an exact congruential shadowing lemma reducing arbitrarily long shadowing episodes to a residue condition n ≡ qw (mod 2bA+1), where qw is the 2-adic representative of a phantom word w of period sum A. The lemma is the iterated step-by-step form of the per-block 2-adic repulsion identity of Chang (2026, Prop. 7.4) and is equivalent in content to the classical inverse formula for parity vectors (Rozier 2025, Lemma 1); the iterated form is what feeds the episode graph construction and the Lean formalization. Both the lemma and its no-infinite-shadowing corollary have been mechanically verified in Lean 4 with Mathlib (Lean v4.29.1, Mathlib v4.29.1); the Lean project is sorry-free and is included in the supplementary archive. For each truncation depth T and high-bit lift count j we build a finite matrix FULLT,j encoding first-return behavior at the critical node, decompose it as FULL = CORE + TAIL via empirical signature majority, and apply a weighted Collatz–Wielandt bound (Lemmens–Nussbaum) with respect to the right Perron eigenvector v of FULLT,j. Numerical results show: bound(T, j) ≤ 0.052 for T ≤ 16 and j ≤ 32, with monotone but geometrically decaying increments in both T and j; The cross-node operator on the SCC has spectral radius 0.0366, strictly lower than the single-node worst case at the critical vertex. What this is not This is not a proof of the Collatz conjecture. The structural problem at the critical SCC is reduced to two explicit a priori estimates on finite matrices: Conjecture 6: asymptotic boundedness of the weighted bound under refinement in T; Conjecture 7: closure of the empirical signature support under refinement in j. The same distributional-to-pointwise barrier is identified in Chang (2026, Sect. 9) as the irreducible obstruction to closing several standard routes; we adopt the same honest position. The natural analytic framework for closing the conjectures is transfer-operator analysis on a Banach space of 2-adic Lipschitz functions via Lasota–Yorke + Hennion's theorem + Keller–Liverani spectral perturbation theory; we have not carried this out, and recent literature on quasi-compactness and certified spectral approximation suggests it is a non-trivial analytic project. Conditional content Conditional on Conjectures 6 and 7, the conclusion of the conditional reduction theorem is the full Collatz convergence statement (every n), which is qualitatively stronger than Tao's unconditional almost-all logarithmic-density result. Research program note This paper is the first artifact of a personal research program by the author, an independent researcher, exploring whether iterative collaboration with large language model assistants can support non-standard attempts at open mathematical problems. Verifying the practical limits of such collaboration is an explicit secondary goal of this work, on equal footing with the substantive Collatz progress. The author led the research direction throughout: the conceptual framing (gravitational debt, 2-adic corridors, the shadowing intuition, the pivot to the spectral program), the strategic choices, and the decision to publish at this stage. The technical work — Python implementation, mathematical formalization, the Lean 4 verification of the shadowing core, and the LaTeX manuscript — was developed in iterative collaboration with multiple LLM systems: OpenAI Codex and Google Gemini for the early empirical phase; Anthropic's Claude (via the Claude Code interface) for the spectral program, the formalization in Lean 4, and the manuscript drafting. The Lean phase explicitly used cross-AI checking (alternating Claude and Codex) to catch Mathlib API mismatches that one assistant missed. The work has not been reviewed by a human mathematical expert. Numerical results are deterministic and reproducible from the supplementary scripts; the Lean code is mechanically checkable with a single lake build invocation. Mathematical claims that are not yet formalized rest on AI-assisted formalization and have not been externally validated; the work is submitted explicitly to invite expert scrutiny. Constructive feedback from researchers in symbolic dynamics, p-adic dynamical systems, and transfer operator theory is explicitly invited. Planned next steps The program continues, after the v2 release, in the following order of increasing analytic difficulty: Priority A — Phantom-set taxonomy vs Chang Theorem 7.15. For a depth cutoff K0 (initially 16, possibly pushed to 20), enumerate all primitive cyclic compositions of valuations with expansive drift via Möbius inversion of necklace counts, compute their 2-adic representatives, simulate sufficiently many integer orbits in each residue class, and verify that no SCC outside the one reported in §8 of the paper appears. Bounded but non-trivial scripting; estimated one to two weeks of focused work. Priority B — Lean formalization of the episode graph and the transfer operator. Conditional on Priority A. Introduce in Lean a SimpleDigraph on nodes (k, c, b), formalize the SCC computation, define FULLT,j and the CORE + TAIL decomposition, and prove that the weighted Collatz–Wielandt bound is a true upper bound on the spectral radius for each finite (T, j). Combinatorial work; no new mathematics, but the Mathlib graph and matrix infrastructure required is non-trivial. Estimated two to four weeks of LLM-assisted Lean sessions. Priority C — Spectral-gap analysis toward Conjecture 6. A Lasota–Yorke inequality on a Banach space of 2-adic Lipschitz functions, Hennion's theorem for quasi-compactness, and Keller–Liverani perturbation theory to control the dependence on T. Open-ended and intentionally flagged as a collaboration target: making concrete progress here requires bringing in a researcher who works in transfer operators on p-adic or symbolic systems. A and B are bounded and scriptable. C is open-ended and collaboration-dependent; it will not be attempted before A and B are closed. Resources Source code: github.com/PieroBorgatta/Collatz Methodology, contribution split, literature reconnaissance method, and full discussion of the planned next phases: see METHODOLOGY.md in the supplementary archive Lean formalization: see lean/ in the supplementary archive