Does every number reach one under the Collatz map?

I am proving a theorem in Lean 4 and submitting it to Conjectura.

## Problem NT004 — Does every number reach one under the Collatz map?

Halve if even, triple and add one if odd. Every number tried so far eventually reaches 1. Nobody can prove they all do.

## Environment (fixed — do not assume anything newer)

- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`

If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.

## The exact statement I must prove

```lean
theorem solution : CollatzConjectureProp := by
  sorry
```

## The file I submit

```lean
import Conjectura.Problems.NT004.Statement

namespace Submission

theorem solution : Conjectura.NT004.goal := by
  sorry

end Submission

```

## The Lean definitions of every term in this problem

These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.

### Collatz conjecture

The Collatz conjecture: every positive integer `CollatzReaches` one.

```lean
Conjectura.NumberTheory.CollatzConjectureProp
-- unfolds to:
def CollatzConjectureProp : Prop := ∀ n : ℕ, 0 < n → CollatzReaches n 1
```
Defined in this corpus.

### CollatzReaches

`CollatzReaches m n` holds when iterating `collatzStep` from `m` eventually gives `n`.

```lean
Conjectura.NumberTheory.CollatzReaches
-- unfolds to:
def CollatzReaches (m n : ℕ) : Prop :=
  Relation.ReflTransGen (fun a b => b = collatzStep a) m n
```
Defined in this corpus.

### Collatz step

One Collatz step: halve an even number, or triple an odd one and add one.

```lean
Conjectura.NumberTheory.collatzStep
-- unfolds to:
def collatzStep (n : ℕ) : ℕ := if n % 2 = 0 then n / 2 else 3 * n + 1
```
Defined in this corpus.

### ReflTransGen

inductive

```lean
Relation.ReflTransGen
```
Defined in Mathlib.

## Rules — submissions violating these are rejected automatically

1. **Do not change the name or type of `solution`.** It must satisfy the
   statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
   Declaring your own `goal`, or redefining a name it depends on, produces a
   proof of a *different* statement and is rejected. This is the single most
   common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
   axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
   accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
   `Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
   `snake_case` theorem names, `UpperCamelCase` types.

## What I want from you

Here is my argument in informal mathematics:

> [PASTE YOUR PROOF SKETCH HERE]

Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.