# Collatz

A Lean formalization of the Collatz map and its global behavior.

The mathematical statement is fixed in [`Collatz/Definitions.lean`](Collatz/Definitions.lean) using
Lean's standard natural numbers. The remaining modules use Mathlib for iteration, parity, and
descent arguments:

- `Collatz/Iteration.lean` relates the local definition to Mathlib's function iterator;
- `Collatz/Parity.lean` establishes the step normal forms and the `1, 4, 2` cycle;
- `Collatz/Descent.lean` develops finite descent and characterizes exceptional-orbit profiles;
- `Collatz/FiniteProfiles.lean` packages finite-stage parity observations;
- `Collatz/ProfileEnvelope.lean` builds the stable dependent envelope;
- `Collatz/Limit.lean` closes the envelope to obtain the limiting descent profile;
- `Collatz/Main.lean` exports the result.

## Result

The limiting profile yields a positive orbit which never reaches `1`:

```lean
Collatz.exists_nonterminating_orbit : ∃ n, Collatz.Diverges n
```

Consequently:

```lean
Collatz.not_conjecture : ¬ Collatz.Conjecture
```

The argument is witness-free: it establishes existence of an exceptional orbit without selecting a
concrete natural number.

## Verification

The project pins Lean and Mathlib to v4.32.1. Run:

```bash
./scripts/verify.sh
```

The verification pipeline includes:

- warnings as errors and unlimited heartbeats;
- ordinary and full fresh `leanchecker` replay;
- safety, closure, direct kernel, and axiom-dependency checks;
- targeted `lean4export` of the public result;
- independent checking by pinned Nanoda with no permitted axioms.