bounded_balanced_search_solved
plain-language theorem explainer
A bounded balanced-search engine produces a rational Erdős-Straus representation for every residual trap n. Researchers attacking the Erdős-Straus conjecture via phase hierarchies would cite this reduction. The proof extracts the balanced pair witness from the engine's bound_ok predicate and feeds it directly into the phase-support representation lemma.
Claim. Suppose $B$ is a bounded balanced-search engine. Then for every natural number $n$ in the residual trap class, there exist nonzero rationals $x,y,z$ such that $4/n = 1/x + 1/y + 1/z$. The residual trap class consists of integers $n>1$ with $n≡1 mod 24$ whose prime factors (and those of $(n+3)/4$) are all congruent to 1 modulo 3.
background
The Erdős-Straus Recognition Rotation Hierarchy module isolates the finite and gate pieces of the RCL attack on the conjecture, leaving two missing engines: prime phase separation and reciprocal pair closure. ResidualTrap n holds when $n>1$, $n mod 24 =1$, and both $n$ and $(n+3)/4$ have exclusively primes congruent to 1 mod 3. BoundedBalancedSearchEngine is a structure supplying a bound function together with the guarantee that for any such $n$ there exists $c$ at most the bound, an admissible hard gate at $c$, and balanced pair phase support for $n$ and $c$ (see its bound_ok field).
proof idea
The proof is a one-line wrapper. It cases on the bound_ok field of the supplied engine applied to $n$ and the trap hypothesis, obtaining a gate $c$ together with the balanced pair phase support witness. It then applies the theorem balanced_pair_phase_support_gives_repr to that witness to conclude the representation.
why it matters
This theorem sits at the center of the rotation hierarchy: it reduces the residual Erdős-Straus class to the existence of a bounded search engine. The two downstream results in PrimePhaseDistribution apply it once a prime phase box distribution or RS prime phase box theorem is supplied, yielding the conditional forms of the conjecture for the trapped class. It fills the concrete target identified in the module: locating the gate and reciprocal pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.