AllPrimeFactorsOneModThree
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.