Conjecture de Syracuse / Collatz : théorème conditionnel formalisé en Lean 4 (kernel-checked). Ne prouve PAS la conjecture. Prouve la non-existence de cycles non-triviaux modulo 3 hypothèses externes documentées (1 conjecture de travail Baker, 1 vérification computationnelle reproductible Barina, 1 dérivation projet DerivedLargeKBound). Conditional theorem formalized in Lean 4 — does NOT prove Collatz, modulo 3 documented external hypotheses. δ8/δ8