ReciprocalPairClosureEngine
plain-language theorem explainer
Reciprocal pair closure asserts that any residual trap n paired with an admissible hard gate c carrying phase support yields an explicit rational divisor witness. Number theorists attacking the Erdős-Straus conjecture inside the recognition rotation hierarchy cite this as the second missing engine. The declaration is a bare structure definition whose single field packages the universal quantification with no proof obligations.
Claim. For all natural numbers $n$ and $c$, if $n>1$, $n≡1 mod 24$, all prime factors of $n$ and of $(n+3)/4$ are ≡1 mod 3, $c≡3 mod 4$, and there exists a residual phase quotient for $c$, then there exist rationals $x,N,d,q$ such that $n≠0$, $x≠0$, $c≠0$, $N=n·x$, $x=(n+c)/4$, $d·q=N$, $(N+d)/c≠0$, and $(N+N·q)/c≠0$.
background
The module converts the RCL attack on the Erdős-Straus conjecture into a proof skeleton by isolating two missing engines as explicit structure fields rather than axioms. Reciprocal pair closure is the second of these; the first is prime phase separation across admissible residual quotients. Local notation follows the eight-tick phases and balanced ledgers imported from the foundation layer.
proof idea
This is a structure definition with no proof body. The single field close directly encodes the universal quantification over the four predicates. No lemmas or tactics are invoked; the declaration simply records the required closure property for downstream instantiation.
why it matters
It supplies the reciprocal closure step required once phase support appears, feeding directly into residual_trap_solved and bounded_residual_trap_solved. Those theorems combine it with phase equidistribution to obtain HasRationalErdosStrausRepr for residual traps. In the framework it closes the arithmetic gap after T5 J-uniqueness and the RCL identity are granted, without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.