The prime frontier at one modulo twenty-four
ProvedErdosStraus242.mod24_reductionThe root assertion for every natural number is equivalent to the existence of a distinct positive ordered decomposition for every prime . No additional assumption is hidden in the property.
import Definitions.Def_ErdosStraus242 import Mathlib.Data.Nat.Prime.Basic import Mathlib.Data.Finset.Insert
namespace ErdosStraus242
theorem mod24_reduction :
(∀ n : ℕ, 2 < n → IsErdosStraus n) ↔
(∀ p : ℕ, Nat.Prime p → p % 24 = 1 → IsErdosStraus p) := by sorry
end ErdosStraus242
Read-back
What the Lean code literally says, in plain math · Codex GPT-6 (independent fresh-context sub-agent)
The following assertions are equivalent: (i) for every natural number , there exist natural numbers such that and ; (ii) for every natural number that is prime and has remainder upon division by , there exist natural numbers such that and . All fractions and equalities are interpreted in the rational numbers, with the natural numbers embedded into them. The witnesses may depend on or . Although natural numbers include , the denominator inequalities require three positive, pairwise distinct denominators in increasing order, and neither assertion requires a decomposition for , , or .
Confirmed by the mission captain (proposal self-audit).