AllPrimeFactorsOneModThree
AllPrimeFactorsOneModThree defines the predicate on a natural number m requiring every prime divisor to satisfy p ≡ 1 mod 3. Researchers attacking the Erdős–Straus conjecture via the Recognition rotation hierarchy cite it to isolate admissible prime residues in residual quotients. The definition is a direct universal quantification with no auxiliary lemmas or reductions.
claimFor a natural number $m$, every prime $p$ dividing $m$ satisfies $p ≡ 1 mod 3$.
background
The Erdős–Straus Recognition Rotation Hierarchy module converts the current RCL attack into a theorem-shaped proof skeleton. It isolates two missing number-theoretic engines: prime phase separation across admissible residual quotients and reciprocal pair closure once phase support appears. No new axioms are introduced; the engines appear as explicit structure fields for future proofs to supply.
proof idea
This is a definition that directly encodes the universal property: for all primes p dividing m, p mod 3 equals 1. It applies the repo-local alias Prime (transparent wrapper for Nat.Prime) and the divisibility relation from Mathlib. No upstream lemmas are invoked; the body is the explicit statement.
why it matters in Recognition Science
It supplies the prime-phase condition required by the downstream ResidualTrap definition, which states that n ≡ 1 mod 24 and both ledger sources are built only from primes 1 mod 3. This fills the first missing engine (prime phase separation) in the hierarchy skeleton. The module doc-comment notes that the two engines remain as structure fields to be discharged by later theorems.
scope and limits
- Does not assert existence of any m satisfying the predicate.
- Does not prove the full Erdős–Straus conjecture or any rotation closure.
- Does not constrain the size or distribution of the primes beyond the residue condition.
- Does not interact with the J-cost or phi-ladder constructions from the Foundation module.
formal statement (Lean)
152def AllPrimeFactorsOneModThree (m : ℕ) : Prop :=
proof body
Definition body.
153 ∀ p : ℕ, Nat.Prime p → p ∣ m → p % 3 = 1
154
155/-- The residual trapped class after the explicit formulas:
156`n ≡ 1 mod 24`, and both ledger sources are built only from primes
157`1 mod 3`. -/