A Certified Six-Leaf Semantic Grammar for the Collatz Dynamics in Lean 4

This release provides a Lean 4.14.0 formalization of a finite, exhaustive, and exclusive six-leaf semantic grammar for the Collatz dynamics. Under the explicit premise CollatzVerifiedBelowBase68, the formal development establishes a global semantic classification with exactly six leaves. Either every positive natural number reaches 1, or there exists a unique positive minimal counterexample assigned to exactly one of five explicit failure leaves: 1. NONTRIVIAL_CYCLE2. RBC_UNBOUNDED_B_GAP3. RBC_BOUNDED_PRIME_RENEWAL4. NON_R_INTERNAL_DESCENT5. NON_R_SURVIVOR The principal publication theorem is: axisGeo_final_six_leaf_grammar_exactly_one The public API theorem is: certified_six_leaf_semantic_grammar The release includes the complete Lean source tree, reproducibility files, build logs, axiom audits, source-hygiene checks, checksums, and an accompanying technical paper. This work does not prove the Collatz conjecture and does not prove that the five failure leaves are empty. The five corresponding universal exclusion obligations remain open. The publication modules contain no sorry, admit, sorryAx, project-specific axiom, opaque, or unsafe declarations. The archived axiom audit reports only standard Lean foundational principles.