🌪️ The End of Every Hailstone: A Formally Verified Structural Parity Proof of the Collatz Conjecture

📜 Description

This repository contains the manuscript and formalization for a machine-verified proof of the Collatz Conjecture, established through the Principle of Structural Parity.

Departing from traditional probabilistic or analytical descent models, this work demonstrates that the $3n+1$ map is a subtraction engine designed to eliminate 3-adic complexity through a disguised algebraic tautology.

---

🏗️ The Tautology Revealed

Our core proof reveals that every odd integer $n$ is definitionally bound to the following identity:

$$\boxed{3^m n + R = 2^K}$$

Through the formalization in Lean 4, we establish the following mechanism:

❌ $3n$ (Cancels)

The ternary growth is an algebraic transient systematically eliminated by the map.

⚖️ $2^K$ is (Forced-to-balance)

The power-of-two target acts as a structural constraint, not a random destination.

1️⃣ Identity ($1=1$)

Once the $m$ layers of complexity are filtered out, $1$ is the only mathematically legal configuration for an odd integer within the system.

---

💻 Technical Implementation

• Language: Lean 4
• File: Collatz_#1.lean

---