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

Version 3 of the preprint, superseding v2 (DOI 10. 5281/zenodo. 20098868) of May 2026. The mathematical core of v2 is unchanged; v3 extends it along two axes: a finite phantom-set taxonomy at depth K₀ = 16, and an extended Lean 4 + Mathlib formalization that now covers the finite operator layer in addition to the shadowing core. 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 (₂ (t), odd (t) 4, h 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 2^bA+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 are mechanically verified in Lean 4 with Mathlib (Lean v4. 29. 1, Mathlib v4. 29. 1) ; the Lean project is sorry-free and axiom-free. For each truncation depth T and high-bit lift count j we build a finite matrix FULLₓ, ₉ 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 FULLₓ, ₉. 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. New in v3 (i) Phantom-set taxonomy at K₀ = 16. Möbius enumeration of all 1247 primitive expansive cyclic compositions with K 16, exact rational 2-adic representatives in exact arithmetic, orbit harness identifying a single nontrivial taxonomy SCC of 1222 raw states. (ii) Deterministic finite-residue-cell Collatz–Wielandt certificate. Exhaustive enumeration of 2^lift\bits residue subclasses per source state (zero budget exits at lift\bits = 4), producing exact rational deterministic transition matrices and an exact CW certificate on the compressed (K, b) macro-state space (37 states): max ratio 90833233962213/129559208330288 < 3/4. Sensitivity at lift\bits \4, 5, 6\ confirms a monotonically improving bound (0. 701 0. 691 0. 667). (iii) Lean-checked finite operator pipeline. New Lean modules EpisodeGraph. lean, Operator. lean, Bound. lean formalize the episode graph, the truncated transfer operator with phase-state quotient, and the generic weighted Collatz–Wielandt bound. Two generated finite numerical certificates are imported and their spectral-radius bridges are exposed: t10j32HighBitTailSpectralRadiusBound₉7₂000: (FULL₁₀, ₃₂) 97/2000 = 0. 0485, a fully expanded 224-row Lean-checked CW certificate at the critical single node; k16s16KDeterministicGeneratedSpectralRadiusBound: (P₊, ₁) 3/4, the deterministic finite-residue-cell certificate at K₀ = 16. Both bridges target Mathlib's real spectralRadius; the entire project is sorry-free and axiom-free. 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 1 (uniform bound in T): ₓ, ₉ bound (T, j) < 1; Conjecture 2 (signature closure in j): empirical transition signatures stabilize for large j with explicit decay rate. The v3 deterministic finite-residue-cell certificate closes the taxonomy-completeness side of the v2 open scope at the explicit depth cutoff K₀ = 16: the original empirical v2 SCC is shown to live inside a larger but still subcritical taxonomy SCC. It does not close the asymptotic-in-T side of either conjecture. 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 1 and 2, the conclusion of the conditional reduction theorem is the full Collatz convergence statement (every positive integer n), which is qualitatively stronger (all integers vs. almost all) than Tao's unconditional almost-all logarithmic-density result. The comparison concerns the scope of the conclusion, not the quality of the proof: Tao's result is a deep unconditional theorem; the present result is a conditional reduction modulo the two stated finite-matrix estimates. v3 does not change the conditional content of v2; it strengthens the unconditional finite-matrix layer that underlies it. Research program note This is the third versioned 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, the framing of the taxonomy phase and of the gated Phase-10 roadmap, and the decision to publish at each stage. The technical work — Python implementation, mathematical formalization, the Lean 4 verification of the shadowing core, the Phase-7 phantom-taxonomy enumeration and the deterministic finite-residue-cell construction, the Phase-8 Lean formalization of the finite operator layer, 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 Lean 4 formalization (v1→v2 shadowing core and v2→v3 finite operator layer), the v3 manuscript drafting, and the v3 gated Phase-10 restructuring; OpenAI Codex for the Phase-7 phantom-taxonomy scripts and the Phase-8 generated Lean certificates; Cross-AI checking (alternating Claude and Codex) used in both Lean phases to catch Mathlib API mismatches and to remove a residual axiom in the T = 10, j = 32 CW certificate that one assistant had introduced and the other closed. The work has not been reviewed by a human mathematical expert. Numerical results are deterministic and reproducible from the supplementary scripts (including the v3 exact-rational deterministic finite-residue-cell certificate) ; 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 (toward v4 or a companion) v3 closes the original Priority A (phantom-set taxonomy) and Priority B (Lean formalization of the episode graph and finite transfer operator) of v2. The remaining priority is the analytic program of Priority C, restructured in v3 as a gated A–J roadmap with explicit kill-switch and a finite-rank fallback baseline already in place. The full operational table is in lean/TODO. md, Phase 10; the published version is §11. 1 of v3. Priority A — Phantom-set taxonomy (closed in v3). All 1247 primitive expansive compositions with K 16 enumerated; deterministic CW bound < 3/4 on the compressed (K, b) macro-state space, imported into Lean. Priority B — Lean formalization of the finite operator layer (closed in v3). Episode graph, phase-state quotient, generic weighted Collatz–Wielandt bound, single- (T, j) certificate at T = 10, j = 32, and the deterministic taxonomy certificate at K₀ = 16 all imported and bridged to Mathlib's spectralRadius. Priority C — Transfer-operator roadmap toward Conjecture 1 (program for v4 / companion / collaboration). A 10-step gated sequence: (A) Literature and hypothesis matrix (Keller–Liverani, Hennion, Baladi, Sarig, GDMS, p-adic dynamics), with Chang 2026 compatibility as a column rather than a separate task. (B) Identify the correct infinite phase space behind FULLₓ, ₉. Load-bearing question: if the finite matrices are not exact projections of any natural infinite kernel, the program forks to step (G). This is the kill-switch source. (C