residual_trap_solved
plain-language theorem explainer
Rotation separation via a prime phase equidistribution engine combined with reciprocal pair closure solves the residual trap class for the Erdős–Straus conjecture. Number theorists reducing the conjecture inside the Recognition Science RCL framework cite this result to isolate the two required engines as explicit assumptions. The proof extracts an admissible gate and its phase support from the first engine then feeds them directly into the closure operation of the second to obtain the representation witness.
Claim. Let $E$ be a prime phase equidistribution engine and $C$ a reciprocal pair closure engine. For every natural number $n$ satisfying the residual trap conditions ($n>1$, $n≡1 mod 24$, and all prime factors of both $n$ and $(n+3)/4$ congruent to 1 modulo 3), the rational $n$ admits an Erdős–Straus representation.
background
The Erdős–Straus Recognition Rotation Hierarchy module reduces the conjecture to two explicit structure assumptions. A PrimePhaseEquidistributionEngine separates any residual trap by an admissible hard gate that carries phase support. A ReciprocalPairClosureEngine converts such support into a gate closure witness that yields the required rational representation. ResidualTrap n holds precisely when $n>1$, $n mod 24 =1$, and both $n$ and $(n+3)/4$ have exclusively prime factors congruent to 1 mod 3. The module proves the finite and gate pieces while leaving the two engines as open structure fields to be supplied by future work. This construction sits inside the Recognition Science attack on the conjecture that employs the Recognition Composition Law to control J-costs across the phi-ladder.
proof idea
The term proof performs rcases on the phase_support field of the equidistribution engine applied to $n$ and the trap hypothesis. This yields an admissible gate $c$ together with the support witness. These arguments are passed to the close field of the reciprocal closure engine, producing a gate closure witness. The gate_closure_witness_gives_repr lemma is then applied to extract the representation.
why it matters
This declaration completes the core reduction in the Erdős–Straus Rotation Hierarchy. It is invoked by the downstream theorem bounded_residual_trap_solved, which replaces the phase engine by a bounded search engine via the implication bounded_search_implies_phase_equidistribution. In the Recognition framework it isolates the prime phase separation and reciprocal closure steps required to settle the residual class under the RCL, without new axioms. The module doc-comment notes that these engines remain the genuinely missing number-theoretic pieces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.