FINITE-STATE DETERMINISTIC VALIDATION OF THE COLLATZ CONJECTURE

This deposit contains a manuscript (preprint version) and its Lean 4 source code for the formal verification of the non-existence of non-trivial cycles and divergent trajectories in the Collatz system. The codebase implements a Deterministic Framework consisting of 14 interconnected lemmas (1A–2F) leading to the final contradictions in Theorem 1 (Non-Existence of Cycles) and Theorem 2 (Impossibility of Divergence). Verification Status: The entire formalization adheres to the highest standards of proof integrity: Tool: Lean 4 Theorem Prover / Mathlib. Integrity: The code contains zero unproven assertions (no uses of sorry or admit). Formal Guarantee: The synthesis formally validates that the required Exponential Cost of Repair (Corollary 1H-1) strictly exceeds the Linear Budget of the path, establishing the structural impossibility of both counterarguments to the conjecture. Note: No hidden axioms or unproven assumptions were used in the encoding of this proof. GitHub Badge (passing): https://github.com/adityabagchi2002-boop/LEAN-VALIDATED-PROOF-OF-COLLATZ-CONJECTURE/blob/main/README.md