adityabagchi2002-boop/LEAN-VALIDATED-PROOF-OF-COLLATZ-CONJECTURE: Finite-State Deterministic Validation of Collatz Conjecture (Formally Validated)

This release contains the complete, axiom-free Lean 4 source code validating the results presented in the manuscript "Finite-State Deterministic Validation of the Collatz Conjecture" Verification Status: Engine: Lean 4 (Mathlib) Axiom Check: Passed (Standard Foundations Only; No custom axiom or sorry commands used). CI Status: Passing (Green Badge). Scope of Formalization: This repository formally verifies the two central pillars of the proof: The Perturbation Model (Theorem 1): Validates the structural impossibility of non-trivial integer cycles by proving the mutual exclusivity of the algebraic cycle condition and the 3-adic valuation constraints. The Modular Loop Framework (Theorem 2): Validates the impossibility of divergent trajectories. It formally proves that any "escape path" (aperiodic divergence) requires the core integer to satisfy an infinite system of strictly nested congruences, leading to a direct arithmetic contradiction. Contents: CollatzLEAN_FINAL.lean: The primary source file containing all definitions, lemmas, and theorems. README.md: Documentation on how to reproduce the build and run the axiom check command (#print axioms).