ReciprocalPairClosureEngine
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove existence of phase support for any concrete n.
- Does not construct explicit values for the witness rationals.
- Does not extend beyond residual traps n≡1 mod 24.
- Does not reference the T0-T8 forcing chain or spatial dimension D=3.
- Does not address the Berry creation threshold or phi-ladder mass formula.
formal statement (Lean)
189structure ReciprocalPairClosureEngine : Prop where
190 close :
191 ∀ n c : ℕ, ResidualTrap n → AdmissibleHardGate c → GateHasPhaseSupport n c →
192 GateClosureWitness n c
193
194/-- Stronger, fully arithmetic bounded search: the search returns the actual
195balanced phase pair, not merely abstract phase support. -/