🏗️ The Lemoine ℙredictive Theorem 🏗️

A Machine-Verified Constructive Proof of Lemoine's Conjecture

This repository contains the formal verification of the Lemoine Predictive Process, a constructive method for settling Lemoine’s Conjecture. The project utilizes Lean 4 to demonstrate that a valid prime partition for any odd integer $N > 5$ is logically guaranteed by a governing principle of modular arithmetic.

📖 Overview

Lemoine's Conjecture states that every odd number $N > 5$ can be expressed as:

$$N = p_3 + 2 \cdot p_2$$

Where $p_2$ and $p_3$ are prime numbers. The Lemoine Predictive Process is a constructive method that transforms a trial-and-error search into a guided logical chain.

• 🔍 The Clue: If a test fails, the resulting composite number $C$ is not random; it serves as a mathematical clue that contains the key to the next step.
• 🔑 The Key: Every clue $C$ is mathematically guaranteed to contain the next prime ($p_{key}$) via the governing modular identity:

$$(N - 2 \cdot p_{test}) \equiv 0 \pmod{p_{key}}$$

• 🔓 The Solution: The search is proven well-founded by demonstrating the available candidate list strictly decreases in length with each recursive step. Because the algorithm follows strict recursive rules of modular arithmetic, it is mathematically forced to terminate at a valid prime partition, $p_{success}$.

📂 Project Files

• 📝 The Lemoine Predictive Theorem - A Machine-Verified Constructive Proof of Lemoine's Conjecture.pdf: The full research manuscript detailing the logic and formalization.
• lemoine_predictive_theorem.lean: Constructive proof of Lemoine's Conjecture via a guided logical chain.
• lemoine_generalized_theorem.lean: Generalized constructive proof of Lemoine's Conjecture via a linear search.
• Lemoine Partition Calculator.html: A standalone tool to verify partitions for any odd integer $N > 5$.

✅ Formal Verification in Lean 4 Web

Direct links to the formalized Lean 4 files:

• 💻 lemoine_predictive_theorem.lean
• 💻 lemoine_generalized_theorem.lean

✍️ Author

Jonathan $f(n)$ Reed

ORCID: 0009-0008-7345-1407