ResidualTrap
plain-language theorem explainer
ResidualTrap defines the class of natural numbers n > 1 with n ≡ 1 mod 24 whose prime factors, together with those of (n + 3)/4, are all congruent to 1 mod 3. Number theorists working on the Erdős-Straus conjecture via the Recognition Composition Law cite this predicate to isolate the residual cases that require separate phase-support arguments. The definition is assembled as a direct conjunction of the stated arithmetic conditions.
Claim. A natural number $n$ belongs to the residual trapped class when $n > 1$, $n ≡ 1 mod 24$, every prime factor of $n$ is congruent to 1 mod 3, and every prime factor of $(n + 3)/4$ is congruent to 1 mod 3.
background
The Erdős-Straus Recognition Rotation Hierarchy module reduces the RCL attack on rational representations to finite gate pieces plus two missing engines: prime phase separation across admissible residual quotients and reciprocal pair closure once phase support appears. ResidualTrap isolates the trapped residuals after the explicit formulas, capturing precisely those n ≡ 1 mod 24 built only from primes 1 mod 3. Upstream results supply the 8-tick phases (periodic with period 2π) and the active edge count A that fix the periodic structure for subsequent phase arguments; the module states that no new axiom is introduced and the missing engines remain explicit structure fields.
proof idea
As a definition, ResidualTrap is assembled directly by conjoining the four arithmetic predicates 1 < n, n % 24 = 1, AllPrimeFactorsOneModThree n, and AllPrimeFactorsOneModThree ((n + 3)/4). No lemmas or tactics are invoked; the predicate simply records the residual class for later use as a hypothesis.
why it matters
ResidualTrap supplies the hypothesis for erdos_straus_residual_from_effectivePrimePhaseInput, erdos_straus_residual_closed, and bounded_balanced_search_solved, each of which shows that bounded phase visibility or effective prime phase input yields a rational Erdős-Straus representation. It marks the precise point in the RCL attack where the eight-tick octave and phi-ladder must be instantiated to close the residual cases. The open question it isolates is the existence of the prime phase separation engine across admissible residual quotients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.