Formal LEAN Validation of Collatz Conjecture

This deposit contains the 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 16 interconnected lemmas (1A–2H) leading to the final contradictions in Theorem 1 (Non-Existence of Cycles) and Theorem 2 (Impossibility of Divergence). LEAN 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 (sorry or admit). Guarantee: The synthesis formally validates that the required Exponential Cost of Repair (Corollary 1H-1) strictly exceeds the Linear Budget of the path, guaranteeing the structural impossibility of both counterarguments to the conjecture. No hidden sorry used and no axiom imposed while encoding the proof concept. Full transparency endeavoured. GitHub Batch (passing): https://github.com/adityabagchi2002-boop/LEAN-VALIDATED-PROOF-OF-COLLATZ-CONJECTURE/blob/main/README.mdGitHub Release: https://github.com/adityabagchi2002-boop/LEAN-VALIDATED-PROOF-OF-COLLATZ-CONJECTURE/releases/tag/v1.0