Formal verification of critical theorems for the epoch-based deterministic framework presented in the Collatz conjecture paper.

This repository contains Lean 4 formalizations of key mathematical results related to the Collatz conjecture (3x+1 problem). The formalization focuses on three core components:

1. Ord‑Fact: Multiplicative order of 3 modulo powers of 2
2. Semigroup ⟨Δ⟩: Junction shift generation of cyclic groups
3. SEDT: Scaled Epoch Drift Theorem (negative drift envelope)

• ✅ Proven: No sorry placeholders, all steps verified
• 🟡 Structured: Logical structure complete, some steps documented as sorry
• 📝 Statement only: Theorem formalized, proof deferred as future work

collatz-lean4/
├── Collatz/
│   ├── Basic.lean              # Core Collatz definitions (T_odd, e, depth_minus)
│   ├── Arithmetic.lean         # Foundational arithmetic lemmas (20/23 proven)
│   ├── OrdFact.lean            # Ord‑Fact theorem + examples t=3,4,5 (proven!)
│   ├── Epoch.lean              # Epoch and Phase type definitions
│   ├── Semigroup.lean          # Junction shift semigroup ⟨Δ⟩
│   ├── SEDT.lean               # SEDT envelope theorem
│   └── Examples.lean           # Worked examples (15 examples)
│
├── lakefile.lean               # Lake build configuration
├── lean-toolchain              # Lean version (v4.24.0-rc1)
└── README.md                   # This file

• Lean 4 (v4.24.0-rc1 or later)
• elan (Lean version manager)

# Clone the repository
git clone <repository-url>
cd collatz-lean4

# Build the project
lake build

# Build examples module (optional)
lake build Collatz.Examples

If everything is configured, lake build should complete successfully.

Theorem (OrdFact.lean):
For t ≥ 3, the multiplicative order of 3 modulo 2^t equals 2^{t-2}.

theorem ord_three_mod_pow_two (t : ℕ) (ht : t ≥ 3) :
  orderOf (3 : ZMod (2^t)) = Q_t t

Examples (all proven with decide):

example : orderOf (3 : ZMod 8) = 2 := by decide   -- t=3 ✅
example : orderOf (3 : ZMod 16) = 4 := by decide  -- t=4 ✅
example : orderOf (3 : ZMod 32) = 8 := by decide  -- t=5 ✅

Proof Strategy:

1. Upper bound: 3^{2^{t-2}} ≡ 1 (mod 2^t) via induction + lifting lemma
2. Lower bound: Minimality via 2-adic valuation
3. Main theorem: Combine using orderOf_dvd_iff + Nat.dvd_prime_pow

Theorem (Semigroup.lean):
The additive subgroup generated by junction shifts equals Z/Q_t Z.

theorem delta_generates {t : ℕ} (ht : t ≥ 3) :
  AddSubgroup.closure (@DeltaSet t) = ⊤

Proof Strategy:

1. DeltaSet contains 1 (trivial junction)
2. 1 is odd → primitive generator of Z/Q_t Z
3. ⟨1⟩ = Z/Q_t Z ⊆ ⟨DeltaSet⟩ → ⟨DeltaSet⟩ = Z/Q_t Z

Theorem (SEDT.lean):
For long t-epochs (L ≥ L₀) with β > β₀(t,U):
ΔV ≤ -ε(t,U;β)·L + β·C(t,U), where ε > 0

theorem sedt_envelope (t U : ℕ) (e : SEDTEpoch) (β : ℝ)
  (ht : t ≥ 3) (hU : U ≥ 1) (hβ : β > β₀ t U) (h_long : e.length ≥ L₀ t U) :
  ∃ (ΔV : ℝ), ΔV ≤ -(ε t U β) * (e.length : ℝ) + β * (C t U : ℝ) ∧ ΔV < 0

Constants defined:

• α(t,U): Touch frequency parameter
• β₀(t,U): Threshold for β
• ε(t,U;β): Negative drift coefficient (β(2-α) - log₂(3/2))
• C(t,U), L₀(t,U), K_glue(t): Overhead bounds

# Build a specific module
lake build Collatz.OrdFact

# Check a file for errors
lake env lean Collatz/Arithmetic.lean

• Collatz/Arithmetic.lean: 0 sorry (complete)
• Collatz/OrdFact.lean: 0 sorry (complete; main theorem proven)
• Collatz/Semigroup.lean: 0 sorry (complete; junction shift generation proven)
• Collatz/SEDT.lean: may contain remaining sorry items marked for future work

GitHub Actions automatically:

• ✅ Builds the project on push/PR
• ✅ Caches Lake dependencies
• ✅ Runs examples
• ✅ Generates build summaries

See .github/workflows/lean.yml for details.

See ../collatz-paper/ for the main mathematical paper and computational verification scripts.

• Lean 4: v4.24.0-rc1 or later
• mathlib4: latest (resolved by Lake)

1. Create a new .lean file in Collatz/
2. Import required modules
3. Add to Collatz.lean (main file)
4. Build and test: lake build

Priority areas for contributions:

1. SEDT.lean: strengthening envelope bounds and completing deferred steps

• Ord‑Fact main theorem: proven
• Semigroup generation: proven
• Arithmetic lemmas: complete
• CI: builds on push/PR via GitHub Actions

• Complete SEDT envelope proof (~5-10 hours)
• Add more worked examples for SEDT

• Full SEDT proof (multi-step induction)
• Cycle exclusion formalization (Appendix B)
• Coercivity proof (Appendix C)
• Integration with computational verification results

MIT — see LICENSE.

• Lean 4 community for mathlib and excellent documentation
• Expert consultations on orderOf patterns and modular arithmetic
• Paper reviewers for suggesting formal verification

Build Status:

Last Updated: October 2025
Maintainer: Anatolii Shumak
Paper: See ../collatz-paper/ for mathematical details