# Collatz and discrete dynamics

[All sections](../README.md)

## Modules

| Module | Verified result |
|---|---|
| [CollatzBase](CollatzBase.en.md) | Reachability of one for the finite base {1,2,3,4,5}. |
| [CollatzAttractor](CollatzAttractor.en.md) | Conditional reachability of one once an orbit enters the finite base. |
| [CollatzCycles](CollatzCycles.en.md) | Exclusion of positive one- and two-step returns; classification of three-step returns. |
| [CollatzParity](CollatzParity.en.md) | Exact branch formulas for parity and residues modulo 4 and 8. |
| [CollatzDyadicContract](CollatzDyadicContract.en.md) | Finite iteration formulas and a decrease on the specified residue branch modulo 8. |
| [CollatzAverageDrift](CollatzAverageDrift.en.md) | The residue-5 branch formula and normalization of prescribed rational weights. |
| [CollatzBranchSeven](CollatzBranchSeven.en.md) | Splitting the residue-7 branch modulo 16, iteration formulas, and the finite orbit of seven. |
| [CollatzBranchFifteen](CollatzBranchFifteen.en.md) | Refining the residue-15 branch modulo 32 and finite iteration formulas. |
| [CollatzDyadicTree32](CollatzDyadicTree32.en.md) | A six-branch partition; arithmetic mean of coefficients 639/512 > 1; 31 reaches 5 after 101 steps. |
| [CollatzGeometricDrift](CollatzGeometricDrift.en.md) | The exact coefficient product 3^30/2^49 is between zero and one. This is a power of the geometric mean, not an orbit-wise contraction theorem. |
| [CollatzLogPotential](CollatzLogPotential.en.md) | Negativity of the specified scalar expression (15/8) log 3 − (49/16) log 2. |
| [CollatzRemainderBound](CollatzRemainderBound.en.md) | The weighted rational correction 40/81 and bounds after division by the input. |
| [CollatzEffectiveDrift](CollatzEffectiveDrift.en.md) | A negative scalar bound for n ≥ 13 and reachability of one for inputs 1 through 12. |
| [CollatzMarkovOperator](CollatzMarkovOperator.en.md) | Equality between a weighted expression and a scalar bound, plus a conditional dichotomy. No Markov transition kernel is constructed. |
| [CollatzUnified](CollatzUnified.en.md) | Selected finite, arithmetic, and scalar results collected in CollatzFormalSuite. |
| [CollatzBakerBound](CollatzBakerBound.en.md) | Numerator and divisibility checks for finite three-transition cases. No general Baker bound is proved. |
| [Collatz2Adic](Collatz2Adic.en.md) | Divisibility of differences by powers of two: one accelerated step loses at most one bit of precision, and n steps lose at most n bits. |
| [Collatz2AdicErgodic](Collatz2AdicErgodic.en.md) | Positive cylinder weights and equal preimage cardinalities at ranks 1 and 2 only. No general Haar-measure invariance or ergodicity theorem is proved. |
| [Generated](Generated.en.md) | A separate real scalar estimate with explicit witnesses s=1/3, gamma=0.94566, and N₀=5. No link to a global orbit is established. |

## Scope

Finite trajectories, congruences, and scalar estimates do not prove the Collatz conjecture. Weighted coefficient identities do not establish the behavior of every deterministic orbit.

[Contributing](../CONTRIBUTING.en.md) · [Validation](../VERIFICATION.en.md)